Paper 2017/1233

Provably secure compilation of side-channel countermeasures

Gilles Barthe, Benjamin Grégoire, and Vincent Laporte


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, and present a general method for proving that compilation preserves software-based side-channel countermeasures. The crux of our method is the notion of 2-simulation, which adapts to our setting the notion of simulation from compiler verification. Using the Coq proof assistant, we verify the correctness of our method and of several representative instantiations.

Available format(s)
Publication info
Preprint. MINOR revision.
constant-timesecure compilation
Contact author(s)
vlaporte @ imdea org
2017-12-22: received
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and Benjamin Grégoire and Vincent Laporte},
      title = {Provably secure compilation of side-channel countermeasures},
      howpublished = {Cryptology ePrint Archive, Paper 2017/1233},
      year = {2017},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.