A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs

doi:10.1145/3428015

	A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs
	Gao, Pengfei1 ; Xie, Hongyi1 ; Song, Fu1 ; Chen, Taolue 2
	2021-05
发表期刊	ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY (IF:6.6[JCR-2023],6.6[5-Year])
ISSN	1049-331X
EISSN	1557-7392
卷号	30 期号:3
DOI	10.1145/3428015
摘要	Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, in this article, we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. We then give novel model-counting-based and pattern-matching-based methods that are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious. We evaluate our approach on various implementations of arithmetic cryptographic programs. The experiments confirm that our approach outperforms the state-of-the-art baselines in terms of applicability, accuracy, and efficiency.
关键词	Formal verification higher-ordermasking cryptographic programs side-channel attacks
URL	查看原文
收录类别	SCIE ; EI
语种	英语
WOS研究方向	Computer Science
WOS类目	Computer Science, Software Engineering
WOS记录号	WOS:000649478300002
出版者	ASSOC COMPUTING MACHINERY
原始文献类型	Article
引用统计	正在获取...
文献类型	期刊论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/131912
专题	信息科学与技术学院_博士生信息科学与技术学院_PI研究组_宋富组信息科学与技术学院_硕士生
通讯作者	Song, Fu
作者单位	1.ShanghaiTech Univ, Shanghai 201210, Peoples R China; 2.Univ Surrey, Guildford, Surrey, England
第一作者单位	上海科技大学
通讯作者单位	上海科技大学
第一作者的第一单位	上海科技大学
推荐引用方式 GB/T 7714	Gao, Pengfei,Xie, Hongyi,Song, Fu,et al. A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY,2021,30(3).
APA	Gao, Pengfei,Xie, Hongyi,Song, Fu,&Chen, Taolue.(2021).A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs.ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY,30(3).
MLA	Gao, Pengfei,et al."A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs".ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 30.3(2021).