Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)
Proceedings of the ACM on Programming Languages(2024)
摘要
Cedar is a new authorization policy language designed to be ergonomic, fast,
safe, and analyzable. Rather than embed authorization logic in an application's
code, developers can write that logic as Cedar policies and delegate access
decisions to Cedar's evaluation engine. Cedar's simple and intuitive syntax
supports common authorization use-cases with readable policies, naturally
leveraging concepts from role-based, attribute-based, and relation-based access
control models. Cedar's policy structure enables access requests to be decided
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 allow for a sound and complete logical encoding, which
enables precise policy analysis, e.g., to ensure that when refactoring a set of
policies, the authorized permissions do not change. We have modeled Cedar in
the Lean programming language, and used Lean's proof assistant to prove
important properties of Cedar's design. We have implemented Cedar in Rust, and
released it open-source. Comparing Cedar to two open-source languages, OpenFGA
and Rego, we find (subjectively) that Cedar has equally or more readable
policies, but (objectively) performs far better.
更多查看译文
关键词
Authorization,Formal models,Policies as code
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要