Verified programming and secure integration of operating system libraries in Coq

Vous êtes invité.e.s à venir assister à la soutenance de thèse de Shenghao Yuan (Equipe TEA) qui se tiendra le 8/12/23 à 14h30, en Salle Métivier.

ATTENTION dans le cadre du plan VIGIPIRATE la règle suivante s'applique pour cet évènement :
L’accès du public à cette soutenance est contraint à une inscription préalable obligatoire auprès de : armelle [*] mozziconacciirisa [*] fr

L’accès ne sera pas autorisé sans inscription préalable. Par ailleurs, les visiteurs ne porteront ni bagage ni sac.

Résumé :

Les fonctionnalités bas niveaux offertes par le langage de programmation C sont à la fois un atout et une source d’erreurs. D’une part, il a été conçu [KR02] pour offrir un contrôle très détaillé de la représentation des données au niveau octet en mémoire informatique. Cette fonctionnalité de bas niveau permet aux programmeurs de développer des artefacts hautement efficaces, économes en ressources, et faciles à lire par rapport au code d’assemblage au niveau machine. Par conséquent, des milliards de lignes de code C hérité sont toujours en service dans des domaines critiques (et non critiques), notamment la finance, les transports, les réseaux numériques et en particulier l’Internet des objets (IoT). D’autre part, le revers de la médaille est que l’utilisation du C facilite les erreurs de gestion de la mémoire de bas niveau, telles que le débordement de flottant, le dépassement de tableau, et l’utilisation après libération, etc. L’abstraction de bas niveau du code C accroît également les vulnérabilités dans des systèmes distribués complexes et parfois critiques, par exemple, en introduisant des erreurs logiques.
Il existe plusieurs façons de détecter les défauts logiciels. Une solution consiste à suivre un processus de développement logiciel strict et qualifiable pour mettre en œuvre des artefacts certifiés (e.g., SCADE KCG [Ber07]) qui satisfont aux exigences de certification
(e.g., DO-178C [Rie17]) pour des domaines critiques spécifiques. Une autre approche consiste à concevoir un nouveau langage doté de fonctionnalités de sécurité spécifiques (e.g., Rust [MK14] pour garantir la sécurité de la mémoire). Bien que ces mesures soient capables
de détecter certaines vulnérabilités, elles ne peuvent généralement pas garantir l’absence de vulnérabilités, en particulier pas de manière rigoureuse sur le plan mathématique.