Skip to Main content Skip to Navigation
New interface
Conference papers

Exploration of fault effects on formal RISC-V microarchitecture models

Abstract : This paper introduces a formal workflow for modeling software/hardware systems in order to explore the effects of fault injections and evaluate the robustness to fault injection attacks. We illustrate this workflow on four versions of a PIN authentication code, embedding different software countermeasures. The code is symbolically evaluated on two implementations of the RISC-V CV32E40P core: the original implementation from the OpenHW group and an implementation that integrates protection of the pipeline control signals. On the original, unprotected core, our formal workflow exposes various vulnerabilities, including previously unknown ones, whereas, on the protected core, it confirms the effectiveness of the proposed countermeasures.
Complete list of metadata
Contributor : Contributeur MAP CEA Connect in order to contact the contributor
Submitted on : Monday, November 14, 2022 - 6:30:09 PM
Last modification on : Thursday, November 17, 2022 - 3:37:28 AM


Files produced by the author(s)



Simon Tollec, Mihail Asavoae, Damien Courousse, Karine Heydemann, Mathieu Jan. Exploration of fault effects on formal RISC-V microarchitecture models. FTDC 2022 - Workshop on Fault Detection and Tolerance in Cryptography, Sep 2022, Virtual event, Italy. pp.73-83, ⟨10.1109/FDTC57191.2022.00017⟩. ⟨cea-03852138⟩



Record views


Files downloads