Formalization and Analysis of Countermeasures Against Fault Injection Attacks on Open-source Processors

Join our dynamic research team at CEA-List within the DSCIN division for a PhD opportunity in the field of hardware security and formal analysis of processor micro-architectures. The focus of this research is the formalization and analysis of countermeasures against fault injection attacks on open-source processors. Operating at the cutting edge of cyber-security for embedded systems, we aim to build formal guarantees for the robustness of these systems in the face of evolving security threats, particularly those arising from fault injection attacks. As a PhD candidate, you will contribute to advancing the understanding of fault injection attacks and their impact on both hardware and software aspects of open-source processors. The scientific challenge lies in devising methods and tools that can effectively analyze the robustness of embedded systems under fault injection. You will work on jointly considering the RTL model of the target processor and the executed program, addressing the limitations of current methods (be it simulation or formal analysis), and exploring innovative approaches to scale the analysis to larger programs and complex processor microarchitectures. The experimental work will be based on RTL simulators such as Verilator or QuestaSim, the formal analysis tool µARCHIFI developped at CEA-List, and open-source implementations of secured processors such as the RISC-V processor CV32E40S. Upon the successful completion of this PhD thesis, you will have contributed to the development of formalized countermeasures against fault injection attacks. This research not only aligns with the broader goals of enhancing cyber-security for embedded systems but also has practical implications, such as contributing to the security verification of realistic secured architectures. Additionally, your work will pave the way for the design of efficient techniques and tools that have the potential to streamline the evaluation of secured systems, impacting fields like Common Criteria certification and reducing time-to-market during the design phase of secure systems.