Xavier Leroy

Collège de France

Science du logiciel

Année 2021-2022

Sécurité du logiciel : quel rôle pour les langages de programmation ?

Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.

Xavier Leroy

Collège de France

Science du logiciel

Année 2021-2022

Sécurité du logiciel : quel rôle pour les langages de programmation ?

Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.

Collège de France

Informatique et sciences numériques (chaire annuelle 2021-2022)

Wendy Mackay

Année 2021-2022

L'avènement de l'intelligence artificielle (IA) a transformé notre façon d'interagir avec les ordinateurs. Même si l’IA peut parfois remplacer l’humain, elle est le plus souvent vouée à aider celui-ci, par exemple dans des tâches d’aide à la décision. Pourtant, une grande partie de la recherche actuelle se concentre sur la manière de créer des algorithmes plus puissants, et moins sur la manière dont ces algorithmes affectent les personnes qui les utilisent. Cette leçon retrace l'histoire des relations entre l'IA et de l'IHM, y compris mes propres recherches sur les partenariats homme-machine, où les utilisateurs restent maîtres de l'interaction afin de passer du paradigme de « l’être humain dans la boucle » à celui de « l’ordinateur dans la boucle ».

Collège de France

Informatique et sciences numériques (chaire annuelle 2021-2022)

Wendy Mackay

Année 2021-2022

L'avènement de l'intelligence artificielle (IA) a transformé notre façon d'interagir avec les ordinateurs. Même si l’IA peut parfois remplacer l’humain, elle est le plus souvent vouée à aider celui-ci, par exemple dans des tâches d’aide à la décision. Pourtant, une grande partie de la recherche actuelle se concentre sur la manière de créer des algorithmes plus puissants, et moins sur la manière dont ces algorithmes affectent les personnes qui les utilisent. Cette leçon retrace l'histoire des relations entre l'IA et de l'IHM, y compris mes propres recherches sur les partenariats homme-machine, où les utilisateurs restent maîtres de l'interaction afin de passer du paradigme de « l’être humain dans la boucle » à celui de « l’ordinateur dans la boucle ».

Xavier Leroy

Collège de France

Science du logiciel

Année 2021-2022

Sécurité du logiciel : quel rôle pour les langages de programmation ?

Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.

Xavier Leroy

Collège de France

Science du logiciel

Année 2021-2022

Sécurité du logiciel : quel rôle pour les langages de programmation ?

Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.

Collège de France

Informatique et sciences numériques (chaire annuelle 2021-2022)

Wendy Mackay

Année 2021-2022

Les médias sociaux sont aujourd’hui partout et notre capacité à collaborer à distance est devenue une seconde nature, particulièrement depuis la pandémie, avec des outils de partage de documents et de communication directe ou différée par le texte, la voix ou la vidéo. Cette leçon retrace l'histoire de la communication médiatisée, en incluant des exemples tirés de mes propres recherches sur les mediaspaces et la vidéo collaborative, et décrit les recherches récentes sur la façon dont les innovations des utilisateurs avec les médias sociaux ont transformé notre façon de penser et d'utiliser les ordinateurs.

Collège de France

Informatique et sciences numériques (chaire annuelle 2021-2022)

Wendy Mackay

Année 2021-2022

Les médias sociaux sont aujourd’hui partout et notre capacité à collaborer à distance est devenue une seconde nature, particulièrement depuis la pandémie, avec des outils de partage de documents et de communication directe ou différée par le texte, la voix ou la vidéo. Cette leçon retrace l'histoire de la communication médiatisée, en incluant des exemples tirés de mes propres recherches sur les mediaspaces et la vidéo collaborative, et décrit les recherches récentes sur la façon dont les innovations des utilisateurs avec les médias sociaux ont transformé notre façon de penser et d'utiliser les ordinateurs.

Xavier Leroy

Collège de France

Science du logiciel

Année 2021-2022

Sécurité du logiciel : quel rôle pour les langages de programmation ?

Qu'il soit vérifié dynamiquement (pendant l'exécution) ou statiquement (par analyse préalable), le typage est un aspect essentiel des langages de programmation de haut niveau. Dans ce cours, nous étudierons les contributions du typage à la sécurité des logiciels, des garanties de base (sûreté des valeurs et de la mémoire) indispensables pour l'isolation logicielle à des garanties d'intégrité plus fines s'appuyant sur l'abstraction de types et l'encapsulation procédurale des valeurs. Nous parlerons aussi des ownership types et des assertions en logique de séparation, et de leurs utilisations possibles pour la sécurité.

Xavier Leroy

Collège de France

Science du logiciel

Année 2021-2022

Sécurité du logiciel : quel rôle pour les langages de programmation ?

Qu'il soit vérifié dynamiquement (pendant l'exécution) ou statiquement (par analyse préalable), le typage est un aspect essentiel des langages de programmation de haut niveau. Dans ce cours, nous étudierons les contributions du typage à la sécurité des logiciels, des garanties de base (sûreté des valeurs et de la mémoire) indispensables pour l'isolation logicielle à des garanties d'intégrité plus fines s'appuyant sur l'abstraction de types et l'encapsulation procédurale des valeurs. Nous parlerons aussi des ownership types et des assertions en logique de séparation, et de leurs utilisations possibles pour la sécurité.