Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”

Gilles Barthe (1) , Benjamin Grégoire (2) , Vincent Laporte (3)

1 Institute IMDEA Software [Madrid]
2 MARELLE - Mathematical, Reasoning and Software
3 ENS Cachan Bretagne - École normale supérieure - Cachan, antenne de Bretagne

Software-based countermeasures provide effective mitigation against side-channel attacks, often with minimal efficiency and deployment overheads. Their effectiveness is often amenable to rigorous analysis: specifically, several popular countermeasures can be formalized as information flow policies, and correct implementation of the countermeasures can be verified with state-of-the-art analysis and verification techniques. However , in absence of further justification, the guarantees only hold for the language (source, target, or intermediate representation) on which the analysis is performed. We consider the problem of preserving side-channel countermeasures by compilation for cryptographic "constant-time", a popular countermeasure against cache-based timing attacks. We present a general method, based on the notion of constant-time-simulation, for proving that a compilation pass preserves the constant-time countermeasure. Using the Coq proof assistant, we verify the correctness of our method and of several representative instantiations.

Domaines: Informatique [cs]

Gilles Barthe, Benjamin Grégoire, Vincent Laporte. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. CSF 2018 - 31st IEEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom. ⟨hal-01959560⟩