Verifying constant-time implementations by abstract interpretation

Article type: Research Article

Authors: Blazy, Sandrine^{; *} | Pichardie, David | Trieu, Alix

Affiliations: Univ Rennes, Inria, CNRS, IRISA, France

Correspondence: [*] Corresponding author. E-mail: [email protected].

Abstract: Constant-time programming is an established discipline to secure programs against timing attackers. Several real-world secure C libraries such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We propose an advanced static analysis, based on state-of-the-art techniques from abstract interpretation, to report time leakage during programming. To that purpose, we analyze source C programs and use full context-sensitive and arithmetic-aware alias analyses to track the tainted flows. We give semantic evidence of the correctness of our approach on a core language. We also present a prototype implementation for C programs that is based on the CompCert compiler toolchain and its companion Verasco static analyzer. We present verification results on various real-world constant-time programs and report on a successful verification of a challenging SHA-256 implementation that was out of scope of previous tool-assisted approaches.

Keywords: Abstract interpretation, constant-time programming, timing attacks, verification of C implementations

DOI: 10.3233/JCS-181136

Journal: Journal of Computer Security, vol. 27, no. 1, pp. 137-163, 2019