Leading insight and applications from AWS security experts on achieving provable security, the highest level of security assurance, in the cloud
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-absolute 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.
BOOT CODE MODEL CHECKING
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.
PROVING TIME-BALANCING OF CRYPTO SYSTEMS
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.
PROVABLE SECURITY OF RESOURCE POLICIES, AT SCALE
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.
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 re-established with little to no interaction from the developers. We describe the proof itself and the technical decisions that enabled integration into development.
FORMAL REASONING ABOUT AWS
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.
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 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.
Articles and blogs
AWS re:Invent 2016: Automated formal reasoning about AWS systems
Automatic and semiautomatic mechanical theorem provers are now being used within AWS to find proofs in mathematical logic that establish desired properties of key AWS components.
How AWS service teams use Automated Reasoning for security
Neha from the AWS Security Automated Reasoning Group explains how her team built new rules for AWS Config and Amazon Macie. You'll learn about semantics-based reasoning and formal verification techniques, and how we use these at AWS to improve and automate security, both internally and for customers.
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.
Bridgewater Associates discuss the use of ARG tools at AWS Summit in NYC
Bridgewater Associates, the world’s largest hedge fund, operates a fleet of AWS accounts with different levels of information sensitivity and risk tolerance. To manage the risk these discrepancies introduce, Bridgewater developed an automated reasoning process that analyzes security policies and operationalizes them into an automated control validation and response system