Paper 2024/247
Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults
Abstract
To assess the robustness of CPU-based systems against fault injection attacks, it is necessary to analyze the consequences of the fault propagation resulting from the intricate interaction between the software and the processor. However, current formal methodologies that combine both hardware and software aspects experience scalability issues, primarily due to the use of bounded verification techniques. This work formalizes the notion of $k$-fault resistant partitioning as an inductive solution to this fault propagation problem when assessing redundancy-based hardware countermeasures to fault injections. Proven security guarantees can then reduce the remaining hardware attack surface to consider in a combined analysis with the software, enabling a full co-verification methodology. As a result, we formally verify the robustness of the hardware lockstep countermeasure of the OpenTitan secure element 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, verify its robustness, and integrate it into the OpenTitan project.
Metadata
- Available format(s)
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- Physical AttacksOpenTitanSecure BootHardwareSoftware
- Contact author(s)
-
simon tollec @ cea fr
vedad hadzic @ iaik tugraz at
nasahlpa @ lowrisc org
mihail asavoae @ cea fr
roderick bloem @ iaik tugraz at
damien courousse @ cea fr
karine heydemann @ thalesgroup com
mathieu jan @ cea fr
stefan mangard @ iaik tugraz at - History
- 2024-02-16: approved
- 2024-02-15: received
- See all versions
- Short URL
- https://ia.cr/2024/247
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2024/247, author = {Simon Tollec and Vedad Hadžić and Pascal Nasahl and Mihail Asavoae and Roderick Bloem and Damien Couroussé and Karine Heydemann and Mathieu Jan and Stefan Mangard}, title = {Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults}, howpublished = {Cryptology ePrint Archive, Paper 2024/247}, year = {2024}, note = {\url{https://eprint.iacr.org/2024/247}}, url = {https://eprint.iacr.org/2024/247} }