FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler

Author: Alix Trieu

Paper Information

Title:A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Authors:Alix Trieu
Proceedings:FCS Informal Proceedings
Editors: Charles Morisset and Limin Jia
Keywords:formal verification, Coq proof assistant, constant-time security, timing attacks, CompCert, verified compilation
Abstract:

ABSTRACT. Cryptographic constant-time programming is an established coding discipline used in cryptography to secure programs against timing attacks. Most, if not all, cryptography library try to adhere to this coding style. The C programming language is oftentimes considered a portable assembly, and is hence used by a great number of cryptography libraries. However, what is executed by the hardware is actual assembly, not C. One can thus wonder whether security properties are preserved through compilation as even formally verified compilers only ensure preservation of observable behaviors.

We present in this paper how to derive a natural framework to prove preservation of cryptographic constant-time security from simulation based proofs of compiler correctness. We also give insights on how this could be adapted to CompCert.

Pages:12
Talk:Jul 08 14:00 (Session 40E: Cryptography)
Paper: