SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits
Abstract: Fault injection attacks represent a type of active, physical attack against cryptographic circuits. Various countermeasures have been proposed to thwart such attacks, however, the design and implementation of which are intricate, error-prone, and laborious. The current formal fault-resistance verification approaches are limited in efficiency and scalability. In this paper, we formalize the fault-resistance verification problem and show that it is coNP-complete. We then devise a novel approach for encoding the fault-resistance verification problem as the Boolean satisfiability (SAT) problem so that modern off-the-shelf SAT solvers can be utilized. The approach is implemented in an open-source tool FIRMER which is evaluated extensively on realistic cryptographic circuit benchmarks. The experimental results show that FIRMER is able to verify fault-resistance of almost all (72/76) benchmarks in 3 minutes (the other three are verified in 35 minutes and the hardest one is verified in 4 h.... https://tches.iacr.org/index.php/TCHES/article/view/11782
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Erschienen in
-
SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits ; volume:2024 ; number:4 ; year:2024
IACR transactions on cryptographic hardware and embedded systems ; 2024, Heft 4 (2024)
- Urheber
-
Tan, Huiyu
Gao, Pengfei
Song, Fu
Chen, Taolue
Wu, Zhilin
- DOI
-
10.46586/tches.v2024.i4.1-39
- URN
-
urn:nbn:de:101:1-2409251857450.860353337951
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
15.08.2025, 07:19 MESZ
Datenpartner
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Tan, Huiyu
- Gao, Pengfei
- Song, Fu
- Chen, Taolue
- Wu, Zhilin
Ähnliche Objekte (12)
Differential power-analysis attacks : a practical example for hardware countermeasures protecting cryptographic circuits
Fault attacks and countermeasures
Fault attacks and countermeasures
VLSI circuits for cryptographic authentication
Algorithmic and Protocol Level Countermeasures to Protect Cryptographic Devices
Locking-enabled security analysis of cryptographic circuits
Leakage and Fault Resilience of Cryptographic Implementations
FIVER – Robust verification of countermeasures against fault injections
Fault simulation for asynchronous circuits
Automated Generation of Fault-Resistant Circuits
Automatic methods for protection of cryptographic hardware against fault attacks
On fault modeling for dynamic MOS circuits
Differential power-analysis attacks : a practical example for hardware countermeasures protecting cryptographic circuits
Fault attacks and countermeasures
Fault attacks and countermeasures
VLSI circuits for cryptographic authentication
Algorithmic and Protocol Level Countermeasures to Protect Cryptographic Devices
Locking-enabled security analysis of cryptographic circuits
Leakage and Fault Resilience of Cryptographic Implementations
FIVER – Robust verification of countermeasures against fault injections
Fault simulation for asynchronous circuits
Automated Generation of Fault-Resistant Circuits
Automatic methods for protection of cryptographic hardware against fault attacks
On fault modeling for dynamic MOS circuits
Differential power-analysis attacks : a practical example for hardware countermeasures protecting cryptographic circuits
Fault attacks and countermeasures
Fault attacks and countermeasures
VLSI circuits for cryptographic authentication
Algorithmic and Protocol Level Countermeasures to Protect Cryptographic Devices
Locking-enabled security analysis of cryptographic circuits
Leakage and Fault Resilience of Cryptographic Implementations
FIVER – Robust verification of countermeasures against fault injections
Fault simulation for asynchronous circuits
Automated Generation of Fault-Resistant Circuits
Automatic methods for protection of cryptographic hardware against fault attacks