< Retour au sommaire

Soutenance de thèse de Soline Ducousso

Titre: Aller de la sûreté à la sécurité en analyse de code : le modèle d'attaquant

le

Lieu: Amphis 33/34

Suivre en visio

Abstract

Les techniques d’analyse de programme permettent d’éliminer bogues et vulnérabilités logicielles afin d’en améliorer la sûreté et la sécurité, mais elles reposent sur un modèle d’attaquant faible, seulement apte à créer des entrées malicieuses. Cependant, un attaquant avancé peut utiliser une combinaison d’attaques logicielles, micro-architecturales, d’injections de fautes matérielles ou d’attaques matérielles contrôlées par logiciel.

Dans cette thèse, nous formalisons l’atteignabilité d’états du programme violant une propriété de sécurité en présence d’un attaquant avancé et présentons l’exécution symbolique adversariale, technique automatique et efficace pour trouver ces chemins d’attaque. L’explosion d’états est atténuée par un encodage non-branchant des capacités de l’attaquant et deux optimisations. Notre technique montre un gain de performance, en particulier pour un attaquant multi- actions et permet l’exploration de différents scénarios de sécurité.