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...

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...

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...

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...

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...

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...

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 ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault...

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 ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault...

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 ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault...

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 ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault...

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 ? Certaines informations sont plus confidentielles que d'autres, ou plus digne de confiance que d'autres. Après une introduction aux politiques de confidentialité de Bell-Lapadula et d'intégrité de Biba, nous étudierons comment contrôler les flux d'information à travers un programme, ou bien dynamiquement, ou bien statiquement à l'aide de systèmes de types ou...

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 ? Certaines informations sont plus confidentielles que d'autres, ou plus digne de confiance que d'autres. Après une introduction aux politiques de confidentialité de Bell-Lapadula et d'intégrité de Biba, nous étudierons comment contrôler les flux d'information à travers un programme, ou bien dynamiquement, ou bien statiquement à l'aide de systèmes de types ou...

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 ? Comment rendre un logiciel résistant non seulement aux « bugs » et aux pannes involontaires, mais aussi aux attaques et à l'utilisation malveillante ? C'est le problème général de la sécurité du logiciel, que nous introduirons dans ce premier cours. Nous étudierons ensuite quelques attaques récentes et les vulnérabilités logicielles qu'elles exploitent.

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 ? Comment rendre un logiciel résistant non seulement aux « bugs » et aux pannes involontaires, mais aussi aux attaques et à l'utilisation malveillante ? C'est le problème général de la sécurité du logiciel, que nous introduirons dans ce premier cours. Nous étudierons ensuite quelques attaques récentes et les vulnérabilités logicielles qu'elles exploitent.

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Les processeurs multicœurs sont un exemple d'architecture parallèle à mémoire partagée, où plusieurs unités de calcul travaillent simultanément sur une mémoire commune. La programmation de ces architectures est difficile : il faut maîtriser les interférences possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Les processeurs multicœurs sont un exemple d'architecture parallèle à mémoire partagée, où plusieurs unités de calcul travaillent simultanément sur une mémoire commune. La programmation de ces architectures est difficile : il faut maîtriser les interférences possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des...