Gilles Barthe, IMDEA Software Institute
From 12.00 until 13.30
At ETH Zurich, CNB/F/110
Universitätstrasse 6, 8092 Zurich
Abstract
Cache and differential power analysis attacks are major concerns for cryptographic implementations. Constant-time security and probing security are information flow policies used by practitioners to improve side-channel resistance of their code against cache attacks and DPA attacks respectively. I will present recent work [1,2,3] on rigorous approaches for proving that implementations verify constant-time and probing security.
[1] J. C. Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, and Michael Emmi. Verifying Constant-Time Implementations, USENIX Security 2016.
[2] Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub, Verified Proofs of Higher-Order Masking, EUROCRYPT 2015.
[3] Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, and Rebecca Zucchini, Strong Non-Interference and Type-Directed Higher-Order Masking, ACM CCS 2016.