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.

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 (category, binary, host:port, 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 CLI renderer (report::render_compact / render_report) prints human-readable output for the openshell-prover binary.
• The gateway calls report::finding_shorthand to build the validation_result string persisted on each draft chunk.

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.