SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits∗

被引：0
作者：
Tan, Huiyu [1 ,2 ]
Gao, Pengfei [3 ]
Song, Fu [4 ,5 ]
Chen, Taolue [6 ]
Wu, Zhilin [4 ]
机构：
[1] ShanghaiTech University, Shanghai
[2] Wingsemi Technology Co., Ltd., Shanghai
[3] Bytedance, Beijing
[4] Key Laboratory of System Software Chinese Academy of Sciences and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing
[5] Nanjing Institute of Software Technology, Nanjing
[6] Birkbeck, University of London
来源：
IACR Transactions on Cryptographic Hardware and Embedded Systems | 2024年 / 2024卷 / 04期
基金：
中国国家自然科学基金;
关键词：
Cryptographic Circuits; Fault Injection; Formal Verification; SAT;
D O I：
10.46586/tches.v2024.i4.1-39
中图分类号：
学科分类号：
摘要：
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). © 2024, Ruhr-University of Bochum. All rights reserved.
引用
收藏
页码：1 / 39
页数：38
相关论文
共 81 条
[11]  
Bruttomesso Roberto, Cimatti Alessandro, Franzen Anders, Griggio Alberto, Hanna Ziyad, Nadel Alexander, Palti Amit, Sebastiani Roberto, A lazy and layered smt(BV) solver for hard industrial verification problems, Proceedings of the 19th International Conference on Computer Aided Verification (CAV), pp. 547-560, (2007)
[12]  
Burch Jerry R., Clarke Edmund M., Long David E., McMillan Kenneth L., Dill David L., Symbolic model checking for sequential circuit verification, IEEE Trans. Comput. Aided Des. Integr. Circuits Syst, 13, 4, pp. 401-424, (1994)
[13]  
Burch Jerry R., Clarke Edmund M., McMillan Kenneth L., Dill David L., Hwang L. J., Symbolic model checking: 10ˆ20 states and beyond, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS), pp. 428-439, (1990)
[14]  
Barthe Gilles, Dupressoir Francois, Fouque Pierre-Alain, Gregoire Benjamin, Zapalowicz Jean-Christophe, Synthesis of fault attacks on cryptographic implementations, Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, pp. 1016-1027, (2014)
[15]  
Biere Armin, Fazekas Katalin, Fleury Mathias, Heisinger Maximillian, CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020, Proceedings of SAT Competition 2020 – Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pp. 51-53, (2020)
[16]  
Burchard Jan, Gay Mael, Ekossono Ange-Salome Messeng, Horacek Jan, Becker Bernd, Schubert Tobias, Kreuzer Martin, Polian Ilia, Autofault: Towards automatic construction of algebraic fault attacks, Proceedings of the Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC), pp. 65-72, (2017)
[17]  
Breier Jakub, Hou Xiaolu, Liu Yang, Fault attacks made easy: Differential fault analysis automation on assembly code, Cryptology ePrint Archive, (2017)
[18]  
Brayton Robert K., Mishchenko Alan, ABC: an academic industrialstrength verification tool, Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), pp. 24-40, (2010)
[19]  
Bradley Aaron R., Sat-based model checking without unrolling, Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 70-87, (2011)
[20]  
Bryant Randal E., Graph-based algorithms for boolean function manipulation, IEEE Trans. Computers, 35, 8, pp. 677-691, (1986)
123456789