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

SCVerify:抗功耗侧信道攻击软件实现的验证

张俊   

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

Abstract:

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

摘要:

功耗侧信道攻击,通过使用统计分析技术推断出加密算法中的密钥,已成为物理网络设备的一个巨大威胁。随机掩码是一种被广泛使用的用来消除密钥数据和侧信道泄露数据之间关联性的对策。尽管现有技术可以验证加密软件代码是否被随机掩码保护,但是它们在准确性和可扩展性方面受到限制。为消除此类限制,提出了一种基于原有技术改进过的验证随机掩码策略的方法,该方法比已有的基于句法类型的推断技术更准确,比使用SAT(SMT)模型计数的方法更具有可扩展性。实际上,该方法使用一系列语义类型推导规则去推导分布类型,这些规则最初保持抽象以允许快速推导,然后具体化那些抽象规则推导解决不了的验证问题。此类细化方法集成在验证工具SCVerify中,并使用包含AES和MAC-Keccak等加密算法的测试用例进行了验证,实验结果表明此方法在准确性和可扩展性方面明显优于当前的技术。

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