News

May 17, 2013 My attack to cast illegitimate votes, control Microsoft accounts and more will appear at Black Hat 2013. Update June 13, 2013: and at WOOT 2013.

March 5, 2013 My paper on miTLS verification has been accepted at IEEE S&P 2013.

Short Bio and Research

I am a post-doctoral researcher in formal methods for security protocols and security-aware applications. My current research project is miTLS, a verified implementation of the TLS security protocol in the computational model of cryptography, via refinement types. I work in the Prosecco research group at INRIA and in the Secure Distributed Computing project at the MSR-INRIA Joint Centre. My main current collaborators are Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss and Pierre-Yves Strub.

I received my PhD in 2010 at Politecnico di Torino, supervised by Riccardo Sisto. During my PhD I co-developed a framework, called spi2java, that allows to semi-automatically generate Java implementations of security protocols formally specified in the spi calculus language.

For half a year, I have been a visiting PhD student at the Microsoft Research Centre, Cambridge, UK, and the Open University, UK, supervised by Jan Jürjens. During my visit, I developed novel formally-based methodologies to design and develop monitors for legacy security protocols implementations.

I am a member of the CryptoForma network, aimed at bridging the gap between symbolic and computational formal methods.