Cedar & Authorization

Overview

Cedar is a domain-specific language for writing and enforcing authorization policies. You write Cedar policies to say who can do what in your application, which invokes the Cedar authorization engine to allow/deny each user request. Cedar is designed to be:

• Expressive: Rich enough to encode complex authorization requirements
• Fast: Efficient authorization decisions even at cloud scale
• Safe: Type system prevents common policy errors
• Analyzable: Automated reasoning can verify policy properties

Cedar demonstrates how programming language techniques — type systems, formal semantics, verification — can underpin practical, high-assurance security tools. I co-led Cedar’s development (with Emina Torlak) during 2022-2024 while full-time at Amazon Web Services, and I’m still involved today as a Cedar user and maintainer.

Cedar is open-source. You can find its main implementations in Rust and Go, its formal specification and differential testing apparatus, and a variety of examples at https://github.com/cedar-policy/. Join Cedar’s Slack to meet and chat with Cedar developers and users.

Cedar is used in production. Here are several examples:

• Amazon Verified Permissions: AWS’s managed authorization service built on Cedar
• MongoDB: Uses Cedar for authorization in Atlas and other products
• Cloudflare: Deployed for internal authorization decisions
• StrongDM: Startup using Cedar for access management services

Verification-Guided Development (VGD)

Cedar pioneered an approach we call verification-guided development, which combines formal verification, property-based and differential testing, and careful API design to build high-assurance software:

1. Formal specification: Mathematical model of system behavior in Lean
2. Mechanized proofs: Verify critical security properties of Cedar’s design
3. Property-based testing: Use thousands of automatically generated inputs in an attempt to falsify key implementation properties
4. Differential testing: Conformance-test implementations (in Rust and Go) against the formal specification

Key Publications and talks

• Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization: PDF (OOPSLA 2024) Youtube The definitive paper and talk on Cedar’s design, including its type system, semantics, validator, and verification approach.

• How We Built Cedar: A Verification-Guided Approach (ESEC/FSE 2024, Industrial Track) Details on our development methodology and lessons learned building a production security system with formal methods.

• Talk: Amazon’s Formal Methods Journey (DARPA Resilience Meeting, 2025) Presents formal methods as used at Amazon, including Cedar’s use of VGD

Future Directions

• Extending Cedar’s expressiveness while maintaining analyzability
• New analysis capabilities (policy optimization, coverage checking)
• Integration with GenAI for Cedar policy generation and explanation, especially of natural-language policy documents