Proving Amazon’s s2n correct

In June 2015, Amazon introduced its s2n library, an open-source TLS library that prioritizes simplicity and speed. A stated benefit of this simplicity is ease of auditing and testing. Galois showed that this benefit extends to verifiability by proving the correctness of s2n’s implementations of both the keyed-Hash Message Authentication Code (HMAC) algorithm and the Deterministic Random Bit Generator (DRBG). To construct these proofs, we used Galois’ Software Analysis Workbench (SAW) to show equivalence between specifications written in Galois’ Cryptol language and the C code of s2n.

Once we have proved our Cryptol implementation equivalent to the C program, we are able to do further reasoning using only the more mathematical Cryptol program. We used these techniques in SAW along with help from the Coq theorem prover to relate a more detailed Cryptol implementation to a specification that exactly matches the NIST specification of HMAC. In doing this, we reduced reasoning about the 103 lines of HMAC code to reasoning about 3 lines of Cryptol.

For an in-depth look at the project, the need for verification, what was proven, and how we leveraged formal verification tools to do it, see our series of blog posts on the topic.

Automating formal verification

An essential part of making formal methods useful in industry is making them a part of the process by which software is created at a company. In this project, we have taken steps to integrate and automate the verification process within Amazon’s ecosystem. The automation of SAW works particularly well with a continuous integration approach, running automatically with each code change, and often keeping the proof intact despite changes to the software. We also integrated our tools into the s2n build environment, allowing anyone with the prerequisites installed to run the same proofs on their own version of the s2n code.

In cooperation with Amazon’s Automated Reasoning Group (ARG), we have learned how to report statistics from these automated runs in such away that the useful work that our tools are doing on the code can be understood by those without a formal methods background. This has resulted in a tool that scrapes the continuous integration system, compiling a useful representation of statistics that can be viewed live.