Write a Blog >>
Fri 24 Jan 2020 15:35 - 15:56 at Ile de France III (IDF III) - Verified & Secure Compilation Chair(s): Andrew Appel

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.

talk (ct-preserv.pdf)1.62MiB

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 16:40
Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew Appel Princeton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine Blazy Univ Rennes- IRISA, Benjamin Gregoire INRIA, Rémi Hutin IRISA / ENS Rennes, Vincent Laporte Inria, David Pichardie Univ Rennes, ENS Rennes, IRISA, Alix Trieu Aarhus University
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Research Papers
Youngju Song Seoul National University, Minki Cho Seoul National University, Dongjoo Kim Seoul National University, Yonghyun Kim Seoul National University, South Korea, Jeehoon Kang KAIST, Chung-Kil Hur Seoul National University
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Research Papers
Timothy Bourke Inria / École normale supérieure, Lélio Brun ENS/Inria, Marc Pouzet École normale supérieure
Link to publication DOI Media Attached File Attached