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
-
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},
url = {https://eprint.iacr.org/2017/1233}
}
