Automated Verification of Correctness for Masked Arithmetic Programs

doi:10.1007/978-3-031-37709-9_13

	Automated Verification of Correctness for Masked Arithmetic Programs
	Liu, Mingyang1 ; Song, Fu1,2,3 ; Chen, Taolue 4
	2023
会议录名称	LECTURE NOTES IN COMPUTER SCIENCE (INCLUDING SUBSERIES LECTURE NOTES IN ARTIFICIAL INTELLIGENCE AND LECTURE NOTES IN BIOINFORMATICS)
ISSN	0302-9743
卷号	13966 LNCS
页码	255-280
DOI	10.1007/978-3-031-37709-9_13
摘要	Masking is a widely-used effective countermeasure against power side-channel attacks for implementing cryptographic algorithms. Surprisingly, few formal verification techniques have addressed a fundamental question, i.e., whether the masked program and the original (unmasked) cryptographic algorithm are functional equivalent. In this paper, we study this problem for masked arithmetic programs over Galois fields of characteristic 2. We propose an automated approach based on term rewriting, aided by random testing and SMT solving. The overall approach is sound, and complete under certain conditions which do meet in practice. We implement the approach as a new tool FISCHER and carry out extensive experiments on various benchmarks. The results confirm the effectiveness, efficiency and scalability of our approach. Almost all the benchmarks can be proved for the first time by the term rewriting system solely. In particular, FISCHER detects a new flaw in a masked implementation published in EUROCRYPT 2017. © 2023, The Author(s).
关键词	Digital arithmetic Side channel attack Automated approach Automated verification Cryptographic algorithms Fields of characteristic 2 Galois's fields Power Random testing Side-channel attacks Term rewriting Verification techniques
会议名称	35th International Conference on Computer Aided Verification, CAV 2023
会议地点	Paris, France
会议日期	July 17, 2023 - July 22, 2023
URL	查看原文
收录类别	EI
语种	英语
出版者	Springer Science and Business Media Deutschland GmbH
EI入藏号	20233614672335
EI主题词	Formal verification
EISSN	1611-3349
EI分类号	721.1 Computer Theory, Includes Formal Logic, Automata Theory, Switching Theory, Programming Theory ; 723.5 Computer Applications ; 921.6 Numerical Methods
原始文献类型	Conference article (CA)
文献类型	会议论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/346449
专题	信息科学与技术学院_硕士生信息科学与技术学院_PI研究组_宋富组
通讯作者	Song, Fu
作者单位	1.ShanghaiTech University, Shanghai; 201210, China; 2.Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Beijing; 100190, China; 3.Automotive Software Innovation Center, Chongqing; 400000, China; 4.Birkbeck, University of London, London; WC1E 7HX, United Kingdom
第一作者单位	上海科技大学
通讯作者单位	上海科技大学
第一作者的第一单位	上海科技大学
推荐引用方式 GB/T 7714	Liu, Mingyang,Song, Fu,Chen, Taolue. Automated Verification of Correctness for Masked Arithmetic Programs[C]:Springer Science and Business Media Deutschland GmbH,2023:255-280.