Défi technologique : Cybersécurité : hardware et software (en savoir +)
Département : Département Systèmes et Circuits Intégrés Numériques (LIST)
Laboratoire : Laboratoire Fonctions Innovantes pour circuits Mixtes
Date de début : 01-10-2023
Localisation : Grenoble
Code CEA : SL-DRT-23-0526
Contact : damien.courousse@cea.fr
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 Grenoble du CEA, dans un environnement pluridisciplinaire : cyber-sécurité, conception logicielle et matérielle de circuits, intelligence artificielle, etc. Plusieurs séjours sur le centre de Saclay seront prévus pour assurer une étroite collaboration avec l'équipe de recherche qui travaille sur BINSEC, basée sur le centre de Saclay du CEA.
