Journal of Frontiers of Computer Science and Technology ›› 2021, Vol. 15 ›› Issue (6): 1074-1083.DOI: 10.3778/j.issn.1673-9418.2002047

• Science Researches • Previous Articles     Next Articles

SCVerify: Verification of Software Implementation Against Power Side-Channel Attacks

ZHANG Jun   

  1. 1. Shanghai Institute of Microsystem and Information Technology, Chinese Academy of Sciences, Shanghai 200050, China
    2. School of Information Science & Technology, ShanghaiTech University, Shanghai 201210, China
    3. University of Chinese Academy of Sciences, Beijing 100049, China
  • Online:2021-06-01 Published:2021-06-03



  1. 1. 中国科学院 上海微系统与信息技术研究所,上海 200050
    2. 上海科技大学 信息科学与技术学院,上海 201210
    3. 中国科学院大学,北京 100049


Power side-channel attacks, have become a serious threat to embedded computing devices in cyber-physical systems because of the ability of deducing secret data using statistical analysis. A common strategy for designing countermeasures against power-analysis-based side-channel attacks uses random masking techniques to remove the statistical dependency between secret data and side-channel information. Although existing techniques can verify whether a piece of cryptographic software code is perfectly masked, they are limited in accuracy and scalability. In order to eliminate such limitations, a refinement-based method for verifying masking countermeasures is proposed. This method is more accurate than prior type-inference based approaches and more scalable than prior model-counting based approaches using satisfiability (SAT) or satisfiability modulo theories (SMT) solvers. Indeed, this method uses a set of semantic type-inference rules to reason about distribution type. These rules are kept abstract initially to allow fast deduction, and then specified when the abstract version is not able to resolve the verification problem. This method is implemented in a software tool called SCVerify and is evaluated on cryptographic benchmarks including advanced encryption standard (AES) and message authentication code Keccak (MAC-Keccak). The experimental results show that the method significantly outperforms state-of-the-art techniques in terms of accuracy and scalability.

Key words: side channel attack, satisfiability modulo theories (SMT), software verification, type inference, formal verification



关键词: 侧信道攻击, 可满足性模理论(SMT), 软件验证, 类型推导, 形式化验证