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 条
[1]  
Azarbad Mohammad Reza, Alizadeh Bijan, Scalable smt-based equivalence checking of nested loop pipelining in behavioral synthesis, ACM Trans. Design Autom. Electr. Syst, 22, 2, (2017)
[2]  
Agoyan Michel, Dutertre Jean-Max, Naccache David, Robisson Bruno, Tria Assia, When clocks fail: On critical paths and clock faults, Proceedings of the 9th IFIP WG 8.8/11.2 International Conference (CARDIS), pp. 182-193, (2010)
[3]  
Atzori Luigi, Iera Antonio, Morabito Giacomo, The internet of things: A survey, Comput. Networks, 54, 15, pp. 2787-2805, (2010)
[4]  
Aghaie Anita, Moradi Amir, Rasoolzadeh Shahram, Shahmirzadi Aein Rezaei, Schellenberg Falk, Schneider Tobias, Impeccable circuits, IEEE Transactions on Computers, 69, pp. 361-376, (2020)
[5]  
Audemard Gilles, Simon Laurent, On the glucose SAT solver, International Journal on Artificial Intel ligence Tools, 27, 1, (2018)
[6]  
Arribas Victor, Wegener Felix, Moradi Amir, Nikova Svetla, Cryptographic fault diagnosis using verfi, Proceedings of the IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 229-240, (2020)
[7]  
Baksi Anubhab, Classical and Physical Security of Symmetric Key Cryptographic Algorithms, (2022)
[8]  
Bertoni Guido, Breveglieri Luca, Koren Israel, Maistri Paolo, Piuri Vincenzo, Error analysis and detection procedures for a hardware implementation of the advanced encryption standard, IEEE Trans. Computers, 52, 4, pp. 492-505, (2003)
[9]  
Biere Armin, Cimatti Alessandro, Clarke Edmund M., Fujita Masahiro, Zhu Yunshan, Symbolic model checking using SAT procedures instead of bdds, Proceedings of the 36th Conference on Design Automation (DAC), pp. 317-320, (1999)
[10]  
Biere Armin, Cimatti Alessandro, Clarke Edmund M., Zhu Yunshan, Symbolic model checking without bdds, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 193-207, (1999)
123456789