Cedar as the policy language in OpenShell

Vishwanath Raman OpenShell Team @ NVIDIA

Dev Note November 9, 2026 Research

OpenShell is a runtime for AI safety and governance that uses a policy driven enablement of least-privilege access to AI agents. OpenShell policies are written in structural YAML and evaluated using Rego¹ as the policy language, with regorus, a Rust implementation of Rego, as the engine. Rego is a general-purpose language with no decidable procedure that can always answer inclusion questions, such as "Does policy \(P_1\) grant no more than policy \(P_2\)?", for all possible policies \(P_1\) and \(P_2\). Today OpenShell gets that analysis by maintaining a prover model for the supported YAML structure and using an SMT² solver as the decision procedure to answer these questions. But every new policy enhancement needs extensions to the YAML schema, the backend Rego program, and to the prover model that analyzes it.

As policy semantics expand, we anticipate the need to enhance the policy language to move beyond point-in-time policies to temporal policies, such as "Allow X only after Y", which would be inexpressible in YAML. Given these considerations, with the desire to future-proof our policy framework, we began our quest for a new policy language. We had the following in mind when it came to picking one.

1. Decidable policy inclusion: We need a language that lets us check if the permissions granted by policy \(P_1\) are no more than those granted by policy \(P_2\), for all policies \(P_1\) and \(P_2\).
2. Built for formal verification: We need a language that is purpose-built for formal analyzability from the ground up, so that what we prove about a policy holds for the policy that runs.
3. Open and widely adopted: The language should be open-source, an industry standard, widely used, and it should extend policies used for cloud-native applications to cover cloud-native AI agents.

One of the applications of the policy framework in OpenShell is to always maintain a least-privilege ceiling for agent fleets. An agent that handles a job should only have privilege grants that are 1/ what the agent needs to do that job and 2/ have been vetted by security and compliance teams. These grants expressed in a policy file then form the privilege ceiling for this agent. In agentic systems with one or more agents, a ceiling policy for an agent is included in the ceiling policy of the team of agents which in turn is included in the ceiling policy of the business unit. In the other direction, a sub-agent spawned for a job might not need all of the permissions of its instantiating parent.

The question then becomes can we always check "Does \(P_1\) give no more permissions than \(P_2\)?" Mathematically, is it the case that \(P_1 \Rightarrow P_2\)? If so, taking \(\mathit{allowed}\) to be a function that takes a policy and returns the set of all requests that policy allows, \(\mathit{allowed}(P_1) \subseteq \mathit{allowed}(P_2)\). This piece of machinery is what lets us maintain a least-privilege ceiling together with permission revocation after use when possible.

Introducing Cedar

Cedar is an open-source CNCF project, originally created at AWS for authorization decisions, and is actively used for agent policies in Amazon Bedrock AgentCore and Strands Agents. It is used at scale for authorization in AWS products and services. It is also fast. The Cedar authors report that, on the benchmarks in their paper, the Cedar authorizer is 42.8–80.8× faster than Rego³.

A Cedar policy follows the Principal, Action, Resource, Context or PARC model for short. It is a concise permit or forbid statement about what action over what resource a principal is proposing under a given context with optional conditions over attributes of the request. Everything is denied by default, and a matching forbid always wins. In Cedar you write a schema that defines the authorization primitives of your system. Validating policies against the schema rules out whole classes of runtime errors during policy evaluation.

Introducing Cedar is best served by an example. For those of you familiar with our YAML policy framework, please read on. For others, if you would like to learn more about our current support for policies, please visit our Sandbox Policies documentation.

A network YAML policy

In this example, a triage agent may label issues in one repository and nothing else on GitHub. It can add labels to issues in NVIDIA/OpenShell but it cannot comment, close issues, edit code, or touch any other repository.

version: 1

network_policies:
  github_triage:
    name: github-issue-labeling
    endpoints:
      - host: api.github.com
        port: 443
        protocol: rest
        enforcement: enforce
        rules:
          - allow:
              method: POST
              path: "/repos/NVIDIA/OpenShell/issues/*/labels"
    binaries:
      - { path: /usr/bin/gh }

The same network policy in Cedar

@id("github_triage/connect")
permit (
    principal is Sandbox::Process,
    action == Sandbox::Action::"NetworkConnect",
    resource == Sandbox::NetworkEndpoint::"api.github.com:443"
)
when { context.binary_path == "/usr/bin/gh" };

@id("github_triage/add-labels")
permit (
    principal is Sandbox::Process,
    action == Sandbox::Action::"HttpRequest",
    resource == Sandbox::NetworkEndpoint::"api.github.com:443"
)
when {
    context.binary_path == "/usr/bin/gh"
    && context.method == "POST"
    && context.path like("/repos/NVIDIA/OpenShell/issues/*/labels", "/")
};

