Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols

Francois Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 2011 IEEE 24th Computer Security Foundations Symposium (CSF)
Number of pages15
DOIs
Publication statusPublished - 11 Aug 2011
EventIEEE Computer Security Foundations Symposium - Cernay-la-Ville, France
Duration: 27 Jun 201129 Jun 2011
Conference number: 24

Publication series

Name
PublisherIEEE
ISSN (Print)1063-6900
ISSN (Electronic)2377-5459

Conference

ConferenceIEEE Computer Security Foundations Symposium
Abbreviated titleCSF2011
Country/TerritoryFrance
CityCernay-la-Ville
Period27/06/1129/06/11

Fingerprint

Dive into the research topics of 'Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols'. Together they form a unique fingerprint.

Cite this