CryptoDB
SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits
| Authors: | |
|---|---|
| Download: | |
| 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 hours). In contrast, the prior approach fails on 31 fault-resistance verification tasks even after 24 hours (per task). |
BibTeX
@article{tches-2024-34456,
title={SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits},
journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
publisher={Ruhr-Universität Bochum},
volume={2024},
pages={1-39},
url={https://tches.iacr.org/index.php/TCHES/article/view/11782},
doi={10.46586/tches.v2024.i4.1-39},
author={Huiyu Tan and Pengfei Gao and Fu Song and Taolue Chen and Zhilin Wu},
year=2024
}