Mid-last year, AWS information security executive Stephen Schmidt unveiled AWS’s open source implementation of SSL/TLS network encryption protocols, dubbed Amazon s2n, a sleek, nimble, and more intuitive means of encrypting a network.
Since then, it has merged more than 100 pull requests from 15 contributors on GitHub (including 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).
One of Amazon’s goals for s2n is to have it seen and used as a proving ground for automated reasoning testing and assurance techniques, before such techniques can be adopted more broadly. The growing supply of compute resources on demand has enabled more rigorous security analysis of each and every code change. To automate this process, Amazon moved away from traditional static analysis and toward integrating analysis steps into the build such that they would be triggered by pull requests and commits.
S2n has also been used as a testbed for tis-interpreter, a static analysis detects use of undefined programming language behavior, and helping to identify and eliminate a series of minor dependencies on implicit compiler behavior. Run-time analysis of s2n also integrates fuzz testing, such that “every change to s2n repositories is run automatically through a libFuzzer-based test,” in order to identify issues that might cause logical errors and other crashes.
Automated formal verification also provides additional security assurances, by proving the outputs of cryptographic operations correct for all potential inputs. The formal verification is built into Amazon’s public GitHub builds to occur on every change. Finally Amazon has announced that it already formally verified its HMAC implementation (an algorithm critical to TLS/SSL encryption protocols) and intends to continue verifying foundational algorithms critical to s2n.