OpenShell/crates/openshell-prover

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:

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.

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 entries:

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.