feat(policy): spike policy envelope and narrowness checks

Problem Statement

Enterprise deployments need a way to define an auditable maximum OpenShell policy/profile and prove that local users, agents, reviewers, provider attachments, and policy updates cannot exceed it.

OpenShell should also explore whether policy proposals can be checked for narrowness. A proposal may be inside the maximum envelope but still too broad for automatic approval, such as granting ** path access when the observed denial was one exact request.

This issue is a spike. It should produce convincing fixtures and a feasibility report, not a production admission gate.

Research Hypothesis

The research question is whether policy negotiation can be reduced to satisfiability checks over OpenShell policy semantics.

For maximum-envelope enforcement, model each relevant capability as an abstract action x:

x = {
  binary,
  host,
  port,
  protocol,
  method,
  path,
  query,
  graphql_operation_type,
  graphql_fields,
  mcp_server,
  mcp_tool,
  mcp_resource
}

Then ask the OpenShell prover / Z3 model for a counterexample:

exists x:
  candidate_allows(x)
  AND NOT maximum_allows(x)

If this is unsat, the candidate stays within the modeled maximum. If this is sat, the solver should return a concrete capability that exceeds the maximum, such as:

x = {
  binary: "/usr/bin/gh",
  host: "api.github.com",
  port: 443,
  protocol: "rest",
  method: "POST",
  path: "/repos/NVIDIA/OpenShell/admin"
}

For narrowness, test whether the same style applies against a request-derived witness:

exists x:
  candidate_delta_allows(x)
  AND NOT witness_allows(x)

Also test whether some narrowness rules are better expressed as structural budget constraints:

breadth(candidate_delta) <= configured_budget

The spike should determine whether narrowness works best as SMT containment, structural budget checks, broadness scoring, or a hybrid.

Proposed Spike

Build fixture-driven tests that load:

maximum_policy: the security-approved OpenShell policy/profile envelope.
current_policy: the runtime's current minimal/effective policy.
proposal: a merge operation or proposed rule.
observed_denial: optional witness data for narrowness checks.
narrowness_budget: optional limits for automatic approval.
expected_max_result: within_max, exceeds_max, or unsupported.
expected_narrowness_result: within_budget, over_budget, or unsupported.

The spike should prefer concrete, runnable fixtures over product design. A successful spike can still be small if it demonstrates the model catches real broadening and gives useful counterexamples.

Initial Fixtures

Maximum-envelope fixtures should include:

Case	Maximum	Proposal	Expected
Exact REST path	`GET /repos/NVIDIA/OpenShell/issues/*`	`GET /repos/NVIDIA/OpenShell/issues/123`	within max
Broader REST path	`GET /repos/NVIDIA/OpenShell/issues/*`	`GET /repos/NVIDIA/**`	exceeds max
Method escalation	`GET /repos/**`	`POST /repos/**`	exceeds max
Query broadening	`GET /search/issues?org=NVIDIA`	`GET /search/issues`	exceeds max
Deny precedence	max `full` with deny `POST /admin/**`	`POST /admin/settings`	exceeds max
Host wildcard broadening	`api.github.com:443`	`*.github.com:443`	exceeds max
Binary broadening	`/usr/bin/gh`	`/usr/bin/*`	exceeds max
CIDR broadening	`10.0.5.0/24`	`10.0.0.0/8`	exceeds max
GraphQL mutation	`query` only	`mutation createIssue`	exceeds max
MCP placeholder	GitHub MCP `get_*` only	`create_pull_request`	exceeds max or unsupported until #1531

Start narrowness with a small budget model:

narrowness_budget:
  max_endpoints_per_update: 1
  max_binaries_per_update: 1
  allowed_method_breadth: exact_observed
  allowed_host_breadth: exact_observed
  allowed_path_breadth: exact_or_one_segment_wildcard
  forbid_recursive_path_wildcard: true
  forbid_binary_glob: true

Narrowness fixtures should include:

