Cedar

Lead Summary

Cedar is a purpose-built authorization policy language released by AWS in May 2023 under the Apache 2.0 license. Where most policy systems are either general-purpose engines (OPA/Rego) or graph-based relationship stores (OpenFGA, SpiceDB), Cedar occupies a deliberate middle ground: it is expressive enough to cover RBAC, ABAC, and entity-hierarchy ReBAC in a single language, while remaining non-Turing-complete so that every policy can be translated into decidable SMT formulas and analyzed with mathematical certainty.

The spine of the language is the PARC model — every policy is a statement about a Principal performing an Action on a Resource given a Context. Policies yield exactly one of two effects: permit or forbid. That constraint, which feels limiting at first, is the prerequisite for everything else Cedar offers: sub-millisecond evaluation, schema-validated typing, and formal safety guarantees proven in Lean.

Cedar joined the Cloud Native Computing Foundation as a Sandbox project in January 2026, moving governance from AWS-only stewardship toward a vendor-neutral RFC process.

---

Core Concepts

The PARC model

Every Cedar policy evaluation receives four inputs: the principal (who is acting), the action (what they want to do), the resource (the thing being acted upon), and the context (request-time metadata such as IP address, MFA status, or timestamp). Policies match against these four slots and produce a boolean permit or forbid decision.

This is not merely a convention — it is an architectural constraint that makes formal verification possible. By fixing the shape of the input space and restricting output to two values, Cedar can be translated into satisfiability modulo theories (SMT) formulas in decidable logical theories. OPA/Rego is Turing-complete and cannot be encoded this way; Cedar's restricted design is the prerequisite for sound and complete automated analysis.

Four design goals in tension

Cedar's designers identified four goals: expressiveness, performance, safety, and analyzability. These pull against each other. Maximum expressiveness means Turing-completeness, which breaks decidable analysis. Cedar resolves the tension by prioritizing safety and analyzability, then recovering expressiveness within those bounds using the PARC domain model.

The result is a language that cannot express arbitrary decision logic, iteration, helper functions, or non-boolean results — but within the authorization domain, these omissions rarely matter and the gains are substantial.

Default deny and forbid-overrides-permit

Cedar's decision procedure has two safety properties proven in Lean:

1. Default deny. If no permit policy evaluates to true for a request, the request is denied. There is no "allow by default" — the absence of an explicit grant is always a denial.

2. Forbid trumps permit. A forbid effect always overrides any permit effect. No combination of permit policies can grant access if any forbid policy also applies to the same request.

These are not runtime behaviors or implementation details. They are mathematical theorems about the language semantics, checkable by automated tools.

---

Policy Structure: Scope and Conditions

A Cedar policy has two parts: a scope and optional condition clauses.

permit (
  principal == User::"alice",
  action    == Action::"ReadDocument",
  resource  == Document::"q3-budget"
);

The scope fixes which principals, actions, and resources the policy applies to. When a request arrives, Cedar first checks whether it matches the scope. Only matching requests proceed to condition evaluation.

Conditions are when and unless clauses that narrow or expand the scope based on attribute values:

permit (
  principal,
  action    == Action::"ReadDocument",
  resource
)
when {
  context.mfa_used == true &&
  resource.classification != "top-secret"
};

The canonical Cedar pattern is: express the coarse-grained RBAC rule in the scope, then refine it with ABAC conditions in when/unless clauses.

---

RBAC: Roles as Group Membership

Cedar implements role-based access control by treating roles as principal groups — entity collections that principals belong to. There are no separate role tables; roles are just entities of a particular type.

// Grant the Editors group permission to update any document
permit (
  principal in Group::"Editors",
  action    in [Action::"UpdateDocument", Action::"CreateDocument"],
  resource  in Namespace::"content"
);

When Cedar evaluates this policy, it checks whether the requesting principal is a member of (or transitively nested inside) Group::"Editors". Adding or removing a user from the Editors group changes what they can do without touching any policy text.

The in keyword is doing relationship traversal here — which is also how Cedar handles entity hierarchies for ReBAC patterns (see below).

---

ABAC: Attribute Conditions

Attribute-based access control flows from the when and unless clauses. ABAC conditions can reference attributes on the principal, the resource, or the context object:

// Allow a user to read documents owned by their department
permit (
  principal,
  action    == Action::"ReadDocument",
  resource
)
when {
  principal.department == resource.owner.department
};

// Allow access only during business hours from known IPs
permit (
  principal in Group::"Contractors",
  action    == Action::"ReadDocument",
  resource  in Namespace::"internal"
)
when {
  context.hour >= 9       &&
  context.hour < 18       &&
  context.ip.isInRange(ip("10.0.0.0/8"))
};

Context attributes are passed in with each authorization request, making them the natural home for request-time facts (timestamp, MFA status, network location) that are not stored on any entity.

---

