feat(policy): Cedar as a policy language in OpenShell #4411

User Story

In OpenShell we use YAML for policies at this time backed by OPA and Rego. While structural YAML covers all the use cases we have today, it is a matter of time before we need policies that are inexpressible in structural YAML such as temporal policies and authorization policies tied to identities, roles, and access. To address these we need a language that is 1/ expressive enough to cover these cases and 2/ is fully formally analyzable so that we can always satisfy our tenet to ensure policies are fully decidable with respect to subsumption so that we can assure least privilege. Rego is not fully decidable, which means there are Rego programs that cannot be adjudicated for inclusion using any theory and an SMT solver. This has prompted using Cedar, which is a fully decidable and formally verified policy language from AWS.

Problem Statement

OpenShell sandbox policies can only be written in YAML and are evaluated by a general-purpose Rego program. There is no way to author a sandbox policy in a language built for automated analysis, so properties such as "this revision only narrows access" or "no policy lets this binary reach this host" cannot be checked mechanically against the policy that is actually enforced.

Impact / Why This Matters

Without this, users must review policy revisions by reading YAML and reasoning about how the Rego evaluator will treat it. The evaluator is over a thousand lines of general-purpose Rego, which tools cannot reason about exhaustively.

This results in:

• policy changes that silently widen access being found only in review or in production logs;
• no way to prove a staged restriction blocks what it should before enforcing it.

This matters because policy is the security boundary for autonomous agents. Cedar is an open-source authorization language from AWS, built for this kind of analysis:

• It has no loops, recursion, or user-defined functions, and it validates policies against a schema.
• Its symbolic compiler, cedar symcc, encodes policies into SMT with a sound and complete encoding, so a solver can prove a revision only narrows access, or return a concrete request that shows it does not.
• The language and its analyses are specified and proved correct in Lean, and the Rust implementation is tested against that model.

Those guarantees apply only if the Cedar policy is the policy OpenShell enforces, not a translation of YAML.

References:

• Cedar paper: OOPSLA 2024, doi:10.1145/3649835, extended version arXiv:2403.04651.
• How Cedar is built and verified: FSE 2024, doi:10.1145/3663529.3663854.
• Verified policy analyses: SymCert, FMCAD 2026.
• Implementation, including cedar symcc: cedar-policy/cedar. Lean model and proofs: cedar-policy/cedar-spec.

Proposed Design

A sandbox policy can be written in Cedar instead of YAML. The format is chosen once per sandbox and never mixed; YAML sandboxes behave exactly as today.

openshell sandbox create --policy ./policy.cedar --middleware ./middleware.yaml -- claude
openshell policy set my-sandbox --policy ./policy.cedar --wait
openshell policy get my-sandbox --full

permit (
    principal is Sandbox::Process,
    action == Sandbox::Action::"NetworkConnect",
    resource is Sandbox::NetworkEndpoint
)
when {
    resource.host like("*.github.com", ".")
    && resource.port == 443
    && context.binary_path == "/usr/bin/curl"
};

permit (
    principal is Sandbox::Process,
    action == Sandbox::Action::"HttpRequest",
    resource == Sandbox::NetworkEndpoint::"api.github.com:443"
)
when { context.method == "GET" && context.path like("/repos/*/*", "/") };

permit (
    principal is Sandbox::Process,
    action in [Sandbox::Action::"ReadFile", Sandbox::Action::"WriteFile"],
    resource in Sandbox::FilesystemPath::"/sandbox"
);

User-facing behavior:

• What Cedar decides. A .cedar file decides outbound connections, each request on inspected connections, and the filesystem paths the sandbox can read or write, using a fixed schema that OpenShell publishes.
• What the CLI does. It validates the file before sending it. Policies OpenShell cannot enforce exactly as written are rejected at submission with an explanation, not loaded and silently ignored.
• Globs. Globs use the same segment rules as YAML: * within one host label or path segment, ** across them. Hosts matched by a glob resolve through policy DNS under the same rules as YAML wildcard hosts.
• Middleware and endpoint settings. Middleware and endpoint settings such as tls: skip, MCP revisions, and the GraphQL persisted-query registry are configuration rather than access control, so they are supplied in a separate YAML file with --middleware.
• Providers. Attached providers supply credentials and token grants on connections and requests the Cedar policy already allows; they never grant access themselves, and their allowed_ips only narrow addresses.
• Request inspection. Request policies can match REST methods, paths, and query parameters (context.query), MCP methods and tool names, GraphQL operation types, names, and top-level fields, and WebSocket messages, including GraphQL over WebSocket. @path gives different paths of one host and port their own protocol and enforcement.
• Connections. @transport("tcp") marks native TCP endpoints, context.destination_ip restricts the resolved addresses a connection may reach (the Cedar form of allowed_ips), and context.binary_aliases matches symlinked binaries as YAML does.
• Audit mode. @enforcement("audit") on request policies gives audit mode, like YAML enforcement: audit, and lets a new restriction be staged and logged before it is enforced.
• Reloads. A running sandbox cannot switch between YAML and Cedar. Rejected revisions follow the gateway's existing policy_validation_failure_mode.
• Logs. They record which engine made each decision.

Acceptance Criteria

