Paper 2026/648

Synthesis of RTL-based Characterization Programs for Fault Injection

Jonah Alle Monne, Univ. Grenoble Alpes, CEA, List, F-38000, Grenoble, France
Guillaume Bouffard, ANSSI
Damien Couroussé, Univ. Grenoble Alpes, CEA, List, F-38000, Grenoble, France
Mathieu Jan, Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France
Abstract

Fault injection attacks pose a significant threat to the security of embedded devices. While their effects are commonly modeled as instruction skips or data corruption, characterizing these faults requires programs that expose software-visible faulty behavior. However, many fault effects originate from microarchitectural elements, making them difficult to identify using existing approaches. On one hand, Register Transfer Level (RTL) analyses provide fine-grained insights but rely on abstract models that may not fully reflect the physical circuit. On the other hand, empirical characterization captures real faults but requires extensive experimentation and often reveals multiple fault models simultaneously, complicating precise identification. To address this gap, we propose an automated methodology that synthesizes characterization programs specifically designed to expose targeted microarchitectural fault models using a model-checking algorithm. Our methodology also assesses additional fault models revealed by these programs. Applied to two RISC-V processor cores, CV32E40P and Ibex, our methodology synthesizes programs that expose bit-flip faults for approximately 70 % of microarchitectural signals, using two days of computation on 10 parallel cores. For 25 % of the control signals in CV32E40P, we synthesize programs enabling the precise attribution of a bit-flip to a targeted signal. Such programs could facilitate the use of fault injection to deduce the placement of microarchitectural elements and help design more effective countermeasures. To the best of our knowledge, this work represents the first systematic methodology for building fault characterization pro- grams, marking a significant step beyond empirical approaches.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. HOST 2026
Keywords
fault injection attacksRTLprocessor microarchitectureprogram synthesisbounded model checking
Contact author(s)
jonah allemonne @ cea fr
Guillaume Bouffard @ ssi gouv fr
damien courousse @ cea fr
mathieu jan @ cea fr
History
2026-04-04: approved
2026-04-02: received
See all versions
Short URL
https://ia.cr/2026/648
License
Creative Commons Attribution-NonCommercial-ShareAlike
CC BY-NC-SA

BibTeX

@misc{cryptoeprint:2026/648,
      author = {Jonah Alle Monne and Guillaume Bouffard and Damien Couroussé and Mathieu Jan},
      title = {Synthesis of {RTL}-based Characterization Programs for Fault Injection},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/648},
      year = {2026},
      url = {https://eprint.iacr.org/2026/648}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.