Refereed Conference Publications
-
Proving Computational Security with a General-Purpose C Verifier, with Cédric Fournet and Andrew D. Gordon.
In submission.
Security protocols and APIs are difficult to specify and implement. A reference or prototype implementation written in C is often the most formal specification at hand. In this paper, we show how general-purpose C verifiers can be used to prove computational security properties, including---for the first time---computational indistinguishability, of protocols and APIs written in C. To do so, we rely on the VCC verifier to prove that the C program has the same observable input-output behaviour as a functional reference implementation written in F#. We then use the F7 type-checker to prove perfect security properties of the reference code assuming ideal cryptographic primitives. Finally, we reduce the security of a probabilistic polynomial-time program that uses concrete cryptographic primitives to the security of the same program using ideal cryptography. We illustrate our method on the implementation of an exemplary key management API, inspired by the next version of the TPM standard.
Details
-
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) | Preprint [.pdf] | Sample Code [tar.gz] | Short slide deck [.pdf] | Full slide deck [.pdf]
Non-Refereed Publications
- Proving Computational Security with a General-Purpose C Verifier, with Cédric Fournet and Andrew D. Gordon. FCC 2012 and ASA-6, Harvard University, June 2012. Talk proposal [.pdf] | Slide Deck [.pptx]
-
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]
Dissertations, Reports and Manuscripts
-
Proving Cryptographic C Programs Secure with General-Purpose Verification Tools, Ph.D. Thesis, supervised by Andrew D. Gordon, Jan Jürjens and Bashar Nuseibeh.
Submitted in September 2012. Examined in February 2013 by Graham Steel and Yijun Yu. Corrections accepted in April 2013. Thesis [.pdf] | Companion Archive [.zip] - 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)