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.
Articles and blogs
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.
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 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 the checking of compliance certi cation and adherence to security invariants for many AWS services that build on existing AWS networking features.
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.
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 Amazon Web Services and used as a foundation by services it provides.
What is AWS Zelkova?
Learn more about AWS Zelkova, a tool that is part of AWS's Provable Security initiative, referring to a collection of automated reasoning technologies that provide higher security assurance for customers. Zelkova is an IAM data governance tool embedded across a variety of AWS services that helps assess IAM policies and their behavior. See how Zelkova automates the assessment of policies by translating IAM policy language into a mathematical model, that can then be used to check key properties of policies.
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
AWS re:Invent 2018: Policy Verification and Enforcement at Scale with AWS
In an ever-growing cloud environment, scaling to a number of accounts can range in the thousands— where edge cases dominate your firm’s spectrum and changes in your environment happen quickly. The Goldman Sachs cloud engineering team finds enforcement of best security practice as a growing concern. With developers managing infrastructure as code (IaC), learn how Goldman Sachs uses distributed serverless logging pipelines and leverages AWS formal verification tools to help enforce access policy in the process. In this session, we cover AWS Config, AWS Lambda, Amazon DynamoDB, and Amazon Simple Notification Service (Amazon SNS) as distributed infrastructure that can help catch security issues early and remediate those that happen unexpectedly.
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. The Automated Reasoning group co-presents with Bridgewater, a customer that has leveraged these technologies to help confirm that security requirements are being met, an assurance not previously available from conventional tools.
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 LogMeIn Automates Governance and Empowers Developers at Scale
In this re:Invent session, 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. We dive deep into LogMeIn’s approach for empowering developers on AWS while also meeting required security controls.
Amazon s2n: Cryptography and Open Source at AWS
Launched in June of 2015, s2n is an AWS open-source implementation of the TLS and SSL network security protocols, which focus on security, simplicity, and performance. With development led by engineers from Amazon EC2, Amazon S3, Amazon CloudFront, and AWS security and cryptography services, s2n is a unique opportunity to observe how we develop and test security and availability for critical software at AWS. Learn how we iterate and code, how we automate software verification beyond the usual code reviews, and how open source works at Amazon.
What It's Like to Work for the AWS Automated Reasoning Group
We talked with engineers and researchers from the Automated Reasoning Group at AWS - https://amzn.to/2Ea1OUj, and learned what they liked about working on their team. Take a look at the interesting projects this team is taking on to help customers achieve provable cloud security!
AWS re:Inforce 2019: Automate Compliance Verification on AWS Using Provable Security
The traditional audit methodology of manually sampling, interviewing, and observing provides limited insight into the adherence of a customer’s cloud environment to common regulatory frameworks. The auditor and customer’s challenge is to generate and evaluate evidence of an entire system’s compliance with specific controls, which becomes increasingly difficult with larger code bases. The AWS Provable Security initiative applies automated reasoning technology to automatically prove that a customer’s cloud environment meets certain regulatory standards.
AWS re:Inforce 2019: The Evolution of Automated Reasoning Technology at AWS
The Automated Reasoning Group strengthened the foundations of AWS and provided customers with tools to verify their own security posture. In this session, 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
In this session, 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. Also learn about AWS tools, such as Tiros and Zelkova, that reason with respect to AWS IAM governance and networks, and are setting new standards for how to protect virtualization layers of the cloud. Further, Byron discusses how these technologies can help customers remain secure both today and in the future.