Mike Hicks
Amazon Web Services

Bio: Mike Hicks is a Senior Principal Scientist at Amazon Web Services, and Professor Emeritus at the University of Maryland. His research has looked at applying novel programming languages and program analysis techniques to solve a variety of problems in security, systems, databases, networks, and quantum computing. 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 currently leads a team that works on automated code reasoning and test generation, having until recently co-led the development of Cedar.

Abstract: Cedar is a new open-source authorization policy language, used to express fine-grained permissions on behalf of applications. Rather than embed authorization logic in their application code, developers can write that logic as Cedar policies and delegate access requests to Cedar’s evaluation engine. Cedar is designed to be ergonomic, fast, safe, and analyzable. Cedar’s simple and intuitive syntax supports common authorization use-cases, naturally leveraging concepts from role-based, attribute-based, and relation-based access control models. Cedar’s policy structure ensures that access requests can be authorized quickly. Cedar’s schema-based 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 allow for a sound and complete logical encoding to a decidable first-order theory, which enables precise automated policy analysis, 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 called 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 and services. Cedar’s code, proofs, and tests are open-source at https://github.com/cedar-policy