ReBAC: Entity Hierarchy and the in Operator

Cedar supports a form of relationship-based access control through its entity hierarchy model. Entities can have parent entities, forming a directed acyclic graph (DAG). The DAG constraint — no cycles — ensures that hierarchy traversal terminates and produces deterministic results.

The in operator traverses this hierarchy. A policy that says resource in Folder::"reports" matches not just the folder itself but any entity that has the folder as an ancestor:

// Anyone who owns a folder automatically has access to all files in it
permit (
  principal,
  action    == Action::"ReadFile",
  resource  in Folder::"quarterly-reports"
)
when {
  resource.owner == principal
};

A more explicit ownership-hierarchy pattern:

// Folder owners can read any file whose parent folder they own
permit (
  principal,
  action    == Action::"ReadFile",
  resource
)
when {
  principal == resource.parentFolder.owner
};

The entity store passed to Cedar at evaluation time carries the parent relationships. Cedar does not maintain a persistent graph — the caller loads the relevant entities and edges for each decision.

Where Cedar's ReBAC stops

Cedar's hierarchy model does not replicate Zanzibar-derived systems like OpenFGA or SpiceDB. Those systems natively support user-defined relation types and traversals across heterogeneous relation kinds (e.g., "viewer-of-folder implies viewer-of-files" expressed as a first-class relation rule). Cedar's parent-child graph supports tree-shaped containment well — nested folders, organizational hierarchies, resource namespaces — but complex arbitrary relation kinds require modeling the relationships as entity attributes and writing policies that interpret them explicitly.

---

Combining All Three: RBAC + ABAC + ReBAC in One Policy

These patterns are not mutually exclusive. Cedar's design explicitly supports combining them in a single policy:

// Editors in the same team as the document's owner can edit it,
// but only if MFA is active and the document isn't locked.
permit (
  principal in Group::"Editors",          // RBAC: role as group
  action    == Action::"EditDocument",
  resource  in Namespace::"team-docs"     // ReBAC: namespace containment
)
when {
  principal.team == resource.owner.team   // ABAC: attribute match
  && context.mfa_used == true             // ABAC: context attribute
}
unless {
  resource.locked == true                 // ABAC: attribute guard
};

The scope expresses the role-based rule; the when clause adds attribute refinement; the unless clause adds an attribute-based guard that overrides the permission when the document is locked.

---

Schema: Declaring the Type System

Cedar's schema is what makes static analysis possible. It declares entity types, their attributes, and which actions apply to which entity types. The policy validator uses this schema to catch errors before deployment:

{
  "MyApp": {
    "entityTypes": {
      "User": {
        "shape": {
          "type": "Record",
          "attributes": {
            "department": { "type": "String" },
            "team":       { "type": "String" }
          }
        },
        "memberOfTypes": ["Group"]
      },
      "Group": {},
      "Document": {
        "shape": {
          "type": "Record",
          "attributes": {
            "classification": { "type": "String" },
            "locked":         { "type": "Boolean" },
            "owner":          { "type": "Entity", "name": "User" }
          }
        },
        "memberOfTypes": ["Namespace"]
      },
      "Namespace": {}
    },
    "actions": {
      "ReadDocument": {
        "appliesTo": {
          "principalTypes": ["User"],
          "resourceTypes":  ["Document"]
        }
      },
      "EditDocument": {
        "appliesTo": {
          "principalTypes": ["User"],
          "resourceTypes":  ["Document"]
        }
      }
    }
  }
}

If a policy references principal.nonexistent_attribute, the validator will reject it. This soundness is formally proven: policies that pass schema validation will not produce type errors at evaluation time for schema-conforming requests.

---

The forbid Guardrail Pattern

forbid policies are the primary tool for security guardrails. Because forbid always overrides permit — regardless of how many permit policies match — a single forbid rule can act as an unconditional safety net:

// No one, regardless of role, can access documents classified top-secret
// without explicit additional clearance
forbid (
  principal,
  action,
  resource
)
unless {
  resource.classification != "top-secret"
  || principal.clearance == "top-secret"
};

A more targeted guardrail that locks down a specific action unconditionally during a maintenance window:

forbid (
  principal,
  action    in [Action::"WriteDocument", Action::"DeleteDocument"],
  resource
)
when {
  context.maintenance_mode == true
};

A forbid is not "deny unless permit wins." It is a hard stop. Once any forbid evaluates to true for a request, the outcome is denial — no permit chain can override it.

This asymmetry is why the pattern of writing broad permit policies scoped to roles and narrow forbid policies scoped to sensitive conditions is idiomatic in Cedar. The forbid layer forms an outer safety boundary that the permit layer operates within.

---

What Cedar Does Not Let You Do (and Why)

Several design omissions are intentional:

No unbounded loops. Loops create an infinite number of possible execution paths, breaking symbolic evaluation. Without symbolic evaluation, SMT analysis is impossible. Cedar offers set operations and .contains() / .containsAll() / .containsAny() instead.

