Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols

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

doi:10.1109/CSF.2011.8

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 proceeding › Conference Contribution (Conference Proceeding)

30 Citations (Scopus)

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 language	English
Title of host publication	Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium (CSF)
Number of pages	15
DOIs	https://doi.org/10.1109/CSF.2011.8
Publication status	Published - 11 Aug 2011
Event	IEEE Computer Security Foundations Symposium - Cernay-la-Ville, France Duration: 27 Jun 2011 → 29 Jun 2011 Conference number: 24

Publication series

Name
Publisher	IEEE
ISSN (Print)	1063-6900
ISSN (Electronic)	2377-5459

Conference

Conference	IEEE Computer Security Foundations Symposium
Abbreviated title	CSF2011
Country/Territory	France
City	Cernay-la-Ville
Period	27/06/11 → 29/06/11

Access to Document

10.1109/CSF.2011.8

Handle.net

Persistent link

30 Citations
1 Article (Academic Journal)

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols
Dupressoir, F., Gordon, A. D., Jürjens, J. & Naumann, D. A., 11 Jul 2014, In: Journal of Computer Security. p. 823-866 44 p.
Research output: Contribution to journal › Article (Academic Journal) › peer-review
15 Citations (Scopus)

Cite this

@inproceedings{e04f724d1c194a2c88b4949b0011e6e5,

title = "Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols",

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.",

author = "Francois Dupressoir and Gordon, \{Andrew D.\} and Jan J{\"u}rjens and Naumann, \{David A.\}",

year = "2011",

month = aug,

day = "11",

doi = "10.1109/CSF.2011.8",

language = "English",

isbn = "978-0-7695-4365-9",

publisher = "IEEE",

booktitle = "Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium (CSF)",

note = "IEEE Computer Security Foundations Symposium, CSF2011 ; Conference date: 27-06-2011 Through 29-06-2011",

}

TY - GEN

T1 - Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols

AU - Dupressoir, Francois

AU - Gordon, Andrew D.

AU - Jürjens, Jan

AU - Naumann, David A.

N1 - Conference code: 24

PY - 2011/8/11

Y1 - 2011/8/11

N2 - 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.

AB - 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.

U2 - 10.1109/CSF.2011.8

DO - 10.1109/CSF.2011.8

M3 - Conference Contribution (Conference Proceeding)

SN - 978-0-7695-4365-9

BT - Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium (CSF)

T2 - IEEE Computer Security Foundations Symposium

Y2 - 27 June 2011 through 29 June 2011

ER -

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols

Abstract

Publication series

Conference

Access to Document

Handle.net

Fingerprint

Research output

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols

Cite this