Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
summary
Cedar defines a concise DSL, a Rust evaluation engine, and a Lean formal model that proves key properties; policies compile into SMT in the sound and complete encoding limited to a decidable fragment so equivalence and counterexamples are decidable. A policy validator with flow‑sensitive capability tracking prevents attribute-access errors. The runtime is poly‑bounded and typically answers requests under 10 micros. AWS ships it in Verified Permissions/Verified Access and the project is open source.
AI-written summary · about
chapters (14)
- 0:00Cedar authorization language
- 1:48Inline authorization problems
- 3:33Why Cedar at AWS
- 4:57Cedar design properties
- 6:40Cedar analyzability focus
- 7:02Cedar syntax and evaluation
- 8:49Cedar policy security
- 10:11Cedar validation and type checking
- 13:02Policy analysis with SMT
- 14:25Cedar performance benchmarks
- 15:49Conclusion and open source
- 16:10Q&A: Cedar vs Daphne and Lean
- 17:34Q&A: Policy synthesis
- 18:38Q&A: DSL design future
related talks
45mNext Generation Authorisation using Cedar
52mAccess management: Customer use of Cedar policy & Verified Permissions
59mProvably secure authorization
30mSecuring Data With Cedar
43mBuilding Authorization with Node.js: Dos and Don’ts
01h 00mCascade - A New High Level SELinux Policy Language
43mApplication Code of Conduct - Full-Stack Policy as Code
59mFine-grained authorization for apps with Amazon Verified Permissions