The differences worth noting are:

1. Two decisions instead of one block. The YAML policy specification language combines rules with binaries in a single entry, whereas Cedar splits this into a NetworkConnect decision and an HttpRequest decision. This separates concerns into a decision for opening the connection using gh and another for the actual request that the proxy inspects. Each HttpRequest policy names the endpoint with either exact matching or with wildcards⁴. Because each decision matches the point of enforcement, being allowed to open a connection never implies being allowed any particular request on it, so each grant stays as narrow as the job needs.
2. What YAML implies, Cedar says. A YAML binary automatically matches its symlinks and the processes launched implicitly. A YAML GET also allows HEAD. Cedar makes these explicit and in that sense the Cedar policy above is narrower than its YAML counterpart. It matches gh and nothing it launches. When you need matching through aliases or child processes, you request them explicitly, using binary_aliases.contains("/usr/bin/gh") or ancestors.contains("/usr/bin/gh").
3. Credentials don't grant access. When you attach a provider, such as GitHub in this case, you are supplying a token and not the permissions that use that token. The Cedar policy is what defines the set of all accesses the token can be used for.
4. Checked when submitted, and analyzable. Cedar rejects malformed policies when they are set, just like YAML, and in addition Cedar's schema checks the conditions themselves, leading to rejections of policies with misspelled attributes or type errors inside a when clause. Since the Cedar policy is the policy that is enforced, we can formally check that this agent's ceiling is subsumed by the triage team's ceiling.

Why we picked Cedar

Cedar balances expressivity, readability, and decidability. Cedar was designed to be fully decidable³. In a nutshell, what makes a policy language decidable is that every question we can ask about a policy, such as "can a given agent ever reach a specific endpoint?" or "does a spawned sub-agent's policy grant anything that its parent does not?", can be answered with a definitive yes or no. This is not true for general-purpose policy languages, where some questions do not yield a definitive yes or no answer using any theory and an SMT solver.

Cedar does not support loops, recursion, or user-defined functions that lead to unboundedness and loss of decidability. In exchange, every evaluation terminates and generally runs in linear time, or quadratic time in the worst case because of set containment operations³. Its symbolic compiler reduces any policy set to SMT with an encoding proved sound and complete⁵ in Lean⁶, and the resulting queries are solved with the cvc5 SMT solver⁷. Analysis therefore extends to whatever an author writes, and it applies to the policy that is enforced, because the compiler and the evaluator share one specified semantics. That is also why a Cedar sandbox enforces the Cedar text itself, so analysis and enforcement always see the same policy.

Cedar has a Lean specification and a Rust implementation checked against it using differential random testing⁸. A Cedar policy is a condition over a principal, an action, a resource, and a request context, validated against a schema, so authors can state precisely what they mean. For example, a policy can let a binary reach an endpoint only when a specific parent launched it, or conversely only when a specific parent did not launch it.

For agents, using Cedar changes the assurance we can offer. Instead of testing that a sub-agent always stays within its parent's permissions, we can prove that it cannot exceed them on any run with the proof over the policy that is actually enforced. This proof holds over all possible requests, which makes the choice compelling.

We anticipate the need for temporal policies and our integration with Cedar provides a clean and natural path to temporal policies with Dogwood⁹, another open-source initiative from AWS. Dogwood extends Cedar with when temporal { ... } conditions over the history of events the authorizer has seen, such as:

• "permit this call only if the same principal was approved within the last hour"
• "deny after a logout until the next login"

Status

We have implemented Cedar as an alternate policy language in OpenShell, with the RFC and integration under review (OpenShell RFC 0020, OpenShell integration). Cedar support is available in development builds today; stable builds reject Cedar policies.

What's coming

Prover

The OpenShell prover is a standalone tool at the moment that encodes YAML policies into an SMT encoding with Z3¹⁰ as the decision procedure to check inclusion between pairs of policies. That encoding is built by hand, so every new policy feature needs a matching extension to the prover. The prover is what we use to continuously check policies against their ceilings and to whittle permissions down. We will extend the prover to cover Cedar, using Cedar's symbolic compiler, whose encoding is proved sound and complete⁵.

A Cedar policy set has a precise set-theoretic meaning, and Cedar's analysis decides relations between policy sets, which gives us the following capabilities that we will expose in the prover.

1. Union: each permit contributes the requests it matches, and a policy set \(P\) allows their union, \(\mathit{allowed}(P)\).

2. Set difference: this is what forbid adds. A matching forbid always overrides any permit, so

   \[ \mathit{allowed}(P) = \Big(\bigcup \mathit{permits}\Big) \setminus \Big(\bigcup \mathit{forbids}\Big) \]

   That's the formal reason "forbid always wins" and why policy order doesn't matter.

