Informations générales
Entité de rattachement
Le CEA est un acteur majeur de la recherche, au service des citoyens, de l'économie et de l'Etat.
Il apporte des solutions concrètes à leurs besoins dans quatre domaines principaux : transition énergétique, transition numérique, technologies pour la médecine du futur, défense et sécurité sur un socle de recherche fondamentale. Le CEA s'engage depuis plus de 75 ans au service de la souveraineté scientifique, technologique et industrielle de la France et de l'Europe pour un présent et un avenir mieux maîtrisés et plus sûrs.
Implanté au cœur des territoires équipés de très grandes infrastructures de recherche, le CEA dispose d'un large éventail de partenaires académiques et industriels en France, en Europe et à l'international.
Les 20 000 collaboratrices et collaborateurs du CEA partagent trois valeurs fondamentales :
• La conscience des responsabilités
• La coopération
• La curiosité
Référence
SL-DRT-24-0543
Direction
DRT
Description du sujet de thèse
Domaine
Défis technologiques
Sujets de thèse
Combinaison de sur et sous-approximations pour l'analyse de programmes bas-niveau
Contrat
Thèse
Description de l'offre
Parce que l'analyse de programme est un problème indécidable, les analyses statiques se divisent en 2 catégories:
- Les analyses sound, qui calculent une surapproximation de tous les comportements du programme, et permettent de vérifier l'absence d'erreur.
- Les analyses complete, qui calculent une sous-approximation des comportements possibles du programme, et permettent de trouver des erreurs.
Le but de la thèse est d'étudier cette combinaison de ces techniques pour l'analyse statique de programmes bas-niveau, en particulier des exécutables binaires, en ciblant notamment les analyses de la mémoires et du flot de contrôle, qui sont les informations capitales pour comprendre les comportements possibles d'un binaire.
[POPL'23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award)
[VMCAI'22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[RTAS'21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award)
[LPAR'18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre
Université / école doctorale
Sciences et Technologies de l’Information et de la Communication (STIC)
Paris-Saclay
Localisation du sujet de thèse
Site
Saclay
Critères candidat
Formation recommandée
Master informatique ou Ecole d'ingenieu. Bagage en vérification/analyse statique,programmation en OCaml, connaissance du C ou assembleur, sont des avantages.
Demandeur
Disponibilité du poste
01/10/2024
Personne à contacter par le candidat
LEMERRE Matthieu 
matthieu.lemerre@cea.fr
CEA
DRT/DILS//LSL
CEA - Centre de Saclay BP 94
F91191 Gif sur Yvette CEDEX
01 69 08 26 28
Tuteur / Responsable de thèse
LEMERRE Matthieu matthieu.lemerre@cea.fr
CEA
DRT/DILS//LSL
CEA - Centre de Saclay BP 94
F91191 Gif sur Yvette CEDEX
01 69 08 26 28
En savoir plus
