Micro-Architectural Challenges in High-Assurance Cryptography
François Dupressoir
Senior Lecturer in Cryptography, University of Bristol
High-Assurance Cryptography aims at developing tools for the verification of cryptographic security on implementations in the presence of side-channels. In this talk, I will present some of its recent achievements—including practical deployments at AWS Labs, and detail some of the challenges that stand in its way—focusing in particular on issues that arise at the increasingly fuzzy boundary between software and hardware. The talk will conclude on a hopeful note, outlining actions software and hardware designers could take to make it possible to understand and analyse (some) cryptographic leakage.
About François Dupressoir
François Dupressoir [0] is head of the Bristol Cryptography Research group, where he conducts research on machine-checked cryptography—formally proving that cryptographic algorithms are secure—and high-assurance cryptographic engineering—formally verifying that cryptographic implementations (at various levels of refinement) are as secure as their specification despite an adversary's ability to gain information through side-channels. He is part of the development team for the EasyCrypt proof assistant, and developed prototype analysers for leakage security (ct-verif, maskVerif), which are deployed on practical, commercial specifications and code. Before Bristol, François was a Lecturer at the University of Surrey, a post-doctoral researcher at the IMDEA Software Institute (Madrid) and a PhD student at the Open University, spending most of his PhD in a Microsoft Research lab.Sponsored by
