Description du sujet de thèse
Domaine
Défis technologiques
Sujets de thèse
Combinaison de sous et surapproximations de la memoire pour l'analyse de code bas-niveau
Contrat
Thèse
Description de l'offre
Le théorème de Rice énonçant qu'on ne peut pas avoir de méthode qui sache automatiquement dire si une propriété sur un programme est vraie ou non a conduit à séparer les outils de vérification en deux groupes: les outils sound fonctionnant par sur-approximation, comme l'interprétation abstraite, sont capables de prouver automatiquement que certaines propriétés sont vraies, mais ne savent parfois pas conclure et produisent des alarmes; à l'inverse, les outils complete fonctionnant par sous-approximation, comme l'exécution symbolique, savent produire des contre-exemples, mais pas démontrer si une propriété est vraie.
*Le but général de la thèse est d'étudier la combinaison entre méthodes sound et complete d'analyse de programme, et en particulier l'analyse statique par interprétation abstraite et la génération de formules sous-approximée par exécution symbolique*.
Nous nous intéresserons particulièrement à la combinaison d'abstractions sur et sous-approximantes, en particulier pour la mémoire. Les applications envisagées en priorité concernent les analyses de code au niveau binaire, telles que réalisées par la combinaison des plateformes d'analyse BINSEC et CODEX, pour pouvoir trouver des failles de securite automatiquement ou demontrer leur absence.
Université / école doctorale
Sciences Mathématiques de Paris Centre (ED386)
Sorbonne Université
Localisation du sujet de thèse
Site
Saclay
Critères candidat
Formation recommandée
Informatique, mathématiques
Demandeur
Disponibilité du poste
01/10/2025
Personne à contacter par le candidat
LEMERRE Matthieu < email supprimé pour raison de sécurité >
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
RIVAL Xavier < email supprimé pour raison de sécurité >
INRIA
INRIA/Ens ULM
DI - Ecole Normale Supérieure
45, rue d'Ulm
75230 Paris Cedex 05 - France
+33 1 44 32 21 50
En savoir plus
Domaine
Défis technologiques
Sujets de thèse
Combinaison de sous et surapproximations de la memoire pour l'analyse de code bas-niveau
Contrat
Thèse
Description de l'offre
Le théorème de Rice énonçant qu'on ne peut pas avoir de méthode qui sache automatiquement dire si une propriété sur un programme est vraie ou non a conduit à séparer les outils de vérification en deux groupes: les outils sound fonctionnant par sur-approximation, comme l'interprétation abstraite, sont capables de prouver automatiquement que certaines propriétés sont vraies, mais ne savent parfois pas conclure et produisent des alarmes; à l'inverse, les outils complete fonctionnant par sous-approximation, comme l'exécution symbolique, savent produire des contre-exemples, mais pas démontrer si une propriété est vraie.
*Le but général de la thèse est d'étudier la combinaison entre méthodes sound et complete d'analyse de programme, et en particulier l'analyse statique par interprétation abstraite et la génération de formules sous-approximée par exécution symbolique*.
Nous nous intéresserons particulièrement à la combinaison d'abstractions sur et sous-approximantes, en particulier pour la mémoire. Les applications envisagées en priorité concernent les analyses de code au niveau binaire, telles que réalisées par la combinaison des plateformes d'analyse BINSEC et CODEX, pour pouvoir trouver des failles de securite automatiquement ou demontrer leur absence.
Université / école doctorale
Sciences Mathématiques de Paris Centre (ED386)
Sorbonne Université
Localisation du sujet de thèse
Site
Saclay
Critères candidat
Formation recommandée
Informatique, mathématiques
Demandeur
Disponibilité du poste
01/10/2025
Personne à contacter par le candidat
LEMERRE Matthieu < email supprimé pour raison de sécurité >
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
RIVAL Xavier < email supprimé pour raison de sécurité >
INRIA
INRIA/Ens ULM
DI - Ecole Normale Supérieure
45, rue d'Ulm
75230 Paris Cedex 05 - France
+33 1 44 32 21 50
En savoir plus
