CoChat
Sign Up
PreprintCited by 2Access Control and TrustLogic, programming, and type systemsDigital Rights Management and Security

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)

Open access
Cutler, Joseph W., Disselkoen, Craig, Eline, Aaron, He, Shaobo, Headley, Kyle, Hicks, Michael, Hietala, Kesha, Ioannidis, Eleftherios +7 more·2024·arXiv
DOI 10.48550/arxiv.2403.04651arXiv 2403.04651
Open this paper in CoChat — free accountOpen PDF

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.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2403.04651

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 30

  1. David Aspinall. 1994. Subtyping with singleton types. In CSL: International Workshop on Computer Science Logic. 1-15.
  2. John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming. 2018. Semantic-based Automated Reasoning for AWS Access Policies using SMT. In 2018 Formal Methods in Computer Aided Design (FMCAD). 1-9. https://doi.org/10.23919/FMCAD.2018.8602994 · DOI · Paper page
  3. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems -28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 13243), Dana Fisman and Grigore Rosu (Eds.). Springer, 415-442. https://doi.org/10.1007/978-3-030-99524-9_24 · DOI
  4. David Basin, Manuel Clavel, and Marina Egea. 2011. A decade of model-driven security. In Proceedings of the 16th ACM symposium on Access control models and technologies (SACMAT).
  5. Carmine Caserio, Francesca Lonetti, and Eda Marchetti. 2022. A Formal Validation Approach for XACML 3.0 Access Control Policy. Sensors 22, 8 (2022). https://www.mdpi.com/1424-8220/22/8/2984
  6. Karl Crary, David Walker, and Greg Morrisett. 1999. Typed Memory Management in a Calculus of Capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Antonio, Texas, USA) (POPL '99). Association for Computing Machinery, New York, NY, USA, 262-275. https://doi.org/10.1145/ 292540.292564 · DOI
  7. 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. 2024. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Proc. ACM Program. Lang. 8, OOPSLA1 (2024).
  8. Nicodemos Damianou, Naranker Dulay, Emil Lupu, and Morris Sloman. 2001. The Ponder Policy Specification Language. In Policies for Distributed Systems and Networks, Morris Sloman, Emil C. Lupu, and Jorge Lobo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 18-38.
  9. Carolina Dania and Manuel Clavel. 2016. OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints. In Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems. 65-75.
  10. Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. 2001. Complexity and expressive power of logic programming. ACM Computing Surveys (CSUR) 33, 3 (2001), 374-425.
  11. Naranker Dulay, Emil Lupu, Morris Sloman, and Nicodemos Damianou. 2001. A policy deployment model for the Ponder language. In 2001 IEEE/IFIP International Symposium on Integrated Network Management Proceedings. Integrated Network Management VII. Integrated Management Strategies for the New Millennium (Cat. No. 01EX470). IEEE, 529-543.
  12. William Eiers, Ganesh Sankaran, Albert Li, Emily O'Mahony, Benjamin Prince, and Tevfik Bultan. 2022. Quantifying permissiveness of access control policies. In Proceedings of the 44th International Conference on Software Engineering. 1805-1817.
  13. William Eiers, Ganesh Sankaran, Albert Li, Emily O'Mahony, Benjamin Prince, and Tevfik Bultan. 2023. Quacky: Quantitative Access Control Permissivness Analyzer. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering (<conf-loc>, <city>Rochester</city>, <state>MI</state>, <country>USA</country>, </conf-loc>) (ASE '22). Association for Computing Machinery, New York, NY, USA, Article 163, 5 pages. https: //doi.org/10.1145/3551349.3559530 · DOI
  14. David F. Ferraiolo and D. Richard Kuhn. 1992. Role-Based Access Control. In 15th National Computer Security Conference.
  15. K. Fisler, S. Krishnamurthi, L.A. Meyerovich, and M.C. Tschantz. 2005. Verification and change-impact analysis of access-control policies. In Proceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005. 196-205. https://doi.org/10.1109/ICSE.2005.1553562 · DOI
  16. C.A.R. Hoare. 2009. Null References: The Billion Dollar Mistake. Presentation at the QCon conference. https: //www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/
  17. Vincent C. Hu, D. Richard Kuhn, David F. Ferraiolo, and Jeffrey Voas. 2015. Attribute-Based Access Control. Computer 48, 2 (2015), 85-88. https://doi.org/10.1109/MC.2015.33 · DOI · Paper page
  18. Graham Hughes and Tevfik Bultan. 2008. Automated verification of access control policies using a SAT solver. International journal on software tools for technology transfer 10, 6 (2008), 503-520.
  19. Trevor Jim. 2001. SD3: A Trust Management System with Certified Evaluation. In IEEE Symposium on Security and Privacy.
  20. Ninghui Li, John C. Mitchell, and William H. Winsborough. 2005. Beyond proof-of-compliance: security analysis in trust management. J. ACM 52 (2005).
  21. Torsten Lodderstedt, David Basin, and Jürgen Doser. 2002. SecureUML: A UML-based modeling language for model- driven security. In International Conference on the Unified Modeling Language. 426-441.
  22. William M McKeeman. 1998. Differential testing for software. Digital Technical Journal 10, 1 (1998), 100-107.
  23. Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. 2017. Relational Constraint Solving in SMT. In Automated Deduction -CADE 26, Leonardo de Moura (Ed.). Springer International Publishing, Cham, 148-165.
  24. Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction -CADE 28, André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 625-635.
  25. Michał H. Pałka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing an Optimising Compiler by Generating Random Lambda Terms. In Proceedings of the 6th International Workshop on Automation of Software Test.
  26. Ruoming Pang, Ramon Caceres, Mike Burrows, Zhifeng Chen, Pratik Dave, Nathan Germer, Alexander Golynski, Kevin Graney, Nina Kang, Lea Kissner, Jeffrey L. Korn, Abhishek Parmar, Christina D. Richards, and Mengzhi Wang. 2019. Zanzibar: Google's Consistent, Global Authorization System. In 2019 USENIX Annual Technical Conference (USENIX ATC '19). Renton, WA.
  27. Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. 2022. A Formal Foundation for Symbolic Evaluation with Merging. Proc. ACM Program. Lang. 6, POPL, Article 47 (jan 2022), 28 pages. https://doi.org/10.1145/ 3498709 · DOI
  28. Oded Shmueli. 1993. Equivalence of Datalog queries is undecidable. The Journal of Logic Programming 15, 3 (1993), 231-241. https://doi.org/10.1016/0743-1066(93)90040-N · DOI
  29. K Tuncay Tekle and Yanhong A Liu. 2010. Precise complexity analysis for efficient Datalog queries. In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming. 35-44.
  30. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation. 283-294. define maintainer: [user,team#member] or admin define owner: [organization] define reader: [user,team#member] or triager or repo_reader from owner define triager: [user,team#member] or writer define writer: [user,team#member] or maintainer or repo_writer from owner type organization relations define member: [user] or owner define owner: [user] define repo_admin: [user,organization#member] define repo_reader: [user,organization#member] define repo_writer: [user,organization#member]

Cited by

Sorted by citations

Authors
Cutler, J. W., Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., Hietala, K., Ioannidis, E., Kastner, J., Mamat, A., McAdams, D., McCutchen, M., Rungta, N., Torlak, E., & Wells, A.
Affiliations
Amazon (United States) (US)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2024
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2403.04651
arXiv
2403.04651
OpenAlex
W4392617601
Cited by
2
References
0
Citations by year
2025: 1 · 2024: 1
Type
posted content
Language
en
Open access
Licence
Locations
  • arXiv (Cornell University) (submittedVersion, cc-by)
  • arXiv (Cornell University) (cc-by)
Topics
  • Social Sciences › Sociology and Political Science › Access Control and Trust
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Information Systems › Digital Rights Management and Security
Keywords
access control, cedar, policy evaluation, policy verification, policy analysis, role-based access control, attribute-based access control, Lean proof assistant, Rust implementation, policy performance

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review