Guiding a general-purpose C verifier to prove cryptographic protocols

Issue title: Computer Security Foundations

Guest editors: Michael BackesGuest Editor and Steve ZdancewicGuest Editor

Article type: Research Article

Authors: Dupressoir, François^{a; *} | Gordon, Andrew D.^{b; c} | Jürjens, Jan^d | Naumann, David A.^e

Affiliations: [a] The Open University, Milton Keynes, UK | [b] Microsoft Research, Cambridge, UK | [c] University of Edinburgh, Edinburgh, UK | [d] TU Dortmund and Fraunhofer ISST, Dortmund, Germany | [e] Stevens Institute of Technology, Hoboken, NJ, USA

Correspondence: [*] Corresponding author. E-mail: fdupress@gmail.com.

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.

Keywords: Symbolic cryptography, program verification, C implementations, security properties, general-purpose verifiers, protocol verification, cryptographic invariants

DOI: 10.3233/JCS-140508

Journal: Journal of Computer Security, vol. 22, no. 5, pp. 823-866, 2014