Provable security
Security assurance, backed by mathematical proof
What is provable security?
We are committed to helping you achieve the highest levels of security in the cloud. We’ve developed automated reasoning tools that use mathematical logic to answer critical questions about your infrastructure to detect misconfigurations that could potentially expose your data. We call this provable security because it provides higher assurance in the security of the cloud and in the cloud.
Learn more:
How automated reasoning helps make AWS products more secure
Learn how the AWS Automated Reasoning Group helps make AWS and other Amazon products more secure. AWS has invested in automated reasoning as a way to provide higher security assurance at scale. Automated reasoning is a sub-field of artificial intelligence; it applies mathematical analysis to better understand complex computer systems or large code bases. Provable security is a collective reference to the tools, features, thought leadership, and community of experts in the automated reasoning field.
Getting started with provable security
We apply automated reasoning in key service areas such as storage, networking, virtualization, identity, and cryptography. You can see provable security at work in Amazon Simple Storage Service (Amazon S3), AWS Identity and Access Management (IAM), Amazon Virtual Private Cloud (VPC), AWS Clean Rooms, and Amazon Verified Permissions.
IAM Access Analyzer
AWS Identity and Access Management (IAM) Access Analyzer uses automated reasoning to analyze all public and cross-account access paths to your resources and provides comprehensive analysis of those paths.
Amazon S3 Block Public Access
S3 Block Public Access uses automated reasoning to provide controls across an entire AWS account or at the individual Amazon S3 bucket level to help ensure that objects never have public access, now or in the future.
Amazon VPC Network Access Analyzer
Amazon VPC Network Access Analyzer uses automated reasoning to identify reachable paths and validate security invariants in your AWS network.
Amazon VPC Reachability Analyzer
Amazon VPC Reachability Analyzer uses automated reasoning to identify feasible paths, and explain infeasible paths, in your AWS network.
AWS Clean Rooms Differential Privacy
AWS Clean Rooms Differential Privacy helps you protect the privacy of your users with mathematically backed and intuitive controls in a few steps.
Build with provable security
Amazon Verified Permissions uses automated reasoning to define fine-grained permissions for application users. Amazon Verified Permissions is a fully managed authorization service that uses the provably correct Cedar policy language, so you can build more secure applications. With Verified Permissions, developers can build applications faster by externalizing authorization and centralizing policy management.
How automated reasoning is strengthening security
Proving the correctness and enhancing performance of IAM
Nitro Isolation Engine formal verification
