Automated Reasoning and Amazon s2n

In June 2015, AWS Chief Information Security Officer Stephen Schmidt introduced AWS’s new Open Source implementation of the SSL/TLS network encryption protocols, Amazon s2n. s2n is a library that has been designed to be small and fast, with the goal of providing you with network encryption that is more easily understood and fully auditable.

In the 14 months since that announcement, development on s2n has continued, and we have merged more than 100 pull requests from 15 contributors on GitHub. Those active contributors include members of the Amazon S3, Amazon CloudFront, Elastic Load Balancing, AWS Cryptography Engineering, Kernel and OS, and Automated Reasoning teams, as well as 8 external, non-Amazon Open Source contributors.

At the time of the initial s2n announcement, three external security evaluations and penetration tests on s2n had been completed. Those evaluations were code reviews and testing completed by security-focused experts, and came in addition to the code reviews and testing that are applied to every code change at Amazon as standard practice. We have continued to perform such evaluations, and we are pleased to have s2n be the focus of additional analysis from external academic and professional security researchers.

Adding automated reasoning to s2n

Because of s2n’s role as security-critical software, one of our goals is to use s2n as a proving ground for new automated reasoning testing and assurance techniques that we can refine for broader adoption within Amazon and beyond. Increasingly, the availability of compute resources on demand such as Amazon EC2 makes it possible to perform extensive security analysis, even on every code change.

As a first step toward automating security and validation checks, we wanted to move away from traditional static analysis steps involving a manual, developer-triggered process to steps that are integrated into the build and triggered for every GitHub pull request and commit. Our public s2n repository includes automated static analysis of the s2n code using the Open Source LLVM-based scan-build and Cppcheck tools, in addition to other commercial tools AWS runs internally.

Through our participation in the Linux Foundation’s Core Infrastructure Initiative, we have also worked with TrustInSoft to use s2n as a proving ground for a new static analysis tool, tis-interpreter, which detects uses of undefined programming language behavior. By using s2n’s test suite as entry points for runtime analysis, TrustInSoft was able to identify and eliminate a series of minor dependencies on implicit compiler behavior.

We have also extended our run-time analysis of s2n to include integrated fuzz testing. Every change to s2n repositories is run automatically through a libFuzzer-based test, and American fuzzy lop is used for offline testing. Based on analyzing the running code, these tests dynamically generate data inputs that are designed to target and exercise all the modes and options that s2n might encounter. The tests also will find corner cases that could lead to issues causing logical errors, memory leaks, or crashes.

Adding automated formal verification of s2n

These kinds of tests are designed to provide assurance for the security and safety characteristics of the s2n code, but cryptographic code also benefits from formal verification, where the outputs of the cryptographic operations are proven correct for all potential inputs.

Typically, formal verification can be tedious and is performed as research by skilled specialists using mathematical toolsets. As a part of our commitment to automated reasoning, we have contracted with Galois to simplify this process and make it more developer friendly. Combining a domain-specific language called Cryptol and a software analysis tool called SAW, Galois has produced a tool chain that allows us to formally verify important aspects of s2n.

This verification also is built into our public GitHub builds. The verification occurs on every change, and includes negative test cases that “verify the verifier” by deliberately introducing an error into a test-only build and confirming that the tools reject it. The formal specifications required to create the proof are extremely small and readable, and no annotations or changes to the s2n code were necessary to support the proof.

In addition, we have already formally verified s2n’s implementation of HMAC, an important algorithm that is used extensively within the TLS/SSL protocols and elsewhere, and will continue work to verify more of the foundational algorithms used within s2n.

Copy and clone our work

If you want to learn more about s2n integrated testing, would like to use it on your own projects, or are interested in using or contributing to s2n, see our public s2n repository on awslabs.

If you have comments or questions about this blog post, submit them in the “Comments” section below.

-Colm