OpenShell/crates/openshell-prover/README.md

<!-- SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. -->
<!-- SPDX-License-Identifier: Apache-2.0 -->

# openshell-prover

Formal verifier for OpenShell sandbox policies. Encodes a policy + its
attached credential set + a binary capability registry as a Z3 SMT
model, then runs reachability queries to detect credentialed-reach and
capability changes a reviewer should be aware of.

The crate also exposes an independent containment API for checking whether a
fully composed candidate policy stays within an operator-supplied boundary. The
`openshell-prover-cli` package wraps that API for local files. Containment and
the legacy proposal-risk queries answer different questions; gateway callers
continue to use the proposal-risk API until the managed-policy migration.

Both prover entrypoints use the bounded `openshell-policy-schema` parser.
Containment rejects unknown fields and managed `metadata`/`review` annotations
as invalid input, then checks schema-valid controls against its supported model.
It uses shared filesystem defaults, port selection, and access-preset semantics.

The containment model accepts ASCII literals in network binary selectors,
endpoint host and path selectors, and REST allow and deny method and path
selectors. It returns `unsupported_policy_shape` when either policy uses a
non-ASCII literal in one of those fields. This boundary does not apply to
filesystem paths or unrelated policy text. Embedded NUL bytes in network
selector fields are also unsupported. ASCII wildcards are modeled over the
runtime match language and can therefore match non-ASCII runtime values. A
solver string that cannot be decoded and validated exactly produces
`invalid_witness` rather than counterexample evidence.

## Containment API compatibility

The containment module is a reusable Rust API, but this contract does not make
the entire `openshell-prover` crate a stable published SDK. Construct options
through `CheckOptions::new`, and accept a policy only when the result is
`CheckResult::Within`:

```rust
use std::time::Duration;
use openshell_prover::containment::{
    CheckOptions, CheckResult, check_within_boundary, parse_policy_str,
};

let boundary = parse_policy_str("version: 1\n")?;
let candidate = parse_policy_str("version: 1\n")?;
let result = check_within_boundary(
    &boundary,
    &candidate,
    CheckOptions::new(Duration::from_secs(10)),
);
let authorized = matches!(result, CheckResult::Within(_));
# Ok::<(), Box<dyn std::error::Error>>(())
```

`ReasonCode`, `CheckDomain`, `Protocol`, and `Counterexample` are open to new
variants. `CheckOptions`, `CheckCoverage`, `WithinEvidence`, and existing
counterexample variants are open to new fields. Match these types with `..`
and wildcard arms, use their accessors and `as_str()` identifiers, and treat
unknown values as a fail-closed result. Existing identifier strings are stable.

`CheckResult` is intentionally closed to the four states `Within`, `Exceeds`,
`Unsupported`, and `Inconclusive`. `FilesystemAccess` is likewise closed to
`Read` and `Write`. Adding a result state or filesystem access mode is a
breaking API change. Rust source compatibility is separate from the CLI JSON
schema contract. The CLI's numeric `schema_version` versions that JSON contract,
while `prover_version` identifies the implementation that produced a result.
The result's `coverage.domains` list is the machine-readable declaration of
modeled authority.

Used by the gateway to gate auto-approval of agent-authored policy
proposals: any finding blocks auto-approval, an empty delta lets the
chunk pass through (when the reviewer opts in via the
`proposal_approval_mode` setting at either gateway or sandbox scope).

## What it decides

The prover answers four formal questions. Each "yes" answer is its own
categorical finding — there is no severity grade. The categories live
in [`finding::category`](src/finding.rs).

