Standalone Policy Prover

openshell-prover checks whether the authority in a local candidate policy is contained within a local boundary policy. The command reads files from the host and does not connect to an OpenShell gateway.

The candidate must be the fully composed effective policy after the proposed change, including any provider-contributed authority. The boundary is an operator-owned ceiling. It does not grant authority by itself.

Install the Prover

The standard OpenShell installer includes openshell-prover:

curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh
openshell-prover --version

The prover remains independent of the gateway at runtime. If you only need the standalone binary, use the artifacts listed in the Support Matrix. These artifacts and openshell-prover-checksums-sha256.txt are attached to OpenShell releases.

The release archive includes the solver linkage required by the executable. It does not require the main openshell command, a gateway configuration, or a separate Z3 installation.

Check a Policy Boundary

Create boundary.yaml with this boundary policy:

version: 1
filesystem_policy:
  read_only:
    - /usr
    - /etc

Create candidate.yaml with this contained candidate:

version: 1
filesystem_policy:
  read_only:
    - /usr

Run the check:

openshell-prover check candidate.yaml --boundary boundary.yaml

A contained candidate prints result: within_boundary and exits with status 0. To see an exceeding result and its counterexample, replace candidate.yaml with a policy that grants writes to /tmp. The boundary grants no write access:

version: 1
filesystem_policy:
  read_only:
    - /usr
  read_write:
    - /tmp

openshell-prover check candidate.yaml --boundary boundary.yaml

To check the current effective policy of an existing sandbox, export it without display metadata:

openshell sandbox get my-sandbox --policy-only > candidate.yaml
openshell-prover check candidate.yaml --boundary boundary.yaml

This export includes provider-contributed rules. For a proposed change that is not active, supply the complete post-change effective policy. The standalone prover does not compose a base policy with provider rules.

Use JSON when a script consumes the result:

openshell-prover check candidate.yaml \
  --boundary boundary.yaml \
  --output json

The JSON object includes the result, exit code, input paths, schema version, prover version, and modeled domains. schema_version versions the JSON contract, prover_version identifies the implementation that produced the result, and coverage.domains is the machine-readable declaration of modeled policy domains. An exceeding result also includes a typed counterexample. Automation should use result and reason_code instead of parsing the human-readable explanation.

The counterexample.domain field selects one of these objects:

Network binary and ancestor_binary values are null when binary identity enforcement is disabled. method and path are null for L4 witnesses. trusted_gateway: true means the witness uses a recognized host-gateway alias with a runtime-provided trusted gateway binding; false uses ordinary destination validation.

The stable reason codes are invalid_input, unsupported_policy_shape, unresolved_workdir, unresolved_binary_path, unresolved_filesystem_path, solver_timeout, solver_unknown, resource_limit, invalid_witness, and cancelled.

The solver has a finite 10-second default budget. Set a different positive budget with an integer followed by ms, s, or m:

openshell-prover check candidate.yaml \
  --boundary boundary.yaml \
  --timeout 30s \
  --output json

Exit Codes

Only exit 0 means the verification succeeded. Treat unsupported and inconclusive results as failures in CI.

Interpretation and Limits

The containment check covers filesystem paths, process identity settings, Landlock compatibility requirements, L4 destination authority, and enforced REST method and path authority, including explicit REST denies. The result object reports the policy domains modeled by each check. Policies that use recognized authority outside that coverage return unsupported rather than silently ignoring it.

Both inputs use the same bounded YAML/JSON parser and authored policy schema as OpenShell. Unknown fields, duplicate keys, malformed field types, and unsupported managed metadata or review annotations return error with reason_code: invalid_input and exit 2. Schema-valid controls outside the containment model return unsupported and exit 3.

The prover applies aggregate limits across the candidate and boundary before semantic shape validation: 1,024 network rules, 4,096 endpoints, 4,096 binary selectors, 65,536 authored port entries, 4,096 allowed_ips entries, 16,384 REST rules, 4 KiB per modeled pattern, and 1 MiB of modeled pattern text. Exceeding any limit returns inconclusive with reason_code: resource_limit. A cancellation already requested at preflight takes precedence over that result; otherwise a resource limit takes precedence over unsupported policy-shape diagnostics. This ordering keeps validation work bounded for checked-in CI inputs.

