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.
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. |
|