[OOPSLA24] Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization

Описание: Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Video, OOPSLA 2024)
Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells
(University of Pennsylvania, USA; Amazon Web Services, USA; Amazon Web Services, USA; Amazon Web Services, USA; Unaffiliated, USA; Amazon Web Services, USA; Amazon Web Services, USA; University of Pennsylvania, USA; Amazon Web Services, USA; University of Maryland, USA; Amazon Web Services, USA; Unaffiliated, USA; Amazon Web Services, USA; Amazon Web Services, USA; Amazon Web Services, USA)

Abstract: 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.

Article: https://doi.org/10.1145/3649835

ORCID: https://orcid.org/0000-0001-9399-9308, https://orcid.org/0000-0003-4358-2963, https://orcid.org/0000-0002-9105-4922, https://orcid.org/0000-0002-9899-6226, https://orcid.org/0000-0002-4880-4150, https://orcid.org/0000-0002-2759-9223, https://orcid.org/0000-0002-2724-0974, https://orcid.org/0000-0003-2749-797X, https://orcid.org/0000-0002-1273-5990, https://orcid.org/0009-0007-1184-7206, https://orcid.org/0009-0002-4005-1817, https://orcid.org/0000-0003-4814-5148, https://orcid.org/0000-0001-5143-8940, https://orcid.org/0000-0002-1155-2711, https://orcid.org/0000-0001-7780-2122

Video Tags: Authorization, Formal models, Policies as code, oopslaa24main-p79-p, doi:10.1145/3649835, orcid:0000-0001-9399-9308, orcid:0000-0003-4358-2963, orcid:0000-0002-9105-4922, orcid:0000-0002-9899-6226, orcid:0000-0002-4880-4150, orcid:0000-0002-2759-9223, orcid:0000-0002-2724-0974, orcid:0000-0003-2749-797X, orcid:0000-0002-1273-5990, orcid:0009-0007-1184-7206, orcid:0009-0002-4005-1817, orcid:0000-0003-4814-5148, orcid:0000-0001-5143-8940, orcid:0000-0002-1155-2711, orcid:0000-0001-7780-2122, Artifacts Evaluated — Reusable, Results Reproduced

Presentation at the OOPSLA 2024 conference, October 20–25, 2024, https://2024.splashcon.org/track/spla...
Sponsored by ACM SIGPLAN,