Qui sommes-nous ?
Espace utilisateur
Formation continue
Credit : L. Godart/CEA
D’un jour à plusieurs semaines, nos formations permettent une montée en compétence dans votre emploi ou accompagnent vers le retour à l’emploi. 
Conseil et accompagnement
Crédit : vgajic
Fort de plus de 60 ans d’expériences, l’INSTN accompagne les entreprises et organismes à différents stades de leurs projets de développement du capital humain.
Thèses
Accueil   /   Thèses   /   Analyses statiques avancées basées sur les types pour la vérification de systèmes d'exploitations

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

Cybersécurité : hardware et software Défis technologiques Informatique et logiciels Sciences pour l’ingénieur

Résumé du sujet

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

Laboratoire

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down