Jonah Alle Monne's PhD Thesis - Formalization and Analysis of Countermeasures against Fault Injection Attacks on Open-source Processors.

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.

Abstract

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.