Provably secure compilation of side-channel countermeasures.
- Date : 14/12/2017
- Place : Inria de Paris - 2 rue Simone Iff - 75012 - Paris
- Guest(s) : Vincent Laporte, IMDEA
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.
For more informations
- Time : 15h30
- Place : INRIA de Paris - 2 rue Simone Iff - Salle Lions 2, bâtiment C