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

doi:10.3778/j.issn.1673-9418.2002047

Abstract

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）, 软件验证, 类型推导, 形式化验证

ZHANG Jun. SCVerify: Verification of Software Implementation Against Power Side-Channel Attacks[J]. Journal of Frontiers of Computer Science and Technology, 2021, 15(6): 1074-1083.

张俊. SCVerify：抗功耗侧信道攻击软件实现的验证[J]. 计算机科学与探索, 2021, 15(6): 1074-1083.

References

[1] KOCHER P C. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[C]//LNCS 1109: Pro-ceedings of the 16th Annual International Cryptology Con-ference, Santa Barbara, Aug 18-22, 1996. Berlin, Heidelberg: Springer, 1996: 104-113.
[2] KOCHER P C, JAFFE J, JUN B. Differential power analysis [C]//LNCS 1666: Proceedings of the 19th Annual Interna-tional Cryptology Conference, Santa Barbara, Aug 15-19,1999. Berlin, Heidelberg: Springer, 1999: 388-397.
[3] QUISQUATER J J, SAMYDE D. Electromagnetic analysis (EMA): measures and counter-measures for smart cards[C]// LNCS 2140: International Conference on Research in Smart Cards, Cannes, Sep 19-21, 2001. Berlin, Heidelberg: Springer, 2001: 200-210.
[4] MORADI A, BARENGHI A, KASPER T, et al. On the vul-nerability of FPGA bitstream encryption against power an-alysis attacks: extracting keys from Xilinx Virtex-II FPGAs[C]//Proceedings of the 18th ACM Conference on Computer and Communications Security, Chicago, Oct 17-21, 2011. New York: ACM, 2017: 111-124.
[5] BL?MER J, GUAJARDO J, KRUMMEL V. Provably secure masking of AES[C]//LNCS 3357: Proceedings of the 11th International Workshop on Selected Areas in Cryptography, Waterloo, Aug 9-10, 2004. Berlin, Heidelberg: Springer, 2004: 69-83.
[6] ISHAI Y, SAHAI A, WAGNER D. Private circuits: securing hardware against probing attacks[C]//LNCS 2729: Proceed-ings of the 23rd Annual International Cryptology Conference, Santa Barbara, Aug 17-21, 2003. Berlin, Heidelberg: Spr-inger, 2003: 463-481.
[7] RIVAIN M, PROUFF E. Provably secure higher-order mask-ing of AES[C]//LNCS 6225: Proceedings of the 12th Inter-national Conference on Cryptographic Hardware and Em-bedded Systems, Santa Barbara, Aug 17-20, 2010. Berlin, Heidelberg: Springer, 2010: 413-427.
[8] BAYRAK A G, REGAZZONI F, NOVO D, et al. Sleuth: automated verification of software power analysis counter-measures[C]//LNCS 8086: Proceedings of the 15th Interna-tional Conference on Cryptographic Hardware and Embedded Systems, Santa Barbara, Aug 20-23, 2013. Berlin, Heidelberg: Springer, 2013: 293-310.
[9] MOSS A, OSWALD E, PAGE D, et al. Compiler assisted masking[C]//LNCS 7428: Proceedings of the 14th Interna-tional Conference on Cryptographic Hardware and Embedded Systems, Leuven, Sep 9-12, 2012. Berlin, Heidelberg: Spr-inger, 2012: 58-75.
[10] ELDIB H, WANG C, SCHAUMONT P. Formal verification of software countermeasures against side-channel attacks[J]. ACM Transactions on Software Engineering and Methodo-logy, 2014, 24(2): 11.
[11] ELDIB H, WANG C, SCHAUMONT P. SMT-based verifi-cation of software countermeasures against side-channel att-acks[C]//LNCS 8413: Proceedings of the 20th International Conference on Tools and Algorithms for Construction and Analysis of Systems, Grenoble, Apr 5-13, 2014. Berlin, Heidelberg: Springer, 2014: 62-77.
[12] PROUFF E, RIVAIN M. Masking against side-channel att-acks: a formal security proof[C]//LNCS 7881: Proceedings of the 32nd Annual International Conference on the Theory and Applications of Cryptographic Techniques, Athens, May 26-30, 2013. Berlin, Heidelberg: Springer, 2013: 142-159.
[13] REPARAZ O, BILGIN B, NIKOVA S, et al. Consolidating masking schemes[C]//LNCS 9215: Proceedings of the 35th Annual Cryptology Conference on Advances in Cryptology, Santa Barbara, Aug 16-20, 2015. Berlin, Heidelberg: Spr-inger, 2015: 764-783.
[14] CORON J S. Formal verification of side-channel counter-measures via elementary circuit transformations[C]//LNCS 10892: Proceedings of the 16th International Conference on Applied Cryptography and Network Security, Leuven, Jul 2-4, 2018. Berlin, Heidelberg: Springer, 2018: 65-82.
[15] BARTHE G, BELA?D S, DUPRESSOIR F, et al. Verified proofs of higher-order masking[C]//LNCS 9056: Proceed-ings of the 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Sofia, Apr 26-30, 2015. Berlin, Heidelberg: Springer, 2015: 457-485.
[16] OUAHNA I B E, MEUNIER Q L, HEYDEMANN K, et al. Symbolic approach for side-channel resistance analysis of masked assembly codes[C]//Proceedings of the 6th Interna-tional Workshop on Security Proofs for Embedded Systems, Taiwan, China, Sep 29, 2017: 17-32.
[17] DE MOURA L M, BJ?RNER N. Z3: an efficient SMT solver [C]//LNCS 4963: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Mar 29-Apr 6, 2008. Berlin, Heidelberg: Springer, 2008: 337-340.
[18] BERTONI G, DAEMEN J, PEETERS M, et al. Keccak im-plementation overview[EB/OL]. [2020-02-26]. https://keccak. team/files/Keccak-implementation-3.2.pdf.