Paper 2017/1233

Provably secure compilation of side-channel countermeasures

Gilles Barthe, Benjamin Grégoire, and Vincent Laporte

Abstract

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.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint. MINOR revision.
Keywords
constant-timesecure compilation
Contact author(s)
vlaporte @ imdea org
History
2017-12-22: received
Short URL
https://ia.cr/2017/1233
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/1233,
      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{https://eprint.iacr.org/2017/1233}},
      url = {https://eprint.iacr.org/2017/1233}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.