Refereed Conference Publications
-
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann.
in Proceedings of the 24th IEEE Symposium on Computer Security Foundations (CSF'11), pages 3--17. Paris, June 2011.
We describe how to verify security properties of C code for cryptographic protocols by using a general-purpose verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security simply by writing suitable header files and annotations in implementation files, rather than by changing VCC itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.
Tech Report (external link) | Preprint [.pdf] | Sample Code [tar.gz] (under BSD license)
Short slide deck [.pdf] | Full slide deck [.pdf]
Non-Refereed Publications
-
Verifying Cryptographic Code in C: Some Experience and the Csec Challenge, with Mihhail Aizatulin, Andrew D. Gordon and Jan Jürjens.
Invited Paper, FAST, Leuven, September 2011. To appear.
The security of much critical infrastructure depends in part on cryptographic software coded in C, and yet vulnerabilities continue to be discovered in such software. We describe recent progress on checking the security of C code implementing cryptographic software. In particular, we describe projects that combine verification-condition generation and symbolic execution techniques for C, with methods for stating and verifying security properties of abstract models of cryptographic protocols. We illustrate these techniques on C code for a simple two-message protocol.
-
Verifying Authentication Properties of C Security Protocol Code Using General-Purpose Verifiers, with Andrew D. Gordon and Jan Jürjens.
ASA-4, FLoC, Edinburgh, July 2010.
We describe how a general purpose C verifier can be used to verify authentication properties of protocol implementations in a way similar to that of F7. We also give an informal security model, based on an assumed translation of verified C programs into F7 modules.
Extended abstract [.pdf] | Slides [.pdf]
Theses
- Code and Proof Obfuscation, M.Sc. Thesis, supervised by David Pichardie. Thesis [.pdf] | Bibliographic Report [.pdf] (in French)
- Deforestation of Functional Programs, B.Sc. Thesis, supervised by Robin Cockett. Thesis [.pdf]
- Using the syntactic construction of verbs to determine the semantic importance of their complements, undergraduate Thesis, supervised by Mehdi Yousfi-Monod and Augusta Mela. Thesis [.pdf] (in French)