Verifying and Quantifying Side-channel Resistance of Masked Software Implementations

doi:10.1145/3330392

	Verifying and Quantifying Side-channel Resistance of Masked Software Implementations
	Gao, Pengfei1,3,4 ; Zhang, Jun1,3,4 ; Song, Fu1 ; Wang, Chao 2
	2019-08
发表期刊	ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY
ISSN	1049-331X
EISSN	1557-7392
卷号	28 期号:3
发表状态	已发表
DOI	10.1145/3330392
摘要	Power side-channel attacks, capable of deducing secret data using statistical analysis, have become a serious threat. Random masking is a widely used countermeasure for removing the statistical dependence between secret data and side-channel information. Although there are techniques for verifying whether a piece of software code is perfectly masked, they are limited in accuracy and scalability. To bridge this gap, we propose a refinement-based method for verifying masking countermeasures. Our method is more accurate than prior type-inference-based approaches and more scalable than prior model-counting-based approaches using SAT or SMT solvers. Indeed, our method can be viewed as a gradual refinement of a set of type-inference rules for reasoning about distribution types. These rules are kept abstract initially to allow fast deduction and then made concrete when the abstract version is not able to resolve the verification problem. We also propose algorithms for quantifying the amount of side-channel information leakage from a software implementation using the notion of quantitative masking strength. We have implemented our method in a software tool and evaluated it on cryptographic benchmarks including AES and MAC-Keccak. The experimental results show that our method significantly outperforms state-of-the-art techniques in terms of accuracy and scalability.
关键词	Differential power analysis perfect masking type inference quantitative masking strength satisfiability modulo theory (SMT) cryptographic software AES MAC-Keccak
收录类别	SCI ; SCIE ; EI
语种	英语
资助项目	U.S. National Science Foundation (NSF)[CNS-1617203]
WOS研究方向	Computer Science
WOS类目	Computer Science, Software Engineering
WOS记录号	WOS:000496205700005
出版者	ASSOC COMPUTING MACHINERY
EI入藏号	20194807768527
EI主题词	Computer software ; Scalability
EI分类号	Computer Software, Data Handling and Applications:723 ; Systems Science:961
WOS关键词	HIGHER-ORDER MASKING ; SECURE ; AES
原始文献类型	Article
引用统计
文献类型	期刊论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/80579
专题	信息科学与技术学院_硕士生信息科学与技术学院_PI研究组_宋富组
通讯作者	Song, Fu
作者单位	1.ShanghaiTech Univ, 393 Middle Huaxia Rd, Shanghai 201210, Peoples R China 2.Univ Southern Calif, 941 Bloom Walk Rd, Los Angeles, CA 90089 USA 3.Univ Chinese Acad Sci, Beijing, Peoples R China 4.Chinese Acad Sci, Shanghai Inst Microsyst & Informat Technol, Beijing, Peoples R China
第一作者单位	上海科技大学
通讯作者单位	上海科技大学
第一作者的第一单位	上海科技大学
推荐引用方式 GB/T 7714	Gao, Pengfei,Zhang, Jun,Song, Fu,et al. Verifying and Quantifying Side-channel Resistance of Masked Software Implementations[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY,2019,28(3).
APA	Gao, Pengfei,Zhang, Jun,Song, Fu,&Wang, Chao.(2019).Verifying and Quantifying Side-channel Resistance of Masked Software Implementations.ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY,28(3).
MLA	Gao, Pengfei,et al."Verifying and Quantifying Side-channel Resistance of Masked Software Implementations".ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 28.3(2019).