Provable Security Resources

Learn how automated reasoning tools and methods within AWS provide the highest levels of security assurance for the cloud. We also discuss potential future avenues of research and application.

In this industrial case study, we describe a new network troubleshooting analysis used by VPC Reachability Analyzer, an SMT-based network reachability analysis and debugging tool. Our troubleshooting analysis uses a formal model of AWS Virtual Private Cloud (VPC) semantics to identify whether a destination is reachable from a source in a given VPC configuration.

Data center security is a foundational component of security in the cloud. This insight paper describes steps we've taken to provide provable security of boot code, an essential step in establishing the security of any data center.

We describe formal verification of s2n, the open-source TLS implementation used in numerous Amazon services. A key aspect of this proof infrastructure is continuous checking to ensure that properties remain proven during the lifetime of the software. At each change to the code, proofs are automatically reestablished with little to no interaction from developers. We describe the proof itself and the technical decisions that enabled integration into development.

In this industrial case study, we describe a new network reachability reasoning tool called Tiros that uses off-the-shelf automated theorem proving tools to identify network misconfigurations of security vulnerabilities. Tiros is the foundation of a network security analysis feature in Amazon Inspector. Tiros is also used within AWS to automate compliance verification and adherence to security invariants for many AWS services that build on existing AWS networking features.

A properly configured policy is a vital part of an organization's security posture. Policy misconfiguration is one of the leading security concerns of cloud customers. This insight paper dives into Zelkova, a policy analysis engine that can automatically detect entire classes of resource misconfigurations.

At AWS, the security and integrity of your data is our top priority, so we developed SideTrail, a program analysis tool that mathematically verifies the correctness of countermeasures in cryptographic code. Learn more in this insight paper.

This insight paper tells the high -level of story of a technique that AWS security experts have used to prove the correctness of systems.