Simon Tollec
Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France

Vedad Hadžić
Graz University of Technology, Graz, Austria

Pascal Nasahl
Graz University of Technology, Graz, Austria; lowRISC C.I.C., Cambridge, United Kingdom

Mihail Asavoae
Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France

Roderick Bloem
Graz University of Technology, Graz, Austria

Damien Couroussé
Univ. Grenoble Alpes, CEA, List, F-38000, Grenoble, France

Karine Heydemann
Thales DIS, Gémenos, France; Sorbonne Univ., CNRS, LIP6, F-75005, Paris, France

Mathieu Jan
Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France

Stefan Mangard
Graz University of Technology, Graz, Austria

Keywords: Physical Attacks, OpenTitan, Secure Boot, Hardware, Software

Abstract

Fault injection attacks are a serious threat to system security, enabling attackers to bypass protection mechanisms or access sensitive information. To evaluate the robustness of CPU-based systems against these attacks, it is essential to analyze the consequences of the fault propagation resulting from the complex interplay between the software and the processor. However, current formal methodologies combining hardware and software face scalability issues due to the monolithic approach used. To address this challenge, this work formalizes the k-fault-resistant partitioning notion to solve the fault propagation problem when assessing redundancy-based hardware countermeasures in a first step. Proven security guarantees can then reduce the remaining hardware attack surface when introducing the software in a second step. First, we validate our approach against previous work by reproducing known results on cryptographic circuits. In particular, we outperform state-of-the-art tools for evaluating AES under a three-fault-injection attack. Then, we apply our methodology to the OpenTitan secure element and formally prove the security of its CPU’s hardware countermeasure to single bit-flip injections. Besides that, we demonstrate that previously intractable problems, such as analyzing the robustness of OpenTitan running a secure boot process, can now be solved by a co-verification methodology that leverages a k-fault-resistant partitioning. We also report a potential exploitation of the register file vulnerability in two other software use cases. Finally, we provide a security fix for the register file, prove its robustness, and integrate it into the OpenTitan project.