About Me
I am a Microsoft Research Ph.D. scholar with the Open University, working on Verifying Implementations of Security Protocols in C under the supervision of Andy Gordon, Jan Jürjens and Bashar Nuseibeh.
My focus has been on guiding existing general-purpose C verification tools (such as VCC, VeriFast or Frama-C) to verify security properties, in a way similar to the initial use of the F7 refinement type system.
I work on the project in parallel with Mihhail Aizatulin, who is focusing on designing and using special-purpose tools to extract and verify protocol models from the target C code.
Research Interests
My current research interests are mainly in the formal verification of imperative programs, with a focus on high-level security properties (authentication, secrecy and information-flow properties), and interactive-theorem proving for verification and security.
I also have some interest in computational security and some aspects of computational soundness.
In the past, I have worked on abstract interpretation, foundational aspects of computer science (category theory, type theory, proof theory and their similarities) and some aspects of programming and natural languages.
Selected Publications
-
A more complete list of my publications, along with their description, is available here.
-
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann. CSF'11, Paris, June 2011. To appear.