Computationally Sound Verification of Source Code

Michael Backes, Matteo Maffei, and Dominique Unruh.
in ACM CCS 2010, ACM Press, pp. 387-398, October 2010. Preprint on IACR ePrint 2010/416.

Abstract

Increasing attention has recently been given to the formal verification of the source code of cryptographic protocols. The standard approach is to use symbolic abstractions of cryptography that make the analysis amenable to automation. This leaves the possibility of attacks that exploit the mathematical properties of the cryptographic algorithms themselves. In this paper, we show how to conduct the protocol analysis on the source code level (F# in our case) in a computationally sound way, i.e., taking into account cryptographic security definitions.

We build upon the prominent F7 verification framework (Bengtson et al., CSF 2008) which comprises a security type-checker for F# protocol implementations using symbolic idealizations and the concurrent lambda calculus RCF to model a core fragment of F#.

To leverage this prior work, we give conditions under which symbolic security of RCF programs using cryptographic idealizations implies computational security of the same programs using cryptographic algorithms. Combined with F7, this yields a computationally sound, automated verification of F# code containing public-key encryptions and signatures.

For the actual computational soundness proof, we use the CoSP framework (Backes, Hofheinz, and Unruh, CCS 2009). We thus inherit the modularity of CoSP, which allows for easily extending our proof to other cryptographic primitives.

Files available online

This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full, updated or preliminary versions are provided. For access to the official version, follow the "Official version" link to the publishers site.

Slides used in my talks are available upon personal request, as long as you agree not to disseminate them to a wider audience or make them available online. If in doubt, please ask.