Guillaume Bouffard
Researcher in Embedded System Security
Jonah Alle Monne is currently pursuing his PhD, entitled Formalization and Analysis of Countermeasures against Fault Injection Attacks on Open-source Processors, at CEA-LIST. His research, which began in October 2024, is co-supervised by Damien Couroussé from CEA-LIST Grenoble and Mathieu Jan from CEA-LIST Saclay.
Given the increasing involvement of electronic devices in our lives, ensuring their security is becoming essential. The objective of this thesis is the formalization and analysis of countermeasures against fault injection attacks on open-source microprocessors. Operating at the cutting edge of cybersecurity for embedded systems, we aim to build formal guarantees of the robustness of these systems in the face of evolving security threats, particularly those arising from fault injection attacks. This work seeks to advance the understanding of fault injection attacks and their impact on both the hardware and software aspects of open-source processors. The scientific challenge lies in designing methods and tools capable of effectively analyzing the robustness of embedded systems under fault injection. We will jointly consider the RTL model of the target processor and the executed program, addressing the limitations of current methods (whether through simulation or formal analysis) and exploring innovative approaches to adapt the analysis to larger programs and more complex processor microarchitectures. The experimental work will rely on RTL simulators such as Verilator or QuestaSim, the formal analysis tool µARCHIFI developed at CEA-List, and open-source implementations of secure processors such as the RISC-V CV32E40S processor. This project aligns not only with broader objectives of improving embedded system cybersecurity but also has practical implications, such as contributing to the verification of realistic secure architectures.
Synthèse de programmes de caractérisation à partir du RTL pour l’injection de fautes- Journée thématique sur les attaques par injection de fautes (JAIF) (2026) | |
|
Les attaques par injection de fautes représentent une menace importante pour la sécurité des dispositifs embarqués. Bien que leurs effets soient souvent modélisés sous forme de sauts d’instructions ou de corruptions de données, la caractérisation de ces fautes nécessite des programmes capables de mettre en évidence des comportements erronés visibles au niveau logiciel. Cependant, des effets de fautes proviennent d’éléments microarchitecturaux, ce qui les rend difficiles à identifier avec les approches existantes. D’un côté, les analyses au niveau Register Transfer Level (RTL) fournissent des informations fines, mais reposent sur des modèles qui omettent des détails des circuits physiques. De l’autre, la caractérisation empirique permet de capturer des fautes réelles, mais nécessite de nombreuses expérimentations et ne permet souvent pas leur identification précise. Pour combler cette lacune, nous proposons une méthodologie automatisée qui synthétise des programmes de caractérisation conçus pour exposer des modèles de fautes microarchitecturaux précis en utilisant un algorithme de model-checking. Notre méthodologie permet également d’évaluer les modèles de fautes additionnels révélés par ces programmes. Appliquée à deux cœurs de processeurs RISC-V, CV32E40P et Ibex, notre approche synthétise des programmes qui mettent en évidence des fautes de type bit-flip pour environ 70 % des signaux microarchitecturaux, avec deux jours de calcul sur 10 cœurs en parallèle. Pour 25 % des signaux de contrôle du CV32E40P, nous synthétisons des programmes permettant d’attribuer précisément un bit-flip à un signal ciblé. De tels programmes pourraient faciliter l’utilisation de l’injection de fautes pour déduire la disposition des éléments microarchitecturaux et aider à concevoir des contre-mesures plus efficaces. À notre connaissance, ce travail présenté à la conférence IEEE HOST 2026 constitue la première méthodologie systématique de construction de programmes de caractérisation de fautes, marquant une avancée significative par rapport aux approches empiriques. |
|
Synthesis of RTL-based Characterization Programs for Fault Injection- In Proceedings of the IEEE International Symposium on Hardware Oriented Security and Trust (HOST) (2026) | |
|
Fault injection attacks pose a significant threat to the security of embedded devices. While their effects are commonly modeled as instruction skips or data corruption, characterizing these faults requires programs that expose software-visible faulty behavior. However, many fault effects originate from microarchitectural elements, making them difficult to identify using existing approaches. On one hand, Register Transfer Level (RTL) analyses provide fine-grained insights but rely on abstract models that may not fully reflect the physical circuit. On the other hand, empirical characterization captures real faults but requires extensive experimentation and often reveals multiple fault models simultaneously, complicating precise identification. To address this gap, we propose an automated methodology that synthesizes characterization programs specifically designed to expose targeted microarchitectural fault models using a model-checking algorithm. Our methodology also assesses additional fault models revealed by these programs. Applied to two RISC-V processor cores, CV32E40P and Ibex, our methodology synthesizes programs that expose bit-flip faults for approximately 70 % of microarchitectural signals, using two days of computation on 10 parallel cores. For 25 % of the control signals in CV32E40P, we synthesize programs enabling the precise attribution of a bit-flip to a targeted signal. Such programs could facilitate the use of fault injection to deduce the placement of microarchitectural elements and help design more effective countermeasures. To the best of our knowledge, this work represents the first systematic methodology for building fault characterization programs, marking a significant step beyond empirical approaches. |
|