3. Intersection, within a single policy: a policy's scope and all of its when clauses are conjoined, and unless clauses are conjoined after negation. A single policy's match set is therefore the intersection of its constraints. There's no operator that intersects two policy sets, though. To require two sets to both allow a request, you evaluate them separately and combine the results outside Cedar.

4. Complement: you never write it directly. It's implicit, because anything no permit matches is denied by default.

Over these, Cedar's analyzer decides the following relations between two policy sets \(P_1\) and \(P_2\), over all requests the schema allows, returning a counterexample when the answer is no. Each relation has a logical reading and a set-theoretic one. Read a policy set as a predicate that is true of exactly the requests it allows. Then implication between policies is inclusion between their allowed sets.

• Inclusion: \(\mathit{allowed}(P_1) \subseteq \mathit{allowed}(P_2)\), or equivalently \(P_1 \Rightarrow P_2\). This is the ceiling check. It answers the question we started with. When the answer is no, the counterexample is a request in \(\mathit{allowed}(P_1) \setminus \mathit{allowed}(P_2)\), naming a grant that exceeds the ceiling. That is the grant to remove when whittling permissions down.
• Equivalence: \(\mathit{allowed}(P_1) = \mathit{allowed}(P_2)\), or \(P_1 \Leftrightarrow P_2\), for example to confirm that a refactored policy allows exactly what the original did. It is inclusion in both directions, so it also confirms that narrowing a policy removed only what we meant to remove.
• Disjointness: \(\mathit{allowed}(P_1) \cap \mathit{allowed}(P_2) = \emptyset\), or \(\neg(P_1 \wedge P_2)\) for every request, for example to confirm that two agents share no grants.

Temporal policies: A teaser

// state:accepted only after a maintainer approved that same issue
// within the last 24 hours.
@id("triage/accept-after-approval")
permit (
    principal is Sandbox::Process,
    action == Sandbox::Action::"AddIssueLabel",
    resource == Sandbox::NetworkEndpoint::"api.github.com:443"
)
when {
    context.input.repo == "NVIDIA/OpenShell"
    && context.input.label == "state:accepted"
}
when temporal {
    formerly within 24h Sandbox::Action::"ApproveIssue"::response{
        input.repo: context.input.repo,
        input.issue: context.input.issue,
        output.approved: true
    }
};

The triage agent from our example can label issues at any time, but one label is special: state:accepted. This Dogwood policy lets the agent apply it only if a maintainer approved that same issue in the last 24 hours. The when block is ordinary Cedar and checks the request in front of us. The when temporal block looks back over the history of events: was there an approval for this repository and issue, with approved: true, within the window? If there was no approval, if it was a rejection, or if it was for a different issue or is more than a day old, the request is denied. Dogwood lowers the temporal condition to a single context value, so the decision is still made by the Cedar engine. Dogwood also adds information providers, values computed on demand that a condition may consult. This is not something OpenShell enforces today but is meant as a teaser of what's coming with Dogwood. AddIssueLabel and ApproveIssue are illustrative actions, not part of the OpenShell policy schema today.

This opens an interesting question and research direction. Since the approved state is updated outside of the policy, it is critical that the events the policy depends on, such as the recorded approval, are correct, because the correctness of the policy decision rests on them. In short, there is a transfer of trust here that falls under the shared responsibility model. The entities producing the events that policies depend on need to ensure those events are correct and recorded with integrity, and the entities writing policies need to choose event sources they can trust.

The correctness of these events is a vertical-agnostic concern. A community-driven initiative to assure the correctness of such events, perhaps deploying either formal or testing-based approaches, is a need.

Looking further out, a common concern from enterprises is authoring and managing the thousands of policies that large-scale agent deployments will need. We are exploring how to synthesize policies from agent traces and intent. Going back to our desire to assure least-privilege access for all agents, decidability across all expressible policies is what makes every synthesized policy checkable against a given policy ceiling before it is ever used. We will share more as that work matures.

Conclusion

We're incredibly excited to bring Cedar and eventually Dogwood to OpenShell. We would like to give a special callout to our friends in AWS Automated Reasoning, Liana Hadarean and Lucas Käldström, for helping us with experimental features to get us here. Thanks to Johnny Greco, from the OpenShell team, for valuable feedback that shaped this note. This is a big step toward correctness as we work toward AI safety and governance on our journey to build trustworthy agentic systems. If you are interested in OpenShell, formal methods, AI safety and governance, or any other related topic, join the OpenShell community. Find the project in the CNCF Slack channel #openshell-dev (join the CNCF Slack).

References