Proving the Correctness of Amazon’s s2n TLS Library (S31b)
The s2n library is Amazon’s open source implementation of the Transport Layer Security (TLS) protocol. It is “designed to be
simple, small, fast, and with security as a priority”. These attributes make formal analysis of its code, with an eye toward high
assurance of its security, a compelling possibility.
Over the last year and a half, we have constructed proofs of the functional correctness of several components of s2n. These proofs
begin with machine-readable specifications of several components written in Cryptol, a domain-specific language designed to support
high-level description of cryptographic algorithms. We then use our Software Analysis Workbench (SAW) to prove that the C code in s2n has
exactly the same functional behavior as the Cryptol specifications, for all possible inputs.
The verification performed by SAW uses symbolic execution toconstruct a complete functional model of the implementation code, an
approach made possible by the fixed heap layouts and bounded iteration in the targeted components. Once the functional model
exists, SAW automatically states the equivalence between the model and the Cryptol specification as a query for a Satisfiability Modulo
Theories (SMT) solver. The solver can then automatically either conclude that the equivalence is valid or produce a counterexample,
described as a concrete set of input values for which the specification and implementation differ.
We have used this process to show that the s2n implementations of the keyed-Hash Message Authentication Code (HMAC) and Deterministic
Random Bit Generator (DRBG) algorithms, as well as the TLS handshake protocol implementation are all functionally equivalent to their
specifications. In addition, we have proved that the Cryptol description of HMAC is equivalent to a version which was previously
proved to have the expected cryptographic properties using the Coq theorem prover and the Foundational Cryptography Framework (FCF)
library, showing that the s2n version provides the same guarantees.
This talk will outline the techniques underlying the proof and walk through the details of the proved properties. We will also provide an
overview of what attributes may make other systems amenable to similar proof efforts.