Process and Landlock settings

Matching supported run_as_user and run_as_group values do not expand the configuration. Changing an explicit non-root identity to root or 0 returns exceeds_boundary with the field and both values. Other identity changes return unsupported; the command does not resolve accounts from a sandbox image. These comparisons assume consistent identity resolution and execution settings. They do not prove permission relationships between arbitrary Linux accounts.

Landlock hard_requirement may not become best_effort. That change returns exceeds_boundary. Keeping the same mode or strengthening it to hard_requirement passes this part of the check. This compares the requested requirement, not whether a target kernel successfully installed Landlock restrictions.

Destination IP restrictions

The network action includes an IPv4 or IPv6 destination address. CIDR entries in allowed_ips are modeled together with host, port, executable, and REST restrictions; network counterexamples include destination_ip. An empty IP list follows the runtime’s destination rules and is not a universal allowlist. The check does not resolve DNS on the host running the CLI.

Policies whose potentially overlapping endpoints select different destination restrictions remain unsupported because the runtime uses the selected endpoint’s address filter. The prover conservatively treats wildcard host selectors on a shared port as potentially overlapping, including when their literal suffixes differ. CIDR unions within a supported endpoint are checked by the solver. Unsupported IP-literal wildcard selectors and ranges rejected by the runtime also cannot produce a successful proof.

Consumers must inspect coverage.domains and require every domain relevant to their authorization decision. A successful result applies only to those reported domains and the documented assumptions.

Remaining limits

Network binary selectors, endpoint host and path selectors, and REST allow and deny method and path selectors must use ASCII literals in both the candidate and boundary. A non-ASCII literal in one of these fields returns unsupported with reason_code: unsupported_policy_shape, including when it appears only in a deny. Embedded NUL bytes in these fields are also unsupported. This is a prover-model limitation, not a general policy validation rule: filesystem paths and unrelated policy text retain their existing Unicode behavior. ASCII wildcard selectors still cover non-ASCII runtime values matched by the policy engine.

Containment means Allowed(candidate) is a subset of Allowed(boundary) under the reported model. It does not establish least privilege, automatic approval eligibility, semantic safety, or equivalence to a running sandbox’s kernel state. In particular:

• The command does not fetch the current sandbox policy or compose provider rules. The caller must supply the effective candidate.
• The command does not apply, approve, or persist a policy.
• Environment-dependent authority, such as an unresolved image workdir, returns unsupported when the result depends on that missing context.
• Binary comparisons that can change when an image resolves an exact selector through a symlink return unsupported. This covers exact candidate grants under boundary globs and exact boundary denies replaced by candidate globs. Use matching exact canonical paths when possible.
• Policies with overlapping L4 and enforced REST endpoints return unsupported because inspection selection depends on the complete set of matching runtime endpoint configurations.
• Network containment checks both supported runtime configurations: binary identity enforcement enabled and disabled. When enabled, grants and denies match the executable or an ancestor identity. Network counterexamples report the configuration and identities that expose the additional authority.
• REST containment witnesses use canonical request methods and paths.
• If a solver string cannot be decoded and validated faithfully, the command returns inconclusive with reason_code: invalid_witness instead of emitting a counterexample.
• Both files are interpreted in the same sandbox filesystem namespace and mount model, with stable path resolution when enforcement rules are created. The CLI does not resolve sandbox paths against the host.
• Filesystem containment supports removing grants and reducing write grants to read-only grants at matching paths. A boundary grant for / also covers other paths for the same access. Comparisons between different paths otherwise return unsupported with reason_code: unresolved_filesystem_path: a lexical child can resolve outside its parent through a symlink, and unrelated paths can resolve to the same object. This includes narrowing /tmp to /tmp/cache. If the boundary grants no access of the requested kind, adding that access returns exceeds_boundary.

Use the Policy Schema Reference for the full policy language. A successful prover result covers only the policy domains reported in its evidence.