Thèse Analyses de Sécurité par Interprétation Abstraite. H/F - Université Paris-Saclay GS Informatique et sciences du numérique

Établissement : Université Paris-Saclay GS Informatique et sciences du numérique
École doctorale : Sciences et Technologies de l'Information et de la Communication
Laboratoire de recherche : CEA /LIST - Laboratoire d'intégration de systèmes et de technologies
Direction de la thèse : Matthieu LEMERRE ORCID 0000000210810467
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-12-19T23:59:59

Depuis récemment, les outils de vérification par interprétation abstraite de code bas-niveau sont devenus suffisamment mûrs pour réaliser des analyses de sécurité. Ils savent notamment faire des analyses précises des propriétés mémoires des programmes, des analyses modulaires sur des morceaux de programmes, et des analyses capables de gérer les aspects bas-niveau du langage. L'outil Codex, développé au CEA LIST, est une exemple d'outil capable de faire ce type d'analyses.

Le but de cette thèse est d'explorer les possibilités permises par un outil d'interprétation abstraite pour réaliser des analyses de sécurité, couvrant les différents aspects: aide à la compréhension de code, vérification d'absence d'erreurs dans des sous parties du code, utilisation des invariants pour produire un langage intermédiaire optimisé.

*Contexte.* Un des rôles important d'un ingénieur sécurité est d'évaluer la sécurité d'un logiciel:
comprendre si un attaquant, qui serait en mesure de contrôler certaines des données envoyées à ce
logiciel, pourrait conduire ce dernier à s'exécuter de manière imprévue : crash du logiciel,
corruption de bases de données, prise de contrôle par injection de code, etc. La méthode dominante
pour ce faire consiste à analyse le code du logiciel avec des outils de base: débogueur ou
désassembleur. Si certains outils, comme le fuzzing ou l'exécution symbolique, peuvent contribuer à
trouver des vulnérabilités, ils ne peuvent pas remplacer l'inspection manuelle : fonctionnant
uniquement par sous-approximation, ils oublient des comportements qu'un attaquant pourrait exploiter
pour trouver une attaque.

Il existe cependant une méthode d'analyse automatique fonctionnant par sur-approximation, permettant
de calculer automatiquement des propriétés qui sont vraies sur tous les comportements du programme :
l'interprétation abstraite. Grâce à elle, il est possible de montrer que certaines attaques sont
impossible, ce qui peut permettre à l'analyse de ne pas avoir besoin de les considérer.

Les applications traditionelles de l'interprétation abstraite sont l'optimisation de programmes dans
les compilateurs et la vérification automatique de logiciel. Les outils issus de la recherche sont
mûrs industriellement pour des analyses numériques automatique d'un système embarqué entier, avec des
succès comme Astrée ou Frama-C. Mais il y a une marche significative entre cela et une analyse
statique de programmes utilisable par un ingénieur sécurité demande, au contraire une analyse qui:

- Sache analyser précisément les propriétés mémoire du programme, car les programmes généralistes font
des allocations dynamiques, car la corruption mémoire est une source importante d'attaques, et que
l'analyse mémoire est un pré-requis indispensable à d'autre analyses comme des analyses de teinte;
- Soit modulaire/compositionelle: il faut pouvoir analyser des morceaux de programmes indépendants,
permettant ainsi à l'analyse d'être utile sur les parties d'intérêt pour l'analyste;
- Soit interactive: il faut que l'analyste puisse lancer des analyses dans des cas particuliers, pour
se concentrer sur certaines attaques; il faut qu'il puisse utiliser les résultats de l'analyse pour
mieux comprendre le programme analysé; il faut que la compréhension du programme par l'analyste
permette de raffiner les résultats de l'analyse;
- Soit précise sur des codes bas-niveau, comme du code C généraliste ou du code binaire exécutable.

Cependant, des progrès récents réalisés dans les analyse symbolique et analyse de code mémoire
permettent de répondre à ces problèmes; le logiciel Codex du CEA LIST, qui les intègre, est ainsi un
des premiers outils d'analyse par interprétation abstraite sachant répondre simultanément à toutes ces
contraintes. Codex prend ainsi en compte des analyses mémoires poussées, basées sur la logique de
séparation [FMSD'21] ou le typage [VMCAI'21,OOPSLA'23]. Il permet de réaliser des analyses
compositionelles [SAS'20,OOPSLA'23]. Il utilise un langage de spécification, TypedC, basé sur des
types; types dont la récupération est un des objectifs primordiaux pour la compréhension de programmes
binaires. Enfin, il dispose d'analyses numériques précises et efficaces [PLDI'24,PLDI'25], et sa
précision a été démontrée pour la vérification de codes binaire de taille importante [RTAS'21]. Enfin,
il permet des analyses statiques symboliques, permettant à l'analyse de faire facilement également des
transformations de programmes, qui peuvent s'appliquer pour décompiler [PLDI'24] ou étudier le flot de
valeurs [POPL'23] d'un programme.

Dans ces conditions, il devient faisable d'envisager l'utilisation d'un interpréteur abstrait pour
l'aide à l'analyse de sécurité.

*But* Le but de cette thèse est d'explorer les possibilités permises par un outil d'interprétation
abstraite pour réaliser des analyses de sécurité, couvrant les différents aspects: aide à la
compréhension de code, vérification d'absence d'erreurs dans des sous parties du code, utilisation des
invariants pour produire un langage intermédiaire optimisé. Nous envisageons notamment les premières
pistes suivantes:

- Utilisation de l'interprétation abstraite pour un 'slicing' optimisé, ne conservant que les parties
du programme 'utiles' selon des critères définis par l'analyste (atteignant/passant certains points de
programmes, dépendant de certaines entrées, selon certaines conditions, etc.);
- Décompilation par interprétation abstraite: récupération d'une forme intermédiaire d'une slice du
programme, optimisée pour une inspection et pour des analyses ultérieures;
- Analyses de dépendances poussées (utilisation d'un langage de formules représentant le flot de
donnée, intégration de propriétés de flot d'information au langage de typage, etc.);
- Interaction analyste/analyseur pour des analyses de sécurité (présentation des résultats, ajouts
d'hypothèses de travail, sélection de comportements d'intérêt)

Connaissances en méthodes formelles/programmation fonctionnelle/sécurité.