Formal Modeling of Clock Glitch Attacks for Security Verification of Processors

Mathematics, information, scientific, software Formal Modeling of Clock Glitch Attacks for Security Verification of Processors H/F Research contextEmbedded 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 activitiesThe 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 modelsSecurity 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 environmentThe 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 securi 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 Keywords: Hardware security · Clock glitch attacks · Fault injection · Formal verification · RISC-V · Secure processors · Embedded systems · RTL analysis