• A sandbox created with a .cedar policy enforces it for network connections (including native TCP and resolved-address ranges), inspected REST, JSON-RPC, MCP, GraphQL, and WebSocket requests, and filesystem access.
• YAML sandboxes behave exactly as before.
• Policies whose meaning OpenShell cannot enforce exactly are rejected by the CLI and the gateway with an actionable message.
• Switching a live sandbox between YAML and Cedar, Cedar global policies, and removing a filesystem grant from a live Cedar sandbox are rejected.
• policy set replaces a Cedar policy on a running sandbox; a rejected revision follows policy_validation_failure_mode.
• Middleware and endpoint settings supplied with --middleware apply on Cedar sandboxes.
• Attached providers inject credentials and token grants only on connections and requests the Cedar policy allows, and uninspected credentialed connections are refused as for YAML.
• Delimited globs on hosts and paths match the same values as the equivalent YAML globs, and host globs resolve through policy DNS.
• Every existing YAML decision test that does not need a Cedar language change has a Cedar equivalent with the same decision, except for documented differences.
• Audit-only request policies log instead of blocking, and staged audit policies never change a decision.
• openshell policy get shows the Cedar text, middleware, and (with --full) provider credential rules.
• Published docs describe authoring Cedar policies, and an end-to-end test covers a pure-Cedar sandbox.

Alternatives Considered

• Supervisor middleware. Middleware runs on traffic after the network decision and cannot own CONNECT authorization or Landlock filesystem grants. A Cedar policy in middleware would be a second decision layer on top of YAML, not an analyzable replacement for it.
• Gateway interceptors. These transform gRPC requests at the gateway and do not take part in runtime network or filesystem decisions inside the sandbox.
• Providers. Providers supply credentials and endpoint metadata; they do not express arbitrary access policy.
• Translating YAML to Cedar. Gaps between the languages would silently narrow or widen access for policies that hit them, and the translation itself would need verifying.
• Running both engines and requiring agreement. This needs the same policy written twice and doubles evaluation without making the enforced policy analyzable.
• Keeping Rego only. This leaves policy changes reviewable only by hand.

Agent Investigation

An implementation is on the feature branch vishwa/cedar-openshell, one commit on main. It passes unit tests on macOS and Linux and a 26-check end-to-end suite (mise run e2e:cedar). Every example and e2e directory with a YAML policy also has a Cedar version, and its scripts run either format with POLICY_FORMAT=cedar. Findings that bear on the design:

• Proto change. Additive SandboxPolicy fields carry the Cedar source and its endpoint settings, so gateway storage, revision history, and policy hashing are unchanged. A gateway-managed field carries provider credential rules.
• Decision routing. In the supervisor, every network decision point can be routed through one engine choice made at startup. A Cedar sandbox builds no OPA engine: middleware selection is shared Rust, and provider rules for token grants are compiled into Cedar.
• Experimental Cedar dependency. Segment-aware globs need delimited like, which the Cedar team has implemented (with a Lean specification and symcc support) on an experimental branch that is not yet released. The branch pins it by commit and can move to a released cedar-policy once Cedar releases delimited like.
• Parity with YAML. Of the 260 existing unit tests that check a YAML policy decision, 258 are ported into a harness that runs paired YAML and Cedar policies through both engines. One needs a Cedar language change (a binary glob matched against parent processes), and one tests data the YAML loader rejects. Across 766 cases, 752 agree and 14 are recorded differences:
  • Cedar allows more for a literal translation in seven cases: request rules on wildcard hosts (not expressible in Cedar), ** next to other characters, audit deny rules beside an enforced path, REST permits covering a GraphQL path, generic WebSocket text permits on a GraphQL-over-WebSocket endpoint, and two cases where a test's explicit protocol: "" leaves the endpoint out of YAML policy DNS but a gateway-delivered policy would not. The docs give a Cedar form that matches YAML for the four policy cases after the first.
  • Cedar allows less in seven cases: HEAD under a GET rule, audit allow rules beside an enforced path, a token-grant owner admitted only through a parent-process glob, MCP revisions without settings, more than 64 query value combinations, and two private-address cases where YAML's first-matching-endpoint order or provider rules admit an address.
• Found and fixed while porting. JSON-RPC calls and response frames sent without POST made Cedar more permissive, and method case made it stricter. Both are fixed and covered by parity cases.
• Known gaps.
  • SQL is not inspected for either format.
  • Globs over set members, such as a binary glob matched against parent processes or GraphQL field globs, need a Cedar language extension the Cedar team is evaluating. Exact names work today.
  • Request rules apply only to exactly named hosts, not to hosts a glob allows.
  • MCP receive streams and response frames need explicit permits, where YAML allows them on MCP endpoints automatically.
  • Proposals and incremental policy updates produce YAML rules, so proposal-based flows stop at the proposal step on Cedar sandboxes.
  • Native TCP, WebSocket, address ranges, symlinked binaries, and token grants are verified by the parity harness and unit tests; e2e/cedar does not cover them yet.
• Pre-issue RFC. A draft RFC describing the implementation is ready to move into rfc/ once maintainers assign a number.

Checklist

• I've reviewed existing issues and the published docs
• This is a design proposal, not a "please build this" request