TY - JOUR
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.
N1 - Publisher Copyright:
© 2014 IOS Press and the authors. All rights reserved.
PY - 2014
Y1 - 2014
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.
KW - C implementations
KW - Symbolic cryptography
KW - cryptographic invariants
KW - general-purpose verifiers
KW - program verification
KW - protocol verification
KW - security properties
UR - http://www.scopus.com/inward/record.url?scp=84939641193&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84939641193&partnerID=8YFLogxK
U2 - 10.3233/JCS-140508
DO - 10.3233/JCS-140508
M3 - Article
AN - SCOPUS:84939641193
SN - 0926-227X
VL - 22
SP - 823
EP - 866
JO - Journal of Computer Security
JF - Journal of Computer Security
IS - 5
ER -