Provably secure authorization
summary
AWS applies automated reasoning to prove access-control properties end to end, building a proven-correct IAM engine (specs in Dafny, proofs in Lean, implementations in Rust/Java) and an authorization stack for apps with CEDAR and Amazon Verified Permissions. Validation runs shadow authorization against the legacy engine, finds ~100 million mismatches/day early (fixed by addressing millisecond timing and Unicode), validates across a quadrillion samples, and enables aggressive optimizations that cut tail authorization latency by about 65%. Services like S3 Block Public Access, IAM Access Analyzer and VPC Reachability Analyzer use the same approach.
AI-written summary · about
chapters (13)
- 0:00Introduction to provable security
- 7:34Automated reasoning fundamentals
- 12:22Provable security in AWS
- 18:43S3 Block Public Access proof
- 19:47Proven correct IAM authorization
- 24:29Formal specification of IAM
- 32:53Validation of IAM correctness
- 38:06Performance improvements with proofs
- 40:01Introducing CEDAR policy language
- 47:01CEDAR vs IAM differences
- 53:30CEDAR validation and RFC process
- 55:18Verified Permissions service
- 56:02Conclusion and future of authorization
related talks
01h 02mReasoning about Security of Amazon Web Services
59mFine-grained authorization for apps with Amazon Verified Permissions
53mAchieving End-to-end Security on AWS
41mJourneys to Zero Trust on AWS
57mA first-principles approach: AWS Identity and Access Management (IAM)
59mAchieving Zero Trust with AWS application networking
26mThe Power of AWS Tags (Advanced IAM Session)
01h 02mWhy IAM is the new perimeter, and how to govern it