Technical talks
Achieve the highest level of assurance with provable security
Learn how AWS achieves provable security protection at scale. You will hear ingredients of the secret sauce about how automated reasoning helps AWS and AWS customers to achieve the highest level of assurance by providing provable security. You will see how we leverage automated reasoning at AWS to ensure that your data is secure in the cloud and how you can secure your sensitive data and workloads.
AWS re:Inforce 2022 - How Guardian Life Insurance validates IAM policies at scale with AWS
Hear how Guardian Life Insurance empowers builders to experiment and innovate quickly, while minimizing the security risk exposed by granting overly permissive permissions. Guardian validates IAM policies in Terraform templates against AWS best practices and their own security policies by using IAM Access Analyzer and custom policy checks. Learn how Guardian then integrates policy validation into CI/CD pipelines and codifies their exception approval process.
Video playlist
Useful and instructive videos covering a variety of related topics.
Research and insights
Formal Reasoning About the Security of Amazon Web Services
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.
Debugging Network Reachability with Blocked Paths
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.
Model Checking Boot Code from AWS Data Centers
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.
Continuous Formal Verification of Amazon s2n
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.
Reachability Analysis for AWS Based Networks
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.
Semantic-Based Automated Reasoning for AWS Access Policies Using SMT
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.
SideTrail: Verifying Time Balancing of Cryptosystems
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.
Object-Oriented Security Proofs
This insight paper tells the high -level of story of a technique that AWS security experts have used to prove the correctness of systems.
A Solver-Aided Language for Test Input Generation
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 programmers 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.
Practical Methods for Reasoning About Java 8's Functional Programming Features
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 AWS and used as a foundation by services it provides.
Articles and blog posts
Wall Street Journal article: Provable Security for Modern Applications
Neha Rungta, Senior Principal Applied Scientist in the AWS Automated Reasoning Group, writes about how automated reasoning can help companies achieve provable security.
Interested in internships with the AWS Automated Reasoning Group?
Want to solve some of the most challenging cloud security problems?
