Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks

doi:10.1007/978-3-031-71177-0_13

	Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks
	Tan, Huiyu1,2 ; Yang, Xi1 ; Song, Fu 3,4; Chen, Taolue 5; Wu, Zhilin 3
	2025
会议录名称	FORMAL METHODS, PT II, FM 2024 (IF:0.402[JCR-2005],0.000[5-Year])
ISSN	0302-9743
卷号	14934
页码	189-207
发表状态	已发表
DOI	10.1007/978-3-031-71177-0_13
摘要	Fault injection attack is a class of active, physical attacks against cryptographic circuits. The design and implementation of countermeasures against such attacks are intricate, error-prone and laborious, necessitating formal verification to guarantee their correctness. In this paper, we propose the first compositional verification approach for round-based hardware implementations of cryptographic algorithms. Our approach decomposes a circuit into a set of single-round sub-circuits which are verified individually by either SAT/SMT- or BDD-based tools. Our approach is implemented as an open-source tool CLEAVE, which is evaluated extensively on realistic cryptographic circuit benchmarks. The experimental results show that our approach is significantly more effective and efficient than the state-of-the-art.
关键词	Benchmarking Boolean functions Open source software Compositional verification Cryptographic algorithms CryptoGraphics Design and implementations Error prones Fault injection attacks Hardware implementations Open source tools Physical attacks Sub-circuits
会议名称	26th International Symposium on Formal Methods (FM)
出版地	GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND
会议地点	null,Milan,ITALY
会议日期	SEP 09-13, 2024
URL	查看原文
收录类别	EI ; CPCI-S
语种	英语
资助项目	Strategic Priority Research Program of CAS[XDA0320101] ; National Natural Science Foundation of China[62072309] ; CAS Project for Young Scientists in Basic Research[YSBR-040] ; ISCAS New Cultivation Project[ISCAS-PYFX-202201] ; ISCAS Fundamental Research Project[ISCAS-JCZD-202302] ; State Key Laboratory of Novel Software Technology, Nanjing University[KFKT2023A04]
WOS研究方向	Computer Science ; Mathematics
WOS类目	Computer Science, Software Engineering ; Computer Science, Theory & Methods ; Mathematics, Applied
WOS记录号	WOS:001336896100013
出版者	SPRINGER INTERNATIONAL PUBLISHING AG
EI入藏号	20244017129767
EI主题词	Formal verification
EISSN	1611-3349
EI分类号	1102.1 ; 1106 ; 1106.5 ; 1201.11 ; 1201.8 ; 913.3 Quality Assurance and Control
原始文献类型	Conference article (CA)
文献类型	会议论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/430526
专题	信息科学与技术学院_硕士生
通讯作者	Song, Fu
作者单位	1.ShanghaiTech University, Shanghai; 201210, China 2.Wingsemi Technology Co., Ltd., Shanghai; 201203, China 3.Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing; 100190, China 4.Nanjing Institute of Software Technology, Nanjing; 211135, China 5.Birkbeck, University of London, London; WC1E 7HX, United Kingdom
第一作者单位	上海科技大学
第一作者的第一单位	上海科技大学
推荐引用方式 GB/T 7714	Tan, Huiyu,Yang, Xi,Song, Fu,et al. Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks[C]. GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND:SPRINGER INTERNATIONAL PUBLISHING AG,2025:189-207.