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.

翻译：Cedar是一种新型授权策略语言，旨在实现高人体工学性、快速执行、安全可靠及可分析性。开发者无需将授权逻辑嵌入应用程序代码，而是可将该逻辑编写为Cedar策略，并将访问决策委托给Cedar的评估引擎。Cedar简洁直观的语法支持常见授权用例的易读策略，自然融合了基于角色、基于属性和基于关系的访问控制模型概念。其策略结构可快速处理访问请求。策略验证器利用可选类型帮助策略编写者避免错误，同时不增加额外负担。Cedar的设计经过精心平衡，能够实现完整且可靠的逻辑编码，从而支持精准策略分析（例如：重构策略集时确保授权权限不变）。我们已在Lean编程语言中建模Cedar，并利用Lean的证明助手验证了Cedar设计的关键属性。我们以Rust语言实现了Cedar并开源发布。与OpenFGA和Rego两款开源语言相比，（主观上）Cedar的策略可读性相当或更优，（客观上）其性能显著更佳。