Proving the correctness of AWS authorization
summary
AWS replaces its IAM authorization engine with a formally specified, machine-checked implementation called One Billion Times Per Second and proves its semantics using automated reasoning in Dafny. Proofs assert properties like “deny trumps allow,” the implementation is compiled to readable Java, validated via a year of shadow mode comparisons and fuzzing with no mismatches across one quadrillion production authorizations, and the verified engine runs about 65% faster than the previous implementation; Cedar and Amazon Verified Permissions expose the same correctness approach to customers.
AI-written summary · about
chapters (9)
- 0:00Introduction to the project
- 2:42What is automated reasoning?
- 8:38Overview of IAM architecture
- 13:46Defining authorization logic
- 22:59Iterative engine optimization
- 35:44Compilation and code review
- 40:02Validation and shadow mode
- 52:14Performance results
- 55:17Conclusion and Cedar
related talks
01h 02mReasoning about Security of Amazon Web Services
59mFine-grained authorization for apps with Amazon Verified Permissions
41mJourneys to Zero Trust on AWS
57mA first-principles approach: AWS Identity and Access Management (IAM)
53mAchieving End-to-end Security on AWS
01h 08mKeynote
26mThe Power of AWS Tags (Advanced IAM Session)
19mSetting up AWS Verified Access