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 maximum. 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.

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.

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 — a SandboxPolicy proto, parsed via openshell-policy::parse_sandbox_policy.
• 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.

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:

• 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.