ShanghaiTech University Knowledge Management System
Formal Verification of Masking Countermeasures for Arithmetic Programs | |
2022-03-01 | |
发表期刊 | IEEE TRANSACTIONS ON SOFTWARE ENGINEERING |
ISSN | 2326-3881 |
EISSN | 1939-3520 |
卷号 | PP期号:99页码:1 |
发表状态 | 已发表 |
DOI | 10.1109/TSE.2020.3008852 |
摘要 | Cryptographic algorithms are widely used to protect data privacy in many aspects of daily lives. Unfortunately, programs implementing cryptographic algorithms may be vulnerable to practical power side-channel attacks, which may infer private data via statistical analysis. To thwart these attacks, several masking schemes have been proposed, giving rise to effective countermeasures for reducing the statistical correlation between private data and power consumptions. However, programs that rely on secure masking schemes are not secure a priori. Indeed, designing effective masking programs is a labor intensive and error-prone task. Although some techniques have been proposed for formally verifying masking countermeasures and for quantifying masking strength, they are currently limited to Boolean programs and suffer from low accuracy. In this work, we propose an approach for formally verifying masking countermeasures of arithmetic programs. Our approach is more accurate for arithmetic programs and more scalable for Boolean programs comparing to the existing approaches. It is essentially a synergistic integration of type inference and model-counting based methods, armed with domain specific heuristics. The type inference system allows a fast deduction of leakage-freeness of most intermediate computations, the model-counting based methods accounts for completeness, namely, to eliminate spurious flaws, and the heuristics facilitate both type inference and model-counting based reasoning, which improve scalability and efficiency in practice. In case that the program does contain leakage, we provide a method to quantify its masking strength. A distuiguished feature of our type sytem lies in its support of compositonal reasoning when verifying programs with procedure calls, so the need of inlining procedures can be significantly reduced. We have implemented our methods in a verification tool QMVERIF which has been extensively evaluated on cryptographic benchmarks including full AES, DES and MAC-Keccak. The experimental results demonstrate the effectiveness and efficiency of our approach, especially for compositional reasoning. In particular, our tool is able to automatically prove leakage-freeness of arithmetic programs for which only manual proofs exist so far; it is also significantly faster than the state-of-the-art tools: EasyCrypt on common arithmetic programs, QMSINFER, SC Sniffer and maskVerif on Boolean programs. |
关键词 | Cryptography Tools Computational modeling Software algorithms Power demand Cognition |
URL | 查看原文 |
收录类别 | SCI ; EI ; SCIE |
语种 | 英语 |
资助项目 | National Natural Science Foundation of China (NSFC)[61532019,61761136011] ; UK EPSRC[EP/P00430X/1] ; NSFC[61872340] ; Guangdong Science and Technology Department grant[2018B010107004] ; Natural Science Foundation of Guangdong Province, China[2019A1515011689] ; State Key Laboratory of Novel Software Technology, Nanjing University, China[KFKT2018A16] |
WOS研究方向 | Computer Science ; Engineering |
WOS类目 | Computer Science, Software Engineering ; Engineering, Electrical & Electronic |
WOS记录号 | WOS:000769989900015 |
出版者 | IEEE COMPUTER SOC |
原始文献类型 | Early Access Articles |
来源库 | IEEE |
引用统计 | |
文献类型 | 期刊论文 |
条目标识符 | https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/122178 |
专题 | 信息科学与技术学院_本科生 信息科学与技术学院_PI研究组_宋富组 信息科学与技术学院_硕士生 信息科学与技术学院_博士生 |
通讯作者 | Fu Song |
作者单位 | 1.ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai 201210, Peoples R China 2.Chinese Acad Sci, Shanghai Inst Microsyst & Informat Technol, Shanghai 200031, Peoples R China 3.Univ Chinese Acad Sci, Beijing 100049, Peoples R China 4.Shanghai Engn Res Ctr Intelligent Vis & Imaging, Shanghai, Peoples R China 5.Univ Surrey, Dept Comp Sci, Guildford GU2 7XH, Surrey, England 6.Nanjing Univ, State Key Lab Novel Software Technol, Nanjing 210093, Peoples R China |
第一作者单位 | 信息科学与技术学院 |
通讯作者单位 | 信息科学与技术学院 |
第一作者的第一单位 | 信息科学与技术学院 |
推荐引用方式 GB/T 7714 | Gao Pengfei,Xie Hongyi,Pu Sun,et al. Formal Verification of Masking Countermeasures for Arithmetic Programs[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,2022,PP(99):1. |
APA | Gao Pengfei,Xie Hongyi,Pu Sun,Jun Zhang,Fu Song,&Chen, Taolue.(2022).Formal Verification of Masking Countermeasures for Arithmetic Programs.IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,PP(99),1. |
MLA | Gao Pengfei,et al."Formal Verification of Masking Countermeasures for Arithmetic Programs".IEEE TRANSACTIONS ON SOFTWARE ENGINEERING PP.99(2022):1. |
条目包含的文件 | ||||||
文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 |
个性服务 |
查看访问统计 |
谷歌学术 |
谷歌学术中相似的文章 |
[Gao Pengfei]的文章 |
[Xie Hongyi]的文章 |
[Pu Sun]的文章 |
百度学术 |
百度学术中相似的文章 |
[Gao Pengfei]的文章 |
[Xie Hongyi]的文章 |
[Pu Sun]的文章 |
必应学术 |
必应学术中相似的文章 |
[Gao Pengfei]的文章 |
[Xie Hongyi]的文章 |
[Pu Sun]的文章 |
相关权益政策 |
暂无数据 |
收藏/分享 |
修改评论
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。