CyLab Seminar

In Person and Virtual - ET - Hamburg Hall A301

MICHAEL HICKS , Senior Principal Scientist , Amazon Web Services, Professor Emeritus, University of Maryland

Cedar: A language for expressing fast, safe, and fine-grained authorization policies

Cedar is a new open-source authorization policy language, used to express fine-grained permissions on behalf of applications. When an application wishes to authorize an access request, it invokes Cedar's authorization engine which consults its policies to render a decision. Cedar was designed to be ergonomic, fast, safe, and analyzable. Cedar’s simple and intuitive syntax supports common authorization use-cases with easy-to-understand policies. Cedar’s policy structure ensures that access requests can be authorized quickly. Cedar's policy validator leverages optional typing to help policy writers avoid mistakes but not get in their way. 

Cedar's design has been finely balanced to enable a sound and complete logical encoding, which allows analysts to precisely reason about what policies do, e.g., to ensure that when refactoring a set of policies, the authorized permissions do not change. Cedar is built using a high-assurance process we call verification-guided development. Its authorization engine and validator are formally modeled in the Lean proof-enabled programming language. Cedar’s core development team proves safety and security properties about those models in Lean, and runs millions of automated differential tests to check that the implementations of the Cedar authorization engine and validator, written in Rust, agree with the Lean models. Cedar is used by AWS's Amazon Verified Permissions and AWS Verified Access services, and in third-party applications. 

All code, proofs, and tests are open-sourceLearn more about Cedar 


Mike Hicks is a Senior Principal Scientist at Amazon Web Services, and Professor Emeritus at the University of Maryland. His research explores programming languages and security. He is a Fellow of the Association of Computing Machinery (ACM), Editor-in-Chief of Proceedings of the ACM on Programming Languages, and prior Chair of ACM's Special Interest Group on Programming Languages. He co-leads the development of Cedar, the policy language underpinning the new Amazon Verified Permissions authorization service. 

Faculty Host:  Bryan Parno 

In Person and Zoom Participation.  

⇒  CyLab seminar is open only to partners and Carnegie Mellon University faculty, students, and staff.

Event Website:

Add event to Google
Add event to iCal