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.

Donner l'assurance que les systèmes autonomes fonctionneront de manière sûre et sécurisée est une condition préalable à leur déploiement dans des domaines d'application critiques en termes de mission et de sécurité. Généralement, les assurances sont fournies sous la forme de cas d'assurance, qui sont des arguments vérifiables et raisonnés démontrant qu'une revendication de haut niveau (concernant généralement la sécurité ou d'autres propriétés critiques) est satisfaite compte tenu d'un ensemble de preuves relatives au contexte, à la conception et à la mise en œuvre d'un système. L'élaboration de cas d'assurance est traditionnellement une activité analytique, réalisée hors ligne avant le déploiement du système, et sa validité repose sur des hypothèses/prédictions concernant le comportement du système (y compris ses interactions avec son environnement). Cependant, il a été avancé que cette approche n'est pas viable pour les systèmes autonomes qui apprennent et s'adaptent en cours de fonctionnement. Cette thèse abordera les limites des approches d'assurance existantes en proposant une nouvelle catégorie de techniques d'assurance de la sécurité fondées sur la sécurité qui évaluent et font évoluer en permanence le raisonnement de sécurité, en même temps que le système, afin de fournir une assurance de la sécurité tout au long de son cycle de vie. En d'autres termes, l'assurance de la sécurité sera fournie non seulement au cours du développement et du déploiement initiaux, mais aussi en cours d'exécution, sur la base de données opérationnelles.

Les vulnérabilités logicielles dues à des erreurs de gestion de la mémoire sont parmi les plus faciles à exploiter. Pour empêcher un attaquant d'injecter son propre code arbitraire (shellcode), les systèmes modernes appliquent généralement une prévention de l'exécution des données (DEP), souvent mise en œuvre sous la forme de permissions de segment (Write xor Execute - W^E).
Cependant, des attaques par réutilisation de code sont apparues pour contourner les protections DEP. Grâce à un problème de logique de mémoire, l'attaquant détourne le flux de contrôle du programme cible et enchaîne de petits fragments de code appelés gadgets pour construire le comportement souhaité, par le biais de la programmation orientée retour (ROP) ou de la programmation orientée saut (JOP).
Au cours des dernières années, plusieurs travaux de recherche ont exploré les moyens d'automatiser la construction d'attaques par réutilisation de code à partir d'attaques de base « sur la pile », abaissant ainsi la barrière à ces méthodes avancées. D'autre part, la protection des programmes repose sur divers mécanismes tels qu'une disposition aléatoire de la mémoire (par exemple, la randomisation de la disposition de l'espace d'adressage - ASLR), l'intégrité du flux de contrôle (CFI) ou un mécanisme de protection de la pile (par exemple, Shadow Stack) pour tenir l'attaquant en échec. Certaines de ces protections peuvent toutefois être coûteuses à mettre en œuvre (temps d'exécution, matériel spécialisé, etc.).

L'objectif général de cette thèse est d'améliorer l'état de l'art de la génération automatique d'exploits dans le but d'évaluer la sécurité de la protection contre la réutilisation des codes. Nous suivrons deux tendances :
(1) d'une part, le candidat fera progresser les méthodes d'automatisation de la réutilisation de code, en prenant en compte la connaissance de la protection pour guider la recherche vers des exploits valides uniquement, en coupant proactivement dans l'espace de recherche, et en recherchant des synergies entre le chaînage ROP/JOP et les méthodes de synthèse de programme telles que la synthèse guidée par la syntaxe ou les méthodes de synthèse stochastiques ;
(2) d'autre part, une fois que le potentiel de ces méthodes sera mieux compris, le candidat concevra une défense efficace contre elles, sur la base d'une analyse complète de leurs principales forces et faiblesses.