Verifying Implementations of Security Protocols in C
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.
Using General-Purpose Tools to Prove Security Properties
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.
Direct Verification of Security Properties on C code
In a first approach, I worked on directly verifying security properties of C protocol code, such as authentication and (weak) secrecy, without the need for an independent protocol specification. This approach is described informally in a workshop paper, and more formally in this CSF'11 paper. However, this approach causes performance issues, due to the use of first-order logic to describe high-level properties, and to the necessary encoding of the protocol specification as mutable ghost state in the verified program.
T3: Verification of Conformance Properties for Security
To mitigate this issue, I am now working, with Andy Gordon, Bart Jacobs, Cédric Fournet and others, on a domain-specific language to describe security protocols. Our goal is to automatically generate, from a high-level protocol description:
- annotations, used to check, using a general-purpose verifier, that an implementation only sends messages as prescribed by the description,
- and a high-level security model, used to prove that any piece of code that is verified to against those annotations has the intended security properties.
Proving Cryptographic C Programs Secure with General-Purpose Verification Tools, Ph.D. Thesis. The Open University, 2013.
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. Pages 3--17.
Verifying C Implementations of Security Protocols Using a General-Purpose Verifier, with Andrew D. Gordon and Jan Jürjens. ASA-4, FLoC, Edinburgh, July 2010. No formal proceedings.
Slides of a short talk at the April 2011 CryptoForma meeting, introducing the ideas behind T3 and conformance verification for security.
Slides of a talk given multiple times, in relation with the CSF'11 paper.
Abstract for the 2010 CRC Ph.D. conference at the Open University, which I was unable to attend.
My first year probation report. [Note: The approach described in this document is not provably sound in general, do not use without considering it carefully, or contacting me to discuss why.]
Slides of a talk given at the École Normale Supérieure de Cachan - Antenne de Bretagne at the beginning of my Ph.D., in January 2009.