* refactor(prover): remove legacy unused reachability constraints
Remove can_write_to_endpoint() and the solver variables and encoding
methods that exist solely to support it. No active query calls this
method; confirmed zero callers across the monorepo. Crate is not
published externally, so no public API concern.
Removed as root cause:
- can_write_to_endpoint(): zero callers in the codebase
Removed as direct consumers of can_write_to_endpoint():
- binary_can_write: only read inside can_write_to_endpoint()
- credential_has_write: only read inside can_write_to_endpoint()
Removed as directly dead (no query ever read them):
- credential_has_destructive: flagged by compiler, silenced with
#[allow(dead_code)] rather than removed
- filesystem_readable: flagged by compiler, silenced with
#[allow(dead_code)] rather than removed
Removed as now-empty encoding methods:
- encode_credentials(): exclusively populated credential_has_write
and credential_has_destructive
- encode_filesystem(): exclusively populated filesystem_readable
Also removed two #[allow(dead_code)] allowances and the corresponding
HashMap::new() initialisers and build() call sites.
Active query behavior is unchanged. All existing prover tests pass
without modification and cover all four finding categories end-to-end.
No new tests added as they would duplicate existing coverage exactly.
Note: removing encode_credentials() leaves write_actions_for_scopes()
and destructive_actions_for_scopes() in credentials.rs with no callers.
Left as a follow-up outside the scope of this change.
Closes#2412
Signed-off-by: Evie Howard <evhoward@redhat.com>
* refactor(prover): remove dead write-capability helpers from binary registry
BinaryProtocol::can_write(), BinaryCapability::can_write(), and
write_mechanisms() lost their only callers when can_write_to_endpoint()
and its supporting model fields were removed. Delete the now-dead methods.
write_mechanisms() had no callers prior to this series; the two can_write()
methods were made dead by the preceding model.rs cleanup.
Signed-off-by: Evie Howard <evhoward@redhat.com>
* docs(prover): remove stale write-bypass mention from module doc comment
The module doc incorrectly listed write-bypass violation detection as a
prover capability. The prover only checks reachability queries; write-bypass
detection was never implemented.
Signed-off-by: Evie Howard <evhoward@redhat.com>
---------
Signed-off-by: Evie Howard <evhoward@redhat.com>
* refactor(inference): remove managed inference routes
Closes#3172
Remove the inference route control plane, inference.local data path, built-in router crate, and SDK surface. Move inference workloads to explicitly imported provider profiles and native endpoints, with migration cleanup and updated tests and documentation.
Signed-off-by: John Myers <9696606+johntmyers@users.noreply.github.com>
* fix(policy): preserve alternate upstream isolation
Restore the provider policy activation guard so legacy OpenAI and Anthropic providers configured for alternate base URLs do not grant egress to the built-in public vendor endpoints.
Signed-off-by: John Myers <9696606+johntmyers@users.noreply.github.com>
---------
Signed-off-by: John Myers <9696606+johntmyers@users.noreply.github.com>
Establish the Phase 1 reference implementation proposed by RFC 0012
while retaining the existing Cargo and Mise workflows during evaluation.
- pin Bazel 9.1.1 and configure Bzlmod, rules_rs, LLVM, protobuf, and
Rust 1.95 toolchains
- import third-party crates from Cargo metadata and propagate the
workspace version into Bazel targets
- add library, binary, proc-macro, unit-test, and integration-test
targets across the supported Rust workspace crates and drivers
- generate protobuf Rust sources and descriptor sets under Bazel while
preserving Cargo-compatible generated-code imports
- annotate aws-lc-sys and zstd-sys native dependencies, build Z3 4.15.2
from source, and generate z3-sys bindings
- make CLI and procfs test fixtures available as explicit Bazel inputs
without relying on fixed host binary paths
- define optimized release targets for Linux x86_64 and aarch64 CLI,
sandbox, and gateway binaries, plus macOS aarch64 artifacts
- add Bazel, buildifier, and lcov to the Nix development environment
RFC: 0012 (rfc12 branch)
Refs: #2491
Signed-off-by: Simon Scatton <sscatton@nvidia.com>
Add gateway-managed AWS STS credential refresh (provider-v2, #1576). The
gateway calls sts:AssumeRole and writes three short-lived credentials
(AWS_ACCESS_KEY_ID, AWS_SECRET_ACCESS_KEY, AWS_SESSION_TOKEN) to the
provider record; the proxy re-signs requests with SigV4. Adds the aws and
aws-s3 provider profiles and a declarative multi-output refresh model
(additional_outputs) so one AssumeRole co-mints all three credentials.
Signed-off-by: Russell Bryant <rbryant@redhat.com>
* feat(prover): add native Rust policy prover with Z3 solver
Add openshell-prover crate implementing formal policy verification
using Z3 SMT solving. Answers two questions about any sandbox policy:
"Can data leave?" and "Can the agent write despite read-only intent?"
Native Rust — no Python subprocess, no PYTHONPATH, no uv dependency.
Z3 bundled via z3-sys for self-contained builds.
Replaces the Python prototype from #703.
Closes#699
Signed-off-by: Alexander Watson <zredlined@gmail.com>
* fix(prover): skip L7-write in exfil, write bypass only on read-only intent
Port two fixes from the Python branch:
- Exfil query skips endpoints where L7 is enforced and working
- Write bypass only fires on explicit read-only intent, not L4-only
Signed-off-by: Alexander Watson <zredlined@gmail.com>
* chore(prover): add missing SPDX license headers to registry and testdata YAML files
* fix(prover): revert serde_yaml to serde_yml to match workspace dependency on main
* fix(prover): apply cargo fmt formatting to prover and cli source files
* ci: add clang and libclang-dev to CI image for z3-sys bindgen
z3-sys requires libclang at build time for bindgen to generate FFI
bindings. Without it, the Rust CI jobs fail on the prover crate.
* fix(prover): use system libz3 instead of compiling from source
Add libz3-dev to the CI image and drop the z3 `bundled` feature from
the workspace dependency. This eliminates the ~30 min z3 C++ build
that ran on every CI cache miss.
sccache only wraps rustc — it does not intercept the cmake C++ build
that z3-sys runs when `bundled` is enabled. The cargo target cache
helped on warm runs but evicts on toolchain bumps and fork PRs.
With the system library pre-installed in the CI image, z3 link time
is always zero.
A `bundled-z3` opt-in feature is added to the prover crate for local
development without system z3:
cargo build -p openshell-prover --features bundled-z3
Regular local dev: brew install z3 (macOS) or apt install libz3-dev
(Linux), then cargo build just works.
Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor
* fix(prover): use u16 for ports, align include_workdir default with runtime
Port fields changed from u32 to u16 across all prover types (policy,
model, finding, queries). Prevents the prover from silently accepting
port values >65535 that the runtime rejects, which would produce
misleading PASS results on invalid policies.
Change include_workdir serde default from true to false to match the
runtime (openshell-policy uses #[serde(default)] which gives false).
The previous mismatch caused the prover to model a /sandbox path that
does not exist at runtime, producing false analysis.
Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor
* refactor(prover): embed registry at compile time, replace hand-rolled glob
Embed binary and API capability registry YAML files into the binary at
compile time using include_dir!. The previous approach used
env!("CARGO_MANIFEST_DIR") which bakes in the build machine's source
path — works in tests but breaks for installed binaries. The CWD
fallback was equally fragile.
The --registry CLI flag still works as a filesystem override for custom
registries. Credentials remain filesystem-loaded (user-supplied data).
Replace the hand-rolled glob matching (~60 lines) with the glob crate's
Pattern::matches(), which is already a transitive dependency.
Remove unused dependencies: openshell-policy, openshell-core, thiserror,
tracing. The prover parses policy YAML directly into its own types and
does not use the policy or core crate APIs.
Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor
* docs: add Z3 system library to prerequisites
The prover crate now links against system libz3 instead of compiling
from source. Document the install steps for macOS, Ubuntu, and Fedora,
and note the bundled-z3 feature flag as a fallback.
Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor
* fix(prover): apply cargo fmt formatting
Made-with: Cursor
---------
Signed-off-by: Alexander Watson <zredlined@gmail.com>
Evie Howard