88 épisodes

Xavier Leroy a étudié les mathématiques puis l'informatique à l'École Normale Supérieure et à l'Université Paris Diderot. Après un doctorat en informatique fondamentale en 1992 et un postdoctorat à l'Université Stanford, il devient chargé de recherche à l'Inria en 1994, puis directeur de recherche en 2000. Il y a dirige aujourd'hui l'équipe de recherche GALLIUM. De 1999 à 2004, il participe à la start-up Trusted Logic. Il est nommé Professeur au Collège de France en mai 2018 et devient le titulaire de la chaire Sciences du logiciel.

Les travaux de recherche de Xavier Leroy portent d'une part sur les nouveaux langages et outils de programmation, et d'autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l'un des principaux développeurs du langage de programmation fonctionnelle OCaml et du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.

Sciences du logiciel - Xavier Leroy Collège de France

    • Éducation

Xavier Leroy a étudié les mathématiques puis l'informatique à l'École Normale Supérieure et à l'Université Paris Diderot. Après un doctorat en informatique fondamentale en 1992 et un postdoctorat à l'Université Stanford, il devient chargé de recherche à l'Inria en 1994, puis directeur de recherche en 2000. Il y a dirige aujourd'hui l'équipe de recherche GALLIUM. De 1999 à 2004, il participe à la start-up Trusted Logic. Il est nommé Professeur au Collège de France en mai 2018 et devient le titulaire de la chaire Sciences du logiciel.

Les travaux de recherche de Xavier Leroy portent d'une part sur les nouveaux langages et outils de programmation, et d'autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l'un des principaux développeurs du langage de programmation fonctionnelle OCaml et du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.

    • video
    07 - Sécurité du logiciel : quel rôle pour les langages de programmation ? - VIDEO

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

    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.

    • 1h 4 min
    07 - Sécurité du logiciel : quel rôle pour les langages de programmation ?

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

    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.

    • 1h 4 min
    • video
    06 - Sécurité du logiciel : quel rôle pour les langages de programmation ? - VIDEO

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

    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.

    • 1h 18 min
    06 - Sécurité du logiciel : quel rôle pour les langages de programmation ?

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

    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.

    • 1h 18 min
    • video
    05 - Sécurité du logiciel : quel rôle pour les langages de programmation ? - VIDEO

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

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

    • 1h 24 min
    05 - Sécurité du logiciel : quel rôle pour les langages de programmation ?

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

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

    • 1h 24 min

Classement des podcasts dans Éducation

Choses à Savoir
Juliette Katz
Clotilde Dusoulier
Miracle Fajr Podcast
Stéphane Genêt
Chloé Bloom