Observed denial	Proposal	Expected
`gh GET api.github.com /repos/NVIDIA/OpenShell/issues/123`	exact same host/method/path/binary	within budget
same	`/repos/NVIDIA/OpenShell/issues/*`	within budget if one-segment wildcard is enabled
same	`/repos/NVIDIA/OpenShell/**`	over budget
same	`**`	over budget
same GET denial	add `POST`	over budget
same host	`*.github.com`	over budget
same binary	`/usr/bin/*`	over budget
one denied endpoint	add GitHub and Slack in one proposal	over budget

Expected Output

A small fixture suite.
A short feasibility note for maximum-envelope checking.
A short feasibility note for narrowness budgets.
Example counterexample/redraft guidance for humans and agents, such as:

exceeds maximum: /usr/bin/gh can POST /repos/NVIDIA/OpenShell/admin via api.github.com:443

within maximum, but over narrowness budget: path /repos/NVIDIA/** is broader than the observed denial; try /repos/NVIDIA/OpenShell/issues/*

Code Areas To Inspect

Area	Files
Runtime policy semantics	`crates/openshell-sandbox/data/sandbox-policy.rego`, `crates/openshell-sandbox/src/opa.rs`, `crates/openshell-sandbox/src/l7/*`
Policy schema and merge	`crates/openshell-policy/src/lib.rs`, `crates/openshell-policy/src/merge.rs`
Prover	`crates/openshell-prover/src/policy.rs`, `crates/openshell-prover/src/model.rs`, `crates/openshell-prover/src/queries.rs`
Gateway proposal flow	`crates/openshell-server/src/grpc/policy.rs`

Non-Goals

Do not implement the production admission gate.
Do not design the full runtime-profile product.
Do not create a multi-issue roadmap before the spike results.
Do not require MCP support beyond placeholder fixtures until feat(policy): add MCP L7 inspection and enforcement #1531 defines the policy surface.

Labels

area:policy, area:gateway, area:sandbox, topic:l7, topic:security, topic:testing, spike, state:in-progress

🏗️ build-plan

Implementation Plan

Issue type: feat
Complexity: Medium
Confidence: Medium — clear first slice, with deliberate unsupported cases for policy surfaces the prover does not model yet

Summary

Add a first maximal-policy containment check to openshell-prover that answers whether a candidate OpenShell policy is within a security-approved maximum policy for the currently modeled allow surface. The first implementation should be fixture-driven, return concrete counterexamples for exceeded maximums, and fail closed with unsupported when either policy uses unmodeled surfaces such as deny rules, GraphQL, MCP, or query-param constraints.

This first slice is not the production admission gate. It is the smallest useful research/build step for validating the formula:

exists x:
  candidate_allows(x)
  AND NOT maximum_allows(x)

Scope

crates/openshell-prover/src/policy.rs: extend the prover-side parsed policy model only as needed for containment fixtures, including detection of unsupported fields such as deny_rules, GraphQL allow fields, and query matchers.
crates/openshell-prover/src/envelope.rs or similar new module: implement check_within_maximum(maximum, candidate) -> MaximumPolicyCheck with within_max, exceeds_max(counterexample), and unsupported(reason) results.
crates/openshell-prover/src/lib.rs: expose the new check for tests and later gateway integration.
crates/openshell-prover/testdata/ or module-level fixtures: add practical maximum-vs-candidate policy cases for REST methods, paths, host wildcards, ports, binaries, and unsupported deny/MCP/GraphQL cases.
crates/openshell-prover/README.md: document the maximal-policy check as a separate containment query from the existing risk/finding queries.

Implementation Steps

Add the result and evidence types.
- MaximumPolicyCheck::WithinMax
- MaximumPolicyCheck::ExceedsMax { counterexample }
- MaximumPolicyCheck::Unsupported { reason }
- Counterexamples should include at least binary, host, port, protocol, method, path, and a short explanation.
Normalize the modeled allow surface.
- Expand access: read-only, read-write, and full into effective REST methods.
- Normalize single port and ports.
- Preserve explicit REST allow rules as method/path pairs.
- Treat L4-only candidate access as broader than an L7 maximum unless the maximum is also L4/full enough to cover it.
Implement containment for the first supported surfaces.
- Candidate binaries must be covered by maximum binaries.
- Candidate host/port/protocol must be covered by a maximum endpoint.
- Candidate allowed REST methods must be a subset of maximum allowed REST methods.
- Candidate REST paths must be covered by maximum REST paths for the supported glob subset.
- Candidate wildcards broader than the maximum should produce a counterexample, not a silent failure.
Fail closed on unsupported policy language features.
- If either policy contains deny_rules, return Unsupported until the deny-rule prover issue lands.
- If either policy uses GraphQL operation fields, query matchers, MCP fields, persisted queries, CIDR-only allowed_ips, or other unmodeled surfaces, return Unsupported with a specific reason.
- Add fixtures that lock these as unsupported so future work can intentionally flip them to modeled behavior.
Add fixture-driven tests for the maximal envelope.
- Exact REST path within max.
- Broader REST path exceeds max.
- Method escalation exceeds max.
- Host wildcard broadening exceeds max.
- Binary wildcard broadening exceeds max.
- Port broadening exceeds max.
- L4 candidate against L7 maximum exceeds max.
- Deny-rule, GraphQL, query, CIDR, and MCP cases return unsupported.
Evaluate how much of this should use Z3 in the first slice.
- The existing prover model is Boolean reachability over enumerated policy atoms, which is good for current risk queries but too coarse for universal wildcard/path containment by itself.
- Start with semantic containment helpers where they are clearer and deterministic.
- Where practical, add a small solver-backed counterexample harness for enumerated method/port/binary choices, and document what would be required to encode string/glob containment directly in Z3.
- The output should make the research result honest: which parts are solver-backed, which are structural, and which need a richer symbolic encoding.

Test Plan

Unit tests: Add focused tests in the new containment module for result classification, counterexample evidence, wildcard/path coverage, method subsets, and unsupported-surface detection.
Integration tests: Add parse-to-check fixtures using realistic OpenShell policy YAML in crates/openshell-prover test coverage.
E2E tests: Not expected for this first slice because it does not wire into gateway admission or sandbox runtime enforcement.

Risks & Open Questions

The existing Z3 model does not yet represent symbolic strings, paths, globs, or all request attributes. If we force everything through that model too early, we may get a less truthful check. The first slice should separate semantic containment from solver-backed experiments and report the boundary clearly.
Deny rules change containment semantics because maximum policy can be broad with carve-outs. Until deny rules are modeled, returning unsupported is safer than incorrectly approving a candidate.
Host/path glob containment can become complex quickly. The first implementation should support the OpenShell glob subset used in fixtures and mark ambiguous patterns unsupported rather than guessing.
Need a decision later on where the production check lives: prover-only library, gateway policy proposal path, provider-profile attachment path, or all three.

Documentation Impact

Update crates/openshell-prover/README.md to describe maximal-policy containment and its current supported/unsupported surfaces.
No published docs or gateway config docs expected in this first slice because no user-facing runtime behavior or gateway TOML field changes.

Revision 1 — initial maximal-policy implementation plan

Closing as spike complete and superseded by production issue #2109. The spike validated the policy-envelope/prover direction; implementation should reuse the useful code and findings from PR #1843 through the #2109 production path.

Navigation Menu

Repository navigation

feat(policy): spike policy envelope and narrowness checks #1840

Problem Statement

Research Hypothesis

Proposed Spike

Initial Fixtures

Expected Output

Code Areas To Inspect

Non-Goals

Labels

Implementation Plan

Summary

Scope

Implementation Steps

Test Plan

Risks & Open Questions

Documentation Impact

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

feat(policy): spike policy envelope and narrowness checks #1840

Description

Problem Statement

Research Hypothesis

Proposed Spike

Initial Fixtures

Expected Output

Code Areas To Inspect

Non-Goals

Labels

Activity

zredlined commented on Jun 9, 2026

Implementation Plan

Summary

Scope

Implementation Steps

Test Plan

Risks & Open Questions

Documentation Impact

zredlined commented on Jul 2, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions