CEA /LIST - Laboratoire d'intégration de systèmes et de technologies

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é. ","identifier":{"@type":"PropertyValue","name":"Université Paris-Saclay GS Informatique et sciences du numérique","value":"5be6738c74bb22a4f4f4a6b0d9526d59"},"url":"https://www.hellowork.com/fr-fr/emplois/76931919.html","datePosted":"2026-03-17T17:43:02Z","directApply":false,"employmentType":["TEMPORARY","FULL_TIME"],"experienceRequirements":"no requirements","hiringOrganization":{"@type":"Organization","name":"Université Paris-Saclay GS Informatique et sciences du numérique"},"industry":"Service public d'état","jobLocation":{"@type":"Place","address":{"@type":"PostalAddress","addressCountry":"FR","addressLocality":"Paris","addressRegion":"Île-de-France","postalCode":"75000"}},"qualifications":"Connaissances en méthodes formelles/programmation

É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

{"@context":"https://schema.org","@type":"JobPosting","title":"Thèse Analyses de Sécurité par Interprétation Abstraite. H/F","description":"