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