Verifying Implementations of Security Protocols in C

Ph.D. project, under the supervision of Andy Gordon, Jan Jürjens and Bashar Nuseibeh.

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.
We intend for this DSL to be language- and security model-independent, so that it can be used to generate annotations for various C verifiers, as well as JML annotations or F7 refinements, and prove security in different attacker models, from symbolic network attackers to PPT attackers.

Related Material

Publications

Other Material

  • 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, poster and abstract of a talk given at the Open University's Computing department Ph.D. conference in 2009.

  • 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.