Preuve dapos;équivalence fonctionnelle de codes binaires pour la sécurisation des programmes embarqués

Description de l'offre : 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 lapos;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 lapos;ajout de contre-mesures au programme cible napos;en modifie pas la fonctionnalité. Cette thèse ciblera le deuxième point : pouvoir apporter des garanties formelles sur la conformité fonctionnelle dapos;un programme sécurisé. Notre approche visera à prouver lapos;é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 dapos;analyse de code binaire développée au CEA List sapos;appuyant sur lapos;état de lapos;art en matière dapos;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 lapos;équipe de développement de BINSEC. Plusieurs séjours sur le centre de Grenoble seront prévus pour assurer une étroite collaboration avec lapos;équipe de développement de COGITO.

Profil du candidat : Master in computer science, with a solid theoretical background.