Cryptographic code in C, such as security protocols and hardware security modules, is a critical substrate of our software infrastructures. The Csec project aims to develop software analysis techniques to verify and find bugs in such code.
- F. Dupressoir, A. D. Gordon, J. Jürjens, and D. Naumann. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. In 24th IEEE Computer Security Foundations Symposium (CSF 2011), pages 1-17, Cernay-la-Ville, June 27-29, 2011. An extended version appears as Technical Report MSR-TR-2010-50, Microsoft Research, May 2011.
- M. Aizatulin, A. D. Gordon, and J. Jürjens. Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution. In 18th ACM Conference on Computer and Communications Security (CCS 2011), to appear, Chicago, October 17-21, 2011. An extended version appears on arXiv, July 2011. Our model extraction software is available here.
- M. Aizatulin, F. Dupressoir, A. D. Gordon, and J. Jürjens. Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. In Formal Aspects of Security and Trust, Leuven, September 15-16, 2011. An extended version appears as Technical Report MSR-TR-2011-118, Microsoft Research, November 2011.
- M. Aizatulin, A. D. Gordon, and J. Jürjens. Computational Verification of C Protocol Implementations by Symbolic Execution. Submitted for publication, February, 2012. Draft available here.
Launched October 5, 2011: the Csec Challenge
We've been surprised in our work in Csec that there are very few small and readily-available benchmark problems on which to evaluate new verification techniques for C cryptographic code. The aim of the Csec Challenge website is to curate a collection of challenge problems, including source code, intended security properties, and the results obtained by various verification tools. We aim to collect both small benchmark problems and larger widely-deployed codebases.