No user-defined functions. User functions enable arbitrary recursion, which increases analysis complexity unboundedly. Cedar provides built-in functions and methods only. The variables available in a policy body are fixed: principal, action, resource, context.

No regular expressions. Regex is intentionally excluded because it is error-prone and hard to analyze. A real incident cited in Cedar's documentation: a policy tested group membership against /admin/ without word boundaries, accidentally matching the "administrative-assistants" group. Cedar provides a like operator with explicit wildcards (* only) and built-in types like ipAddr and decimal for common authorization predicates.

No Turing-completeness. This is the root constraint from which all others follow. Cedar's language maps to decidable SMT theories (linear arithmetic, bit-vectors, fixed-width strings). OPA/Rego is Turing-complete and cannot be encoded this way, which is why Rego cannot provide sound and complete analysis.

---

Formal Verification as Design Rationale

The practical policy patterns above rest on a formal foundation that influences their behavior in ways worth understanding.

Cedar's authorization engine is formally specified in Lean 4, an open-source proof assistant. The Lean model is fully executable and serves as the reference implementation. The production Rust engine is validated against the Lean model through differential random testing (DRT): millions of randomly generated policy evaluation inputs are run through both engines, and any divergence is a bug. This process discovered 25+ bugs during development that conventional testing would likely have missed — 4 found during the proof process itself, 21 from DRT.

The symbolic compiler translates Cedar policies into SMT formulas. Its correctness is also proven in Lean. This means analysis errors cannot arise from compiler bugs — only from the SMT solver or from fundamental misunderstandings in policy intent.

What this gives practitioners:

• Policy equivalence checking. You can prove that a refactored policy set is semantically equivalent to the original — the set of authorized requests did not change. No other practical policy language offers this.
• Vacuity detection. A policy that never evaluates to true for any valid request in the schema is a policy that can never matter. Cedar Analysis can detect this.
• Overly-permissive policy detection. Ask whether any request exists that would be permitted by the new policy set but denied by the old one.

---

Comparison with Related Systems

Fig 1

Dimension	Cedar	OPA/Rego	OpenFGA / SpiceDB
Model	PARC, policy-as-code	General-purpose, policy-as-code	Relationship graph + tuple store
Expressiveness	Authorization domain	Turing-complete	Typed relations only
Formal analysis	Sound, complete (SMT)	Not possible	Limited
Performance	42–80x faster than Rego	Baseline	Optimized for graph traversal
Primary layer	Application authorization	Infrastructure / K8s / CI-CD	App-level fine-grained permissions
Deployment	Embedded SDK or managed (AVP)	Sidecar / embedded	Managed service

OPA's Turing-completeness is a real advantage for infrastructure-layer policies (Kubernetes admission control, service mesh) where the problem space is too varied for a fixed model. Cedar's restricted design is a real advantage for application authorization where PARC maps naturally and you want safety guarantees.

Within the PARC domain, Rego can exhibit non-determinism and runtime exceptions in ways Cedar cannot, because Cedar's type system and evaluation model guarantee a definite result for every valid request.

---

Deployment

Cedar supports two topologies:

Embedded SDK. The cedar-policy Rust crate evaluates policies inside the application process. Bindings exist for Python (cedarpy), Go (cedar-go), .NET (CedarDotNet), and Ruby (cedar-policy-rb). Sub-millisecond evaluation latency. Policies must be loaded from wherever you store them; Cedar does not prescribe storage.

Managed service via Amazon Verified Permissions (AVP). AVP stores Cedar policies centrally, evaluates decisions via a REST API, and handles audit logging. Architecturally separate from but tightly integrated with Cedar. Useful when policy management needs to be centralized and decoupled from application deployments.

The practical tradeoff: the embedded SDK gives zero remote latency and no AWS dependency; AVP centralizes policy management across services but introduces AWS coupling. Self-hosted, multi-cloud, and air-gapped scenarios face more friction with Cedar than with OPA, which has a richer independent deployment ecosystem.

---

Current Status

Cedar joined the CNCF Sandbox in January 2026, placing it on the graduated-project path alongside OPA (already a CNCF Graduated project). This formalized a Rust-style RFC governance process for language changes, with core semantic changes requiring RFC proposals and community review.

Production adopters include MongoDB Atlas (multi-tenant database resource policies across thousands of deployments), StrongDM (native Go implementation for database access control), Cloudflare, and Cloudinary. At AWS, Cedar underpins Amazon Verified Permissions and AWS Systems Manager.

An emerging use case is AI agent authorization via MCP. Cedar's decidable analysis makes it a natural fit for constraining autonomous agents: a cedar-analysis-mcp-server packages Cedar's analysis capabilities so that LLM-based systems can query formal policy analysis before executing tool calls.