Automated Cryptographic Analysis for Protocol Implementations

There has been much recent progress in formal methods and tools for cryptography, enabling, in principle, the automated verification of complex security protocols. In practice, however, these methods and tools remain difficult to apply. Often, verification occurs independently of the development process, rather than during design, prototyping, and testing. Also, as the protocol or its implementations evolve, it is difficult to carry over security guarantees from past formal verification. More generally, the verification of a system that uses a given protocol involves more than the cryptographic verification of an abstract model; it may rely as well on more standard analyzes of code (e.g. to ensure memory safety) and system configuration (e.g. to protect a TCB). For these reasons, we are interested in the integration of modern cryptographic verifiers into the arsenal of software testing and verification tools.

Implementations vs Abstract Models Protocol specifications include many details; most (but not all) of them are of no importance for security. In the process of distilling a formal cryptographic model, most of these details are discarded. When is a protocol model oversimplified? In contrast with formal guarantees proved within the model, the relevance of the model relies on the experience of the formalist. The problem is compounded when considering protocol implementations. Thus, inasmuch as possible, we propose to verify detailed protocol implementations and deployments, rather than simplified abstract models. Using automated tools based on sound proof techniques, the details can either be safely erased, or dealt with by brute-force analysis.

From Implementations to Cryptographic Models In recent work, Bhargavan et al. advocate the automatic extraction and verification of cryptographic models from executable code. They verify protocol implementations written in F#, a dialect of ML, by compilation to ProVerif. Their approach relies on sharing as much code as possible between implementations and models: their code differs mostly in the implementation of core cryptographic libraries, which use bitstrings for concrete execution and symbolic terms for verification.
In this work, we rely on these tools, and also experiment with direct computational cryptographic verifications of protocol implementations. For automated verification, we rely on CryptoVerif, Blanchet's recent tool for concrete cryptography. For automated model extraction, we develop a new compiler from protocols coded in F# to CryptoVerif scripts. We thus obtain computational verification results for executable code.

Methodology The picture below outlines our approach to protocol verification. It involves developing, testing, and verifying a small reference implementation of the protocol plus typical applications.

Verification consists of selecting a part of the implementation, writing additional ``verification harness'' code that specifies the attacker model, the cryptographic assumptions, and the target security properties, and then compiling their combination to some automated prover. Inasmuch as the verification toolchain is automated, one can easily re-verify the code base as it evolves.
In our experience, symbolic and computational verifications are complementary. Computational verification is more precise but more difficult to achieve; we obtain results only for the cryptographic core of the protocol implementation. Symbolic verification typically applies to the whole protocol, sometimes even including the application, but does not detect low-level cryptographic errors. Overall, we believe that the overhead of verification is getting affordable, in comparison with design, development, and testing. The next generation of tools could enable their integration in the development process.

Implementing and Verifying TLS

As an extended case study, we consider implementations of TLS, one of the most widely deployed communications protocol. Due to its popularity, many systems embed an implementation of TLS and rely on its security for communications.
As well as being of practical importance, TLS is a well-understood protocol, with a carefully-written, self-contained specification, a series of successive versions, and a large body of related verification work, providing a detailed history of their security concerns and improvements. Also, TLS is not an academic protocol, optimized (or designed) for verification purposes. This sometimes complicates its security analysis, but also provides a good benchmark for assessing verification techniques.

Contributions

• We program a small functional implementation of TLS. Using simple client and server code, we confirm that our TLS implementation can interoperate with mainstream implementations.
• Relying on a combination of recent model-extraction and verification tools, we obtain a range of positive security results, covering both symbolic and computational cryptographic aspects of the protocol. We thus provide security guarantees for code as it is used in typical deployments of TLS.
• To support computational verification, we develop a new tool for extracting cryptographic models from executable code written in F\#, a dialect of ML. We believe this enables the first automated verification of executable code against standard cryptographic assumptions.
• We review known weaknesses in various versions of TLS, and confirm that they are clearly exposed as part of our verification process, for the corresponding weakened variants of TLS.

Papers and Tools

The draft paper Automated Computational Verification for Cryptographic Protocol Implementations describes the FS2CV tool. See also the corresponding files, including the tool and sample verified protocols.

Cryptographically Verified Implementations for TLS presented at ACM CCS 2008. (corresponding long version, slides and files).

Crypto-Verifying Protocol Implementations in ML position paper presented at FCC'07. (corresponding files).

People

Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Eugen Zălinescu.

Related Stuff

FS2PV & Samoa

CryptoVerif