### Formal Verification of a Constant-Time Preserving C Compiler

Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu

##### Abstract

Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as ''cryptographic constant-time'', is adopted by several popular cryptographic libraries. This paper focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time? Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C. Concretely, we modify the CompCert compiler to eliminate sources of potential leakage. Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time. Finally, we prove that the modified CompCert compiler preserves constant-time. Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time. These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.

Available format(s)
Category
Implementation
Publication info
Published elsewhere. POPL20
DOI
10.1145/3371075
Keywords
CompilationFormal verificationConstant-time security
Contact author(s)
alix trieu @ cs au dk
History
2019-12-12: last of 2 revisions
See all versions
Short URL
https://ia.cr/2019/926

CC BY

BibTeX

@misc{cryptoeprint:2019/926,
author = {Gilles Barthe and Sandrine Blazy and Benjamin Grégoire and Rémi Hutin and Vincent Laporte and David Pichardie and Alix Trieu},
title = {Formal Verification of a Constant-Time Preserving C Compiler},
howpublished = {Cryptology ePrint Archive, Paper 2019/926},
year = {2019},
doi = {10.1145/3371075},
note = {\url{https://eprint.iacr.org/2019/926}},
url = {https://eprint.iacr.org/2019/926}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.