REVIEW 5 cited by
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)
read the original 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.
Forward citations
Cited by 5 Pith papers
-
Execution Envelopes: A Shared Admission Contract for Backend AI Execution Requests
Execution envelopes define a shared admission contract for backend AI execution requests to attach unified logging, governance, and policy hooks at entry.
-
PASS: A Provenanced Access Subaccount System for Blockchain Wallets
PASS replaces private-key control in blockchain wallets with provenance tracking, using an Inbox-Outbox mechanism for verifiable lineage on external actions while preserving privacy for internal transfers, with Lean 4...
-
AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis
AutoCedar first builds a reviewed, checkable authorization boundary from natural-language requirements, then synthesizes Cedar policies against that fixed target with verifier-guided repair, solving all 221 CedarBench tasks.
-
Autoformalization of Agent Instructions into Policy-as-Code
An LLM-based generator-critic loop autoformalizes natural language policies into Cedar policies that cover substantially more of the source specification than hand-coded symbolic enforcement on MedAgentBench.
-
Automating Formal Verification with Reinforcement Learning and Recursive Inference
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.