Verifying Cryptographic Code in C: Some Experience and the Csec Challenge

Mihhail Aizatulin, François Dupressoir, Andrew D. Gordon, Jan Jürjens

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationFormal Aspects of Security and Trust
Subtitle of host publication8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers
PublisherSpringer Berlin Heidelberg
Pages1-20
Number of pages20
Volume7140
ISBN (Electronic)978-3-642-29420-4
ISBN (Print)978-3-642-29419-8
DOIs
Publication statusPublished - 2011

Fingerprint

Dive into the research topics of 'Verifying Cryptographic Code in C: Some Experience and the Csec Challenge'. Together they form a unique fingerprint.

Cite this