| Category | Question the prover decides |
|---|---|
| `link_local_reach` | Does this policy grant reach to a host in `169.254.0.0/16` or `fe80::/10`? |
| `l7_bypass_credentialed` | Does it let a binary using a non-HTTP wire protocol (per the binary registry's `bypasses_l7` flag) reach a host where a credential is in scope? |
| `credential_reach_expansion` | Does it let a binary reach a (host, port) with a credential in scope, where the binary couldn't reach that endpoint before? |
| `capability_expansion` | On a (binary, host, port) the binary already reaches with credentials, does it add a new HTTP method? |

The first two are unconditional risks. The latter two are *delta*
properties — the gateway runs the prover on both the baseline policy
and the merged policy and surfaces only the new paths.

## Evidence shape

Each finding carries one or more [`FindingPath::Exfil`](src/finding.rs)
entries:

```rust
pub struct ExfilPath {
    pub binary: String,
    pub endpoint_host: String,
    pub endpoint_port: u16,
    pub mechanism: String,        // human-readable description
    pub policy_name: String,      // rule the path traverses
    pub category: String,         // one of the category constants
    pub method: String,           // populated for capability_expansion; empty otherwise
}
```

The gateway's `finding_delta` keys paths by `(finding query, binary,
host:port, path category, method)` so that adding a new method on an
already-reached host surfaces as exactly one new path (not the whole
re-emission of the existing method set).

### Category suppression at the delta layer

`capability_expansion` paths whose `(binary, host, port)` tuple is also
in the `credential_reach_expansion` delta are suppressed by the
gateway. A brand-new credentialed reach is described by the
reach-expansion finding alone, not also by N per-method findings.

## Adding a new category

1. Add a constant to `src/finding.rs::category`.
2. In `src/queries.rs::check_credential_safety`, add the branch that
   detects the new category and emits one `ExfilPath` per evidence
   row. Set `path.category` to the new constant.
3. In `src/report.rs::format_path_line`, add a `match` arm rendering
   the per-path display string the reviewer sees.
4. (Gateway) If the new category should be suppressed by another, add
   the suppression rule to `crates/openshell-server/src/grpc/policy.rs::finding_delta`.
5. Add a unit test in `src/queries.rs` and an integration test in
   `crates/openshell-server/src/grpc/policy.rs::tests`.

The four v1 categories cover the formal properties the OpenShell
auto-approval gate cares about today. Additional categories (e.g.,
"destructive method introduced," "new outbound TLS without SNI") would
be additive — they don't displace existing categories.

## What the prover does *not* decide

- **Semantic risk of an action.** The prover models *can the binary do
  this?*, not *is this destructive?*. `PUT /repos/.../contents/file.md`
  and `GET /repos/.../contents/file.md` are both authenticated actions;
  the reviewer (or a downstream layer like an LLM contextual reviewer
  or an intent file) decides if the action is desired.
- **Cross-sandbox or cross-binary intent.** The model is per-sandbox.
  If two sandboxes share a credential through external policy, the
  prover reasons about each independently.
- **Runtime behavior.** The prover analyzes the policy as written; it
  doesn't observe the proxy's actual decisions. The proxy is the
  enforcement layer; the prover is the change-review layer.

## Inputs

- **Policy** — authored YAML decoded by `openshell-policy-schema` with the shared
  fail-closed parser, then projected into the prover-only `PolicyModel`.
  Missing `version` and unknown authored fields are rejected consistently with
  runtime parsing. An absent `filesystem_policy` uses the runtime-effective
  `include_workdir: true`; an explicitly present empty object remains `false`.
  Explicit `protocol: tcp` is treated as L4, matching runtime classification.
- **Credential set** — built from the sandbox's attached providers in
  `crates/openshell-server/src/grpc/policy.rs::build_credential_set_for_sandbox`.
  v1 captures presence only (host-coarse); no scope modeling.
- **Binary registry** — YAML descriptors at
  `crates/openshell-prover/registry/binaries/*.yaml`. Each describes
  the binary's protocols, `bypasses_l7` flag, and `can_exfiltrate`
  capability.

Accepted-risk files, credential descriptors, and binary registries are
separate file formats. They continue to use their own serde definitions and do
not form part of the authored policy schema.

## Outputs

- A list of `Finding` values, one per fired category. Each finding's
  `query` field holds the category name.
- The legacy report renderers (`report::render_compact` / `render_report`)
  format proposal-risk findings for terminal consumers.
- The gateway calls `report::finding_shorthand` to build the
  `validation_result` string persisted on each draft chunk.
- The containment API returns typed evidence to `openshell-prover-cli`, which
  owns the standalone command's text and JSON formats and exit codes.

## Z3 model layout

See `src/model.rs`. Briefly:

- Endpoint facts are indexed by rule, endpoint position, and effective port.
  Sibling endpoints retain their own grants even when their destinations overlap.
- Query entrypoints return an error if the base constraints are inconsistent or
  the solver cannot reach a conclusion. Callers must propagate that error; it
  cannot be accepted as a finding or compared as an empty finding list.

- Bool sorts per `(binary, endpoint)` pair encode policy reachability,
  filtered by binary capability flags (`can_exfiltrate`,
  `bypasses_l7`).
- Bool sorts per `(binary, host)` encode credential-in-scope (one
  credential set per sandbox).
- The reachability formula composes these into the SAT query the
  `queries::check_credential_safety` loop iterates over.

## Tests

- Unit tests in each module (`src/queries.rs`, `src/report.rs`,
  `src/policy.rs`) cover individual primitives and category emission.
- Integration tests in `src/lib.rs::tests` exercise the full
  parse → build_model → run_all_queries pipeline against testdata
  policies in `testdata/`.
- Gateway-level acceptance tests in
  `crates/openshell-server/src/grpc/policy.rs::tests` lock in the
  end-to-end `validation_result` shape and the auto-approval gate.