Title

AWS re:Invent 2022 - Security alchemy: How AWS uses math to prove security (SEC310)

Summary

Bridget Johnson, GM of IAM Access Analyzer, and Neha Roshita, leader of the automated reasoning and identity team, discuss how AWS uses automated reasoning and mathematical proofs to ensure cloud security.
They introduced Zalkova, an internal tool for analyzing access control policies, which led to the development of services and features for customer security assurance.
The talk covered the importance of security controls, such as network controls, access controls, data encryption, and service control policies.
They emphasized the use of automated reasoning to provide comprehensive analysis and provable security, replacing traditional methods like testing and code reviews.
The speakers demonstrated how AWS turns policies and configurations into mathematical formulas, which are then solved using SMT (Satisfiability Modulo Theories) solvers to prove security properties.
They showcased IAM Access Analyzer and VPC Network Access Analyzer, tools that use automated reasoning to identify public and cross-account access, and to verify network configurations.
The talk concluded with a discussion on the shared responsibility model in security and the introduction of Amazon Verified Permissions in preview.

Automated reasoning is a transformative approach to cloud security, providing a higher level of assurance by proving the correctness of configurations mathematically.
AWS's use of automated reasoning internally and externally indicates a commitment to the highest security standards and innovation in security practices.
The introduction of Amazon Verified Permissions suggests AWS is expanding its automated reasoning capabilities to custom resource permissions, potentially offering customers more granular control over their applications' access controls.
The speakers' emphasis on the shared responsibility model highlights the importance of both AWS and its customers in maintaining cloud security.
The use of SMT solvers and the concept of universal statements in automated reasoning demonstrate the complexity and sophistication of AWS's security analysis tools.
The talk's focus on practical demonstrations of security tools like IAM Access Analyzer and VPC Network Access Analyzer provides actionable insights for AWS customers to improve their security posture.