Contrats HW/SW pour l’analyse de robustesse aux fautes de processeurs open-source // HW/SW Contracts for Security Analysis Against Fault Injection Attacks on Open-source Processors

Cette thèse se concentre sur la cybersécurité des systèmes embarqués, en particulier sur la vulnérabilité des processeurs et des programmes face aux attaques par injection de fautes. Ces attaques perturbent le fonctionnement normal des systèmes, permettant aux attaquants d'exploiter des failles pour accéder à des informations sensibles. Bien que des méthodes formelles aient été développées pour analyser la robustesse des systèmes, elles se limitent souvent à des analyses séparées du matériel et des logiciels, négligeant l'interaction entre les deux.

Le travail proposé vise à formaliser des contrats entre le matériel et le logiciel (HW/SW) spécifiquement pour l'analyse de sécurité contre les injections de fautes. En s'appuyant sur une approche de partitionnement matériel, cette recherche cherche à atténuer les problèmes de scalabilité liés à la complexité des modèles de microarchitecture. Les résultats attendus incluent le développement de techniques et d'outils permettant une vérification efficace de la sécurité des systèmes embarqués, ainsi que la création de contrats qui faciliteront l'évaluation de la conformité des implémentations matérielles et logicielles. Cette approche pourrait également réduire le temps de mise sur le marché des systèmes sécurisés.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

This thesis focuses on the cybersecurity of embedded systems, particularly the vulnerability of processors and programs to fault injection attacks. These attacks disrupt the normal functioning of systems, allowing attackers to exploit weaknesses to access sensitive information. Although formal methods have been developed to analyze the robustness of systems, they often limit their analyses to hardware or software separately, overlooking the interaction between the two.

The proposed work aims to formalize hardware/software (HW/SW) contracts specifically for security analysis against fault injection. Building on a hardware partitioning approach, this research seeks to mitigate scalability issues related to the complexity of microarchitecture models. Expected outcomes include the development of techniques and tools for effective security verification of embedded systems, as well as the creation of contracts that facilitate the assessment of compliance for both hardware and software implementations. This approach could also reduce the time-to-market for secure systems.

------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Pôle fr : Direction de la Recherche Technologique
Pôle en : Technological Research
Département : Département Systèmes et Circuits Intégrés Numériques (LIST)
Service : DSCIN
Laboratoire : Laboratoire Fonctions Innovantes pour circuits Mixtes
Date de début souhaitée : 01-10-2025
Ecole doctorale : Mathématiques, Sciences et Technologies de l’Information, Informatique (MSTII)
Directeur de thèse : COUROUSSE Damien
Organisme : CEA
Laboratoire : DRT/DSCIN/DSCIN/LFIM
URL : https://damien.courousse.fr
URL : https://list.cea.fr/en

Public/private mixed funding

Pôle fr : Direction de la Recherche Technologique
Pôle en : Technological Research
Département : Département Systèmes et Circuits Intégrés Numériques (LIST)
Service : DSCIN

Master 2 en informatique ou cyber-sécurité avec une composante méthodes formelles