I am a post-doctoral researcher at IMDEA, under the supervision of Gilles Barthe, and working on proving concrete realizations and implementations of cryptographic primitives and protocols secure.
I was awarded 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.
My current research interests are mainly in the formal verification of imperative programs, with a focus on computational cryptographic security properties.
In the past, I have worked on abstract interpretation and some aspects of programming and natural languages.
A more complete list of my publications is available here.
Synthesis of Fault Attacks on Cryptographic Implementations, with Gilles Barthe, Pierre-Alain Fouque, Benjamin Grégoire and Jean-Christophe Zapalowicz. CCS 2014, to appear.
Making RSA-PSS Secure Against Random Faults, with Gilles Barthe, Benjamin Grégoire, Pierre-Alain Fouque, Mehdi Tibouchi and Jean-Christophe Zapalowicz. CHES 2014, to appear.
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. 22(5):823-866, 2014.
- Certified Computer-Aided Cryptography: Efficient Provably Secure Machine Code from High-Level Implementations, with J. C. Bacelar Almeida, Manuel Barbosa and Gilles Barthe. ACM CCS'13, Berlin, November 2013, pages 1217--1230.