Post-doc Researcher in Formal Modeling of Clock Glitch Attacks for Security Verification of Processors

The CEA's technology research division (DRT) develop a broad portfolio of technologies in the fields of information and communication, energy and health.CEA technology research division leverages a unique innovation-driven culture and unrivalled expertise to develop and disseminate new technologies for industry, effectively bridging the gap between the worlds of research and industry.CEA-List is a research institute specialized in smart digital systems, located in the heart of the Paris-Saclay science and technology cluster.

Within the DSCIN department of CEA List, the LECA and LFIM laboratories invest R&D efforts in the analysis of the robustness of embedded systems against fault-injection attacks.

The Innovative Functions for Mixed Circuits Laboratory (LFIM) is focused on electronic design and software systems that meet requirements in terms of energy efficiency, size, operating reliability, real-time performance and safety. These systems are used in a wide range of fields, including embedded systems (transport, energy, connected objects), and consumer and professional electronics. The technologies developed within the laboratory draw on the latest advances in nanoelectronics, automation, embedded artificial intelligence and cryptographic acceleration. They respond to the societal challenges of sustainable development and trust in digital systems, while offering new applications made possible by new information and communication technologies. To this end, the LFIM studies, designs and integrates digital and mixed processing architectures on silicon for application needs in the fields of IoT, radio frequency circuits and cyber-physical systems.

Research context.

Embedded processors are increasingly deployed in security-critical applications, making their protection against physical attacks a major challenge. Among these threats, clock glitch attacks remain a powerful and accessible fault injection technique, especially relevant for IoT and embedded systems due to their low-cost implementation.

Recent research at Inria Rennes led to the development of TRAITOR [1-2], an experimental platform capable of generating synchronous clock perturbations and characterizing their impact on processor microarchitectures. These experiments suggest that clock glitches induce sampling faults on sensitive sequential elements, but the corresponding fault models remain to be formally validated.

In parallel, CEA-List has developed µArchiFI [3-4], a formal framework enabling pre-silicon analysis of fault injection effects at RTL level, from hardware implementation details up to software execution. While µArchiFI currently supports fault models representative of laser-based attacks, formal modeling of clock glitch effects remains an open challenge.

Research objective and activities.

The goal of this postdoctoral project is to develop the first formal methodology for analyzing processor robustness against clock glitch attacks by combining experimental characterization of clock glitches and formal verification of their impact. The project will establish a bridge between physical fault injection experiments and formal security verification, enabling rigorous evaluation of hardware/software countermeasures.

The postdoctoral researcher will contribute to the following tasks:

• Formal modeling of clock glitch effects. Develop a discrete fault model suitable for formal verification, based on the Energy Threshold Fault Model (ETFM) and experimental observations. The objective is to represent the effects of clock-induced sampling faults while maintaining the scalability of formal analysis.
• Experimental validation of fault models. Conduct clock glitch injection campaigns (e.g. using the TRAITOR or ChipWhisperer platforms) and compare experimental results with µArchiFI predictions. This iterative approach will refine and validate the formal models
• Security analysis of protected processors. Apply the developed methodology to secure embedded processors such as RISC-V CV32E40S and OpenTitan Secure Ibex. The analysis will identify potential vulnerabilities and evaluate the effectiveness of hardware/software countermeasures against clock glitch attacks.

Research environment.

The researcher will join a joint effort between CEA-List (Grenoble, Saclay) and Inria Rennes (PACAP team), combining expertise in: hardware security, fault injection attacks, processor microarchitecture analysis, formal verification, embedded systems, numerical systems designs. The project builds on complementary developments from both teams: TRAITOR for experimental fault injection and µArchiFI for formal security analysis

References.

[1] Effects of synchronous clock glitch on the security of integrated circuits, A. Marotta, , Theses, Université de Rennes ; RENNES, 2025

[2] Characterizing and Modeling Synchronous Clock-Glitch Fault Injection. A. Marotta, R. Lashermes, G. Bouffard, O. Sentieys, et R. Dafali, . in Constructive Side-Channel Analysis and Secure Design. 2024

[3] µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections. S. Tollec, M. Asavoae, D. Couroussé, K. Heydemann, et M. Jan, . in FMCAD. 2023

[4] Exploration of Fault Effects on Formal RISC-V Microarchitecture Models. S. Tollec, M. Asavoae, D. Couroussé, K. Heydemann, et M. Jan, . in FDTC. 2022

Applicants should hold a PhD in computer science, electrical engineering, embedded systems, or a related field. Strong candidates will have experience in one or more of the following areas:

• hardware security and fault injection attacks,
• formal methods and verification,
• RTL design and digital circuits,
• processor architectures (RISC-V experience is a plus),
• embedded software.

The position offers an opportunity to work at the intersection of hardware security, formal methods, and secure processor design, combining theoretical research with experimental validation.

Location: CEA-List (Grenoble or Paris-Saclay)

Duration: 12 months with possible extensions