TY - GEN
T1 - Guiding a general-purpose C verifier to prove cryptographic protocols
AU - Dupressoir, François
AU - Gordon, Andrew D.
AU - Jürjens, Jan
AU - Naumann, David A.
PY - 2011
Y1 - 2011
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.
UR - http://www.scopus.com/inward/record.url?scp=80052648343&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80052648343&partnerID=8YFLogxK
U2 - 10.1109/CSF.2011.8
DO - 10.1109/CSF.2011.8
M3 - Conference contribution
AN - SCOPUS:80052648343
SN - 9780769543659
T3 - Proceedings - IEEE Computer Security Foundations Symposium
SP - 3
EP - 17
BT - Proceedings - 24th IEEE Computer Security Foundations Symposium, CSF 2011
T2 - 24th Computer Security Foundations Symposium, CSF 2011
Y2 - 27 June 2010 through 29 June 2010
ER -