La thèse se place dans le contexte de la cyber-sécurité des systèmes
embarqués et des objets connectés, plus particulièrement de leur
sécurisation contre les attaques physiques (attaques par canal
auxiliaire et attaques par injection de fautes).

Le CEA List développe une chaîne de compilation basée sur LLVM,
COGITO, pour l'application automatisée de contre-mesures contre les
attaques physiques. Deux éléments sont cruciaux pour renforcer la
confiance dans la robustesse des contre-mesures appliqués dans les
programmes binaires compilés :
1. la preuve de robustesse des contre-mesures mises en œuvre,
2. la preuve que l'ajout de contre-mesures au programme cible n'en
modifie pas la fonctionnalité.

Cette thèse ciblera le deuxième point : pouvoir apporter des garanties
formelles sur la conformité fonctionnelle d'un programme sécurisé.
Notre approche visera à prouver l'équivalence fonctionnelle du
programme sécurisé à un autre programme de référence, par exemple le même programme mais dépourvu de contre-mesures. Nous
utiliserons BINSEC (https://binsec.github.io), une plate-forme
open-source d'analyse de code binaire développée au CEA List
s'appuyant sur l'état de l'art en matière d'analyse de code binaire et
de méthodes formelles.

La thèse se déroulera sur le centre de Saclay du CEA List (NanoInnov), dans l'équipe de développement de BINSEC.
Plusieurs séjours sur le centre de Grenoble seront prévus pour assurer une étroite
collaboration avec l'équipe de développement de COGITO.