Towards Efficient Verification of Constant-Time Cryptographic Implementations

作     者：Luwei Cai Fu Song Taolue Chen 

作者机构：ShanghaiTech University Shanghai China State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China / University of Chinese Academy of Sciences Beijing China / Nanjing Institute of Software Technology Nanjing China Birkbeck University of London London United Kingdom 

出 版 物：《Proceedings of the ACM on Software Engineering》 

年 卷 期：2024年第1卷第FSE期

页      面：1019-1042页

基　　金：CAS Project for Young Scientists in Basic Research ISCAS New Cultivation Project ISCAS Fundamental Research Project National Natural Science Foundation of China State Key Laboratory of Novel Software Technology, Nanjing University Birkbeck BEI School Project 

主　　题：Timing side-channel constant-time cryptographic implementation formal verification taint analysis 

摘      要：Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software security. Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks, but developing constant-time implementations turns out to be challenging and error-prone. Current verification approaches/tools suffer from scalability and precision issues when applied to production software in practice. In this paper, we put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Specifically, we first use an IFDS-based lightweight taint analysis to prove that a large number of potential (timing) side-channel sources do not actually leak secrets. We then resort to a precise taint analysis and a safety verification approach to determine whether the remaining potential side-channel sources can actually leak secrets. These include novel constructions of taint-directed semi-cross-product of the original program and its Boolean abstraction, and a taint-directed self-composition of the program. Our approach is implemented as a cross-platform and fully automated tool CT-Prover. The experiments confirm its efficiency and effectiveness in verifying real-world benchmarks from modern cryptographic and SSL/TLS libraries. In particular, CT-Prover identify new, confirmed vulnerabilities of open-source SSL libraries (e.g., Mbed SSL, BearSSL) and significantly outperforms the state-of-the-art tools.