Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Computational verification of C protocol implementations by symbolic execution

: Aizatulin, M.; Gordon, D.; Jürjens, J.


Association for Computing Machinery -ACM-, Special Interest Group on Security, Audit and Control -SIGSAC-:
CCS 2012, 19th ACM Conference on Computer and Communications Security : October 16-18, 2012, Sheraton Raleigh Hotel, Raleigh, NC, USA
New York: ACM, 2012
ISBN: 978-1-4503-1651-4
Conference on Computer and Communications Security (CCS) <19, 2012, Raleigh/NC>
Fraunhofer ISST ()
security; verification; protocols; symbolic execution; CryptoVerif; computational

We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The new contribution is the second step in which we translate the extracted model to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of the original C implementation. We implement our method and apply it to verify several protocols out of reach of previous work in the symbolic model (using ProVerif), either due to the use of XOR and Diffie-Hellman commitments, or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to target a verifier for the computational model. We successfully verify over 3000 LOC. One example (about 1000 LOC) is independently written and currently in testing phase for industrial deployment; during its analysis we uncovered a vulnerability now fixed by its author.