Analyses statiques avancées basées sur les types pour la vérification de systèmes d'exploitations

Description de l'offre : Dans des travaux récents [RTAS 2021], nous avons démontré l'intérêt d'une analyse statique guidée par un système de types dépendants avancé pour analyses des programmes systèmes bas-niveau, allant jusqu'à pouvoir vérifier automatiquement l'absence d’escalade de privilège dans un noyau de système d'exploitation embarqué comme conséquence de la type-safety du code du noyau. La gestion de la mémoire est un problème particulièrement ardu lors de l'analyse de programmes systèmes, ou plus largement, de programmes écrits en C, et l’analyse basée sur les types fournit une solution satisfaisante à applicabilité large (par exemple, code de gestion de structures de données [VMCAI 2022], runtime de langage dynamique, code applicatif orienté performance, etc.) Le but de la thèse est d’étendre les applications qui peuvent être faites de l’utilisation d’une analyse statique basée sur les types. [RTAS’21] No Crash, No Exploit: Automated Verification of Embedded Kernels. O. Nicole, M. Lemerre, S. Bardin, X. Rival (Best paper) [VMCAI’22] Lightweight Shape Analysis based on Physical Types, O. Nicole, M. Lemerre, X. Rival [POPL’23] SSA Translation Is an Abstract Interpretation, M. Lemerre (Distinguished paper).

Profil du candidat : Master informatique ou Ecole d'ngenieur. Bagage en vérification/analyse statique ,programmation en OCaml, connaissance du C ou assembleur, sont des avantages.