Provable Security

Security Assurance, Backed by Mathematical Proof

AWS is committed to helping you achieve the highest levels of security in the cloud. Using automated reasoning technology, the application of mathematical logic to help answer critical questions about your infrastructure, AWS is able to detect entire classes of misconfigurations that could potentially expose vulnerable data. We call this provable security that provides higher assurance in security of the cloud and in the cloud.

Find below the latest research and insights into key cloud security challenges of today and the future.

What is Automated Reasoning?

Research and Insights

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.

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.

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.

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 re-established with little to no interaction from the 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 recently introduced network security analysis feature in the Amazon Inspector service now available to millions of customers building applications in the cloud. 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.

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

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

Developing a small but useful set of inputs for tests is challenging. We show that a domain-specific language backed by a constraint solver can help the programmer with this process. The solver can generate a set of test inputs and guarantee that each input is different from other inputs in a way that is useful for testing.

We describe new capabilities added to the Java Modeling Language and the OpenJML deductive program verification tool to support functional programming features introduced in Java 8. We also report on the application of the extensions to a secure streaming protocol library developed by Amazon Web Services and used as a foundation by services it provides.

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. In the case where there is no feasible path, our analysis derives a blocked path: an infeasible but otherwise complete path that would be feasible if a corresponding set of VPC configuration settings were adjusted.


AWS re:Invent 2019: Provable access control-Know who can access your AWS resources

Learn about the evolution of automated reasoning technology at AWS and how it works in the services in which it is embeddeed.

AWS re:Invent 2019: Deep Dive into IAM Access Analyzer

Deep dive into this new capability for security teams and administrators to validate that resource policies only provide the intended public and cross-account access.

AWS re:Invent 2019: Leadership Session-AWS Security

Stephen Schmidt and Neha Rungta address the current state of cloud security, identity and compliance and what's new from AWS Security. 

AWS re:Inforce 2019: The Evolution of Automated Reasoning Technology at AWS

Eric Brandwine and Neha Rungta discuss the evolution of automated reasoning technology at AWS and how it works in the services in which it is embedded, including Amazon S3, AWS Config, and Amazon Macie.

AWS re:Inforce 2019: An AWS Approach to Higher Standards of Assurance w/ Provable Security

Byron Cook talks about the AWS provable security initiative, a collection of automated reasoning technologies that help prove the correctness of key security components both in and of the cloud. 

AWS re:Inforce 2019: Automate Compliance Verification on AWS Using Provable Security

Learn how the AWS Provable Security initiative applies automated reasoning technology to automatically prove that a customer’s cloud environment meets certain regulatory standards.

Bridgewater Associates discuss the use of ARG tools at AWS Summit in NYC

Learn how Bridgewater Associates, the world's largest hedge fund, developed an automated reasoning process that analyzes security policies and operationalizes them into an automated control validation and response system.

AWS re:Invent 2018: Policy Verification and Enforcement at Scale with AWS

With developers managing infrastructure as code (IaC), learn how Goldman Sachs uses distributed serverless logging pipelines and leverages AWS automated reasoning tools to help enforce access policy in the process. 

AWS re:Invent 2018: The Theory and Math Behind Data Privacy and Security

Data privacy and security are top concerns for customers in the cloud. In this session, the AWS Automated Reasoning group shares the advanced technologies, rooted in mathematical proof, that help provide the highest levels of security assurance in today's data-driven world.

How LogMeIn Automates Governance and Empowers Developers at Scale

Learn how LogMeIn moves quickly and stays secure through the power of automation on AWS. We walk through core AWS security building blocks, such as IAM, AWS CloudTrail, AWS Config, and Amazon CloudWatch. 

What is AWS Zelkova?

Learn more about AWS Zelkova, a tool that is part of AWS's Provable Security initiative. Zelkova is an IAM data governance tool embedded across a variety of AWS services that helps assess IAM policies and their behavior.

How AWS service teams use Automated Reasoning for security

Neha from the AWS Security Automated Reasoning Group explains how her team built new automated reasoning rules for AWS Config and Amazon Macie. 

Formal reasoning about the security of Amazon Web Services

Plenary lecture at the Federated Logic Conference, 16 July 2018

AWS re:Invent 2017: AWS CISO Steve Schmidt talks about Zelkova

AWS CISO and VP of Security Steve Schmidt talks about the development and use of formal/constraint-based tools in AWS.

Interested in internships with the AWS Automated Reasoning Group?

Want to solve some of the most challenging cloud security problems?

Contact an AWS Business Representative
Have Questions? Connect with an AWS Business Representative
Exploring security roles?
Apply today »
Want AWS Security updates?
Follow us on Twitter »