Mihhail Aizatulin (Russian: Михаил Айзатулин)
2nd Floor, Jenny Lee Building,
The Open University
Milton Keynes, MK7 6AA
I'm a PhD student at the The Open University supervised by Andrew Gordon, Jan Jürjens and Bashar Nuseibeh. I am working on a static analysis tool for cryptographic security properties of C programs. The aim is to automatically check for violations of secrecy and authentication in protocol implementations like OpenSSL, GnuTLS or Kerberos. François Dupressoir works on the same problem using a different approach.
The current method uses symbolic execution of the C code to extract a model which can then be analysed either in the symbolic setting [AGJ2011] using ProVerif or in the computational setting [AGJ2012] using CryptoVerif. The implementation is available for download.
Computational Verification of C Protocol Implementations by Symbolic Execution (with Andy Gordon and Jan Jürjens), CCS 2012. [pdf]
We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. As in previous work, the first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The new contribution is the second step in which we translate the extracted model to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of the original C implementation. We implement our method and apply it to verify several protocols out of reach of our initial work in the symbolic model, using ProVerif, either due to the use of XOR and Diffie-Hellman commitments, or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to target a verifier for the computational model. We successfully verify over 3000 LOC, more than any prior work on cryptographic code in C. Our largest example, about 1000 LOC, is independently written; during its analysis we uncovered a vulnerability now fixed by its author.
A tutorial paper that illustrates two verification approaches on an extended example.
Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual annotation of source code. First, symbolically execute the C program to obtain symbolic descriptions for the network messages sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyser (ProVerif) to prove security properties or find attacks. We formalise our algorithm and appeal to existing results for ProVerif to establish computational soundness under suitable circumstances. We analyse only a single execution path, so our results are limited to protocols with no significant branching. The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.
Some further materials outlining the approach:
Computationally Sound Analysis of a Probabilistic Contract Signing Protocol (with Henning Schnoor and Thomas Wilke), ESORICS 2009. [pdf], [bib].
We extended the thesis protocol to multiple rounds and made the analysis probabilistic and computational (as opposed to nondeterministic and symbolic in the thesis). To prove security in the computational setting we first prove a general computational soundness result for strategy-based properties.
Diploma Thesis: A Timely and Balanced Optimistic Contract-Signing Protocol, University of Kiel, March 2008.
[pdf], [bib], [src], [slides].
- csec-modex - the implementation of the current C security verification method. Bug reports are very welcome!
- Algorithms and visualisation for automata on infinite words in Haskell, January 2008. [Source code], [Visualisation samples].
- Calysto C static checker by Domagoj Babic [pdf], [src]
- "Loop Invariants on Demand" by K. Rustan M. Leino and Francesco Logozzo [pdf], [src]
- Curriculum Vitae: [pdf], [src].
- I am member of the Cryptoforma network that aims at bringing the computational and the symbolic cryptography communities together.
- I support the Libel Reform Campaign.
Last Updated: 15.02.2012