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:  

Provable security features  |  Provable security resources

How it works

We apply automated reasoning in key service areas such as storage, networking, virtualization, identity, and cryptography. You can see automated reasoning at work in HAQM CodeGuru, HAQM Simple Storage Service (HAQM S3), AWS Identity and Access Management (IAM), HAQM VPC Network Access Analyzer, HAQM VPC Reachability Analyzer, and HAQM Verified Permissions.

HAQM CodeGuru

HAQM CodeGuru Reviewer uses automated reasoning and machine learning to identify critical issues, security vulnerabilities, and hard-to-find bugs during application development. It also provides recommendations to improve code quality.

How it works - HAQM CodeGuru

HAQM S3 Block Public Access

S3 Block Public Access uses automated reasoning to provide controls across an entire AWS account or at the individual HAQM S3 bucket level to help ensure that objects never have public access, now or in the future.

How it works - HAQM S3 Block Public Access

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.

How it works - IAM Access Analyzer

HAQM VPC Network Access Analyzer

HAQM VPC Network Access Analyzer uses automated reasoning to identify reachable paths and validate security invariants in your AWS network.

How it works - VPC Network Access Analyzer

HAQM VPC Reachability Analyzer

HAQM VPC Reachability Analyzer uses automated reasoning to identify feasible paths, and explain infeasible paths, in your AWS network.

How it works - VPC Reachability Analyzer

Build with provable security

HAQM Verified Permissions uses automated reasoning to define fine-grained permissions for application users. HAQM 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.


Explore more of AWS