I am a lecturer in Secure Systems at the University of Surrey. My research revolves around proving cryptographic and side-channel security properties of concrete realizations and implementations of cryptographic primitives and protocols, in the presence of partial compromise. This involves tackling problems in modelling adversaries and systems, designing and applying proof methodologies and verification tools, and generally finding less tedious ways of verifying complex properties of important (but not vast) quantities of code.
Before this, I was a post-doctoral researcher at the IMDEA Software Institute, working mainly with Gilles Barthe, Pierre-Yves Strub and Benjamin Grégoire (Inria Sophia-Antipolis -- Méditerranée).
Prior to that, I received a Ph.D. from the Open University on the 23rd of April 2013, for my dissertation on "Proving Cryptographic C Programs Secure with General-Purpose Verification Tools". It was written under the supervision of Andy Gordon, Jan Jürjens and Bashar Nuseibeh, and was supported by a Microsoft Research Ph.D. Scholarship. I spent most of my Ph.D. time at the MSR lab in Cambridge.
My current research interests are mainly in the formal verification of imperative programs, with a focus on computational cryptographic security properties and proofs of security in the presence of side-channels and partial compromise.
In the past, I have worked on abstract interpretation and some aspects of programming and natural languages.
OpportunitiesIf you are interested in research positions (including short summer internships) on implementation-aware security proofs, please contact me.
- Program Committees: PROOFS (2014, 2015, 2016); ESSoS (2014)
- Academic Juries:
I was an invited speaker at the workshop on Constructive Side-Channel Analysis and Secure Design 2016.
Selected PublicationsFor the full list, see my publications page, on DBLP, or Google Scholar.
Strong Non-Interference and Type-Directed Higher-Order Masking, with Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub and Rebecca Zucchini. ACM CCS 2016.
Verifying Constant-Time Implementations, with J. C. Bacelar Almeida, Manuel Barbosa, Gilles Barthe and Michael Emmi. USENIX Security 2016.
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC, with J. C. Bacelar Almeida, Manuel Barbosa and Gilles Barthe. FSE 2016. Best paper award.
Verified Proofs of Higher-Order Masking, with Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire and Pierre-Yves Strub. EuroCrypt 2015.
Synthesis of Fault Attacks on Cryptographic Implementations, with Gilles Barthe, Pierre-Alain Fouque, Benjamin Grégoire and Jean-Christophe Zapalowicz. CCS 2014.
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann. Journal of Computer Security 2014.
Certified Computer-Aided Cryptography: Efficient Provably Secure Machine Code from High-Level Implementations, with J. C. Bacelar Almeida, Manuel Barbosa and Gilles Barthe. CCS 2013.