We've been surprised in our work in the Csec project 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 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.

This initial version of the repository is launched as part of the University of Edinburgh Microsoft Research Joint Initiative in Informatics, on October 5, 2011, during Rick Rashid's visit to Edinburgh.

Challenge Collections

The challenge is to verify security properties of the source (or binary) code.  The verification results obtained so far include correspondence assertions (for authentication) and secrecy properties.

The csec-protocols collection of benchmark examples is available here:

• Csur: implements the Needham-Schroeder-Lowe protocol; due to Fabrice Parrennes and Jean Goubault-Larrecque in the Csur proiect.
• NSL: implements of the Needham-Schroeder-Lowe protocol; due to Mihhail Aizatulin in the Csec project.
• Simple_hash: implements a single message protocol; due to Mihhail Aizatulin in the Csec project.
• RPC: implements a two-message authenticated RPC; due to Francois Dupressoir in the Csec project.
• RPC-enc: implements a two-message authenticated and encrypted RPC; due to Mihhail Aizatulin in the Csec project. 

The CryptokiX cryptographic codebase is available here:

• CryptokiX: implements a PKCS#11 software token; hosted by the Secgroup of Riccardo Focardi.

Verification Results

We aim here to record known verification results on cryptographic software in C.

• As reported at VMCAI'05, the Csur tools verify the Csur version of NSL from the csec-protocols collection.
• As reported at CSF'09, ASPIER verifies the main loop of OpenSSL (not included here).
• As reported at CSF'11, VCC verifies some examples, including RPC from the csec-protocols collection.
• As reported at CCS'11, the csec-tools symbolic execution tool extracts verifiable models of all five examples from the csec-protocols collection.

Disclaimer

This source code forms a collection of benchmark examples to further research on verification tools; it is not intended for production use.

Related Repositories

There are related repositories with complementary goals:

• SPORE (Security Protocols Open Repository) collects formal descriptions of security protocols, but not implementation code,
• VSR (Verified Software Repository) collects verified software, in general, rather than cryptographic software in particular.