Proving Amazon's s2n Correct
Presented as part of the 2017 HCSS conference.
ABSTRACT
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 recently 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.
This talk will address Industrialization of Formal Methods. This is not only because s2n is a commercial product, but because we have taken steps to make our verification of s2n useful within Amazon’s ecosystem. 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. 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.
--
Before starting at Galois in 2015, Joey Dodds was a Ph.D. candidate at Princeton University, working mainly on the VST project doing research around verifying C programs. At Princeton, Joey also researched a logic for conditional information flow, as a candidate method for analyzing information flow in the SPARK Ada toolkit.
During his work as a Master’s student at KSU, Joey worked on Guardol, a programming language for configuring guards, a hardware solution to cross domain security. Specifically, he worked on various analyses for checking the validity of Guardol programs. Joey also contributed to the Kiasan bounded symbolic execution engine, as part of the Sireum project.