About us
Espace utilisateur
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Home   /   Thesis   /   Formalization and Analysis of Countermeasures Against Fault Injection Attacks on Open-source Processors

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

Computer science and software Cyber security : hardware and sofware Engineering sciences Technological challenges


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.


Département Systèmes et Circuits Intégrés Numériques (LIST)
Laboratoire Fonctions Innovantes pour circuits Mixtes
Université Grenoble Alpes
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down