From 680906ecd6beaceead79a49d4d47f12adc54a949 Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 18:45:06 +0000 Subject: [PATCH 01/12] feat(prover): add standalone policy maximum checker Signed-off-by: Johnny Greco --- .github/workflows/branch-checks.yml | 19 + .github/workflows/build-prover-binaries.yml | 42 + .../workflows/package-release-binaries.yml | 96 + .github/workflows/release-dev.yml | 28 +- .github/workflows/release-tag.yml | 31 +- AGENTS.md | 1 + CONTRIBUTING.md | 13 +- Cargo.lock | 15 + Cargo.toml | 1 + architecture/build.md | 13 +- architecture/security-policy.md | 30 +- crates/openshell-prover-cli/Cargo.toml | 32 + crates/openshell-prover-cli/README.md | 34 + crates/openshell-prover-cli/src/main.rs | 571 ++++ crates/openshell-prover-cli/tests/cli.rs | 304 +++ .../tests/fixtures/candidate-contained.yaml | 9 + .../tests/fixtures/candidate-exceeds.yaml | 9 + .../tests/fixtures/invalid.yaml | 4 + .../tests/fixtures/maximum.yaml | 10 + .../tests/fixtures/unsupported.yaml | 6 + crates/openshell-prover/Cargo.toml | 5 + crates/openshell-prover/README.md | 12 +- crates/openshell-prover/src/containment.rs | 2293 +++++++++++++++++ crates/openshell-prover/src/lib.rs | 1 + .../openshell-prover/tests/runtime_parity.rs | 283 ++ .../openshell-supervisor-network/src/opa.rs | 88 + docs/reference/policy-prover.mdx | 160 ++ 27 files changed, 4099 insertions(+), 11 deletions(-) create mode 100644 .github/workflows/build-prover-binaries.yml create mode 100644 crates/openshell-prover-cli/Cargo.toml create mode 100644 crates/openshell-prover-cli/README.md create mode 100644 crates/openshell-prover-cli/src/main.rs create mode 100644 crates/openshell-prover-cli/tests/cli.rs create mode 100644 crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml create mode 100644 crates/openshell-prover-cli/tests/fixtures/candidate-exceeds.yaml create mode 100644 crates/openshell-prover-cli/tests/fixtures/invalid.yaml create mode 100644 crates/openshell-prover-cli/tests/fixtures/maximum.yaml create mode 100644 crates/openshell-prover-cli/tests/fixtures/unsupported.yaml create mode 100644 crates/openshell-prover/src/containment.rs create mode 100644 crates/openshell-prover/tests/runtime_parity.rs create mode 100644 docs/reference/policy-prover.mdx diff --git a/.github/workflows/branch-checks.yml b/.github/workflows/branch-checks.yml index 7b0c77c8fd..caccd0e87b 100644 --- a/.github/workflows/branch-checks.yml +++ b/.github/workflows/branch-checks.yml @@ -173,6 +173,25 @@ jobs: run: | cargo nextest run --profile ci --workspace --features openshell-server/test-support + - name: Verify standalone policy prover package + if: matrix.system == 'x86_64-linux' + env: + CARGO_NET_OFFLINE: "true" + run: | + cargo test --locked -p openshell-prover-cli + cargo build --locked --release -p openshell-prover-cli --bin openshell-prover + cargo tree --locked -p openshell-prover-cli --edges normal --prefix none > /tmp/openshell-prover-dependencies.txt + if grep -Eq '^(openshell-(cli|server|sdk|bootstrap|tui|providers|core|policy)) v' /tmp/openshell-prover-dependencies.txt; then + echo "ERROR: standalone prover includes an OpenShell control-plane dependency" >&2 + cat /tmp/openshell-prover-dependencies.txt >&2 + exit 1 + fi + target/release/openshell-prover check \ + crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml \ + --maximum crates/openshell-prover-cli/tests/fixtures/maximum.yaml \ + --output json > /tmp/openshell-prover-result.json + grep -q '"result"[[:space:]]*:[[:space:]]*"within_max"' /tmp/openshell-prover-result.json + - name: Verify telemetry can be compiled out run: | cargo build -p openshell-gateway --bin openshell-gateway diff --git a/.github/workflows/build-prover-binaries.yml b/.github/workflows/build-prover-binaries.yml new file mode 100644 index 0000000000..22fd96a97a --- /dev/null +++ b/.github/workflows/build-prover-binaries.yml @@ -0,0 +1,42 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +name: Build Prover Binaries + +on: + workflow_call: + inputs: + cargo-version: + required: true + type: string + checkout-ref: + required: false + type: string + default: "" + secrets: + CACHIX_AUTH_TOKEN: + required: true + +permissions: + contents: read + +jobs: + build: + strategy: + matrix: + include: + - triple: x86_64-unknown-linux-musl + runner: linux-amd64-cpu8 + - triple: aarch64-unknown-linux-musl + runner: linux-arm64-cpu8 + - triple: aarch64-apple-darwin + runner: macos-15-xlarge + uses: ./.github/workflows/build-binaries.yml + with: + package: openshell-prover-cli + binary: openshell-prover + triple: ${{ matrix.triple }} + runner: ${{ matrix.runner }} + cargo-version: ${{ inputs.cargo-version }} + checkout-ref: ${{ inputs.checkout-ref }} + secrets: inherit diff --git a/.github/workflows/package-release-binaries.yml b/.github/workflows/package-release-binaries.yml index f1900f3c35..fc791f9f48 100644 --- a/.github/workflows/package-release-binaries.yml +++ b/.github/workflows/package-release-binaries.yml @@ -5,6 +5,11 @@ name: Package Release Binaries on: workflow_call: + inputs: + checkout-ref: + required: false + type: string + default: "" permissions: actions: read @@ -52,6 +57,15 @@ jobs: - artifact: openshell-driver-vm-aarch64-apple-darwin binary: openshell-driver-vm package: driver-vm-macos + - artifact: openshell-prover-x86_64-unknown-linux-musl + binary: openshell-prover + package: prover-binary-linux-amd64 + - artifact: openshell-prover-aarch64-unknown-linux-musl + binary: openshell-prover + package: prover-binary-linux-arm64 + - artifact: openshell-prover-aarch64-apple-darwin + binary: openshell-prover + package: prover-binary-macos steps: - name: Download ${{ matrix.artifact }} uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 @@ -75,3 +89,85 @@ jobs: path: ${{ matrix.artifact }}.tar.gz retention-days: 5 if-no-files-found: error + + smoke-prover: + name: Smoke packaged prover (${{ matrix.triple }}) + needs: package + runs-on: ${{ matrix.runner }} + timeout-minutes: 10 + strategy: + fail-fast: false + matrix: + include: + - triple: x86_64-unknown-linux-musl + runner: linux-amd64-cpu8 + package: prover-binary-linux-amd64 + - triple: aarch64-unknown-linux-musl + runner: linux-arm64-cpu8 + package: prover-binary-linux-arm64 + - triple: aarch64-apple-darwin + runner: macos-15-xlarge + package: prover-binary-macos + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + ref: ${{ inputs['checkout-ref'] || github.sha }} + + - name: Download packaged prover + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: ${{ matrix.package }} + path: package + + - name: Extract and run containment check + env: + TRIPLE: ${{ matrix.triple }} + run: | + set -euo pipefail + mkdir extracted + tar -xzf "package/openshell-prover-${TRIPLE}.tar.gz" -C extracted + test "$(find extracted -type f | wc -l | tr -d ' ')" = 1 + test -x extracted/openshell-prover + if [ "${RUNNER_OS}" = "Linux" ]; then + tasks/scripts/verify-static-binary.sh extracted/openshell-prover + else + otool -L extracted/openshell-prover | tee linkage.txt + if grep -Eiq 'libz3|/nix/store' linkage.txt; then + echo "ERROR: packaged prover has a non-portable native dependency" >&2 + exit 1 + fi + fi + extracted/openshell-prover check \ + crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml \ + --maximum crates/openshell-prover-cli/tests/fixtures/maximum.yaml \ + --output json > result.json + grep -q '"result"[[:space:]]*:[[:space:]]*"within_max"' result.json + + prover-checksums: + name: Package prover checksums + needs: smoke-prover + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - name: Download packaged prover archives + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + pattern: prover-binary-* + path: release + merge-multiple: true + + - name: Generate prover checksums + run: | + set -euo pipefail + cd release + sha256sum openshell-prover-*.tar.gz > openshell-prover-checksums-sha256.txt + test "$(awk 'END { print NR }' openshell-prover-checksums-sha256.txt)" = 3 + sha256sum --check openshell-prover-checksums-sha256.txt + + - name: Upload prover checksums + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 + with: + name: prover-checksums + path: release/openshell-prover-checksums-sha256.txt + retention-days: 5 + if-no-files-found: error diff --git a/.github/workflows/release-dev.yml b/.github/workflows/release-dev.yml index fb364b4e13..b411674448 100644 --- a/.github/workflows/release-dev.yml +++ b/.github/workflows/release-dev.yml @@ -89,6 +89,15 @@ jobs: cargo-version: ${{ needs.compute-versions.outputs.cargo_version }} secrets: inherit + build-prover: + needs: compute-versions + permissions: + contents: read + uses: ./.github/workflows/build-prover-binaries.yml + with: + cargo-version: ${{ needs.compute-versions.outputs.cargo_version }} + secrets: inherit + build-gateway: needs: compute-versions permissions: @@ -120,7 +129,7 @@ jobs: secrets: inherit package-binaries: - needs: [build-cli, build-gateway, build-sandbox, build-vm-driver] + needs: [build-cli, build-prover, build-gateway, build-sandbox, build-vm-driver] permissions: actions: read contents: read @@ -410,6 +419,19 @@ jobs: path: release/ merge-multiple: true + - name: Download prover binary artifacts + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + pattern: prover-binary-* + path: release/ + merge-multiple: true + + - name: Download prover checksums + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: prover-checksums + path: release/ + - name: Download wheel artifact uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 with: @@ -607,11 +629,15 @@ jobs: release/openshell-driver-vm-x86_64-unknown-linux-gnu.tar.gz release/openshell-driver-vm-aarch64-unknown-linux-gnu.tar.gz release/openshell-driver-vm-aarch64-apple-darwin.tar.gz + release/openshell-prover-x86_64-unknown-linux-musl.tar.gz + release/openshell-prover-aarch64-unknown-linux-musl.tar.gz + release/openshell-prover-aarch64-apple-darwin.tar.gz release/*.whl release/openshell.rb release/openshell-checksums-sha256.txt release/openshell-gateway-checksums-sha256.txt release/openshell-sandbox-checksums-sha256.txt + release/openshell-prover-checksums-sha256.txt release-helm: name: Release Helm Chart (OCI, dev) diff --git a/.github/workflows/release-tag.yml b/.github/workflows/release-tag.yml index 962d846407..66ef2803eb 100644 --- a/.github/workflows/release-tag.yml +++ b/.github/workflows/release-tag.yml @@ -118,6 +118,16 @@ jobs: checkout-ref: ${{ inputs.tag || github.ref }} secrets: inherit + build-prover: + needs: compute-versions + permissions: + contents: read + uses: ./.github/workflows/build-prover-binaries.yml + with: + cargo-version: ${{ needs.compute-versions.outputs.cargo_version }} + checkout-ref: ${{ inputs.tag || github.ref }} + secrets: inherit + build-gateway: needs: compute-versions permissions: @@ -152,11 +162,13 @@ jobs: secrets: inherit package-binaries: - needs: [build-cli, build-gateway, build-sandbox, build-vm-driver] + needs: [build-cli, build-prover, build-gateway, build-sandbox, build-vm-driver] permissions: actions: read contents: read uses: ./.github/workflows/package-release-binaries.yml + with: + checkout-ref: ${{ inputs.tag || github.ref }} build-gateway-image: needs: [compute-versions, build-gateway] @@ -506,6 +518,19 @@ jobs: path: release/ merge-multiple: true + - name: Download prover binary artifacts + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + pattern: prover-binary-* + path: release/ + merge-multiple: true + + - name: Download prover checksums + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: prover-checksums + path: release/ + - name: Download wheel artifact uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 with: @@ -645,11 +670,15 @@ jobs: release/openshell-driver-vm-x86_64-unknown-linux-gnu.tar.gz release/openshell-driver-vm-aarch64-unknown-linux-gnu.tar.gz release/openshell-driver-vm-aarch64-apple-darwin.tar.gz + release/openshell-prover-x86_64-unknown-linux-musl.tar.gz + release/openshell-prover-aarch64-unknown-linux-musl.tar.gz + release/openshell-prover-aarch64-apple-darwin.tar.gz release/*.whl release/openshell.rb release/openshell-checksums-sha256.txt release/openshell-gateway-checksums-sha256.txt release/openshell-sandbox-checksums-sha256.txt + release/openshell-prover-checksums-sha256.txt - name: Upload pre-release artifacts if: needs.compute-versions.outputs.is_prerelease == 'true' diff --git a/AGENTS.md b/AGENTS.md index 954ffe1147..22ac9396cc 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -60,6 +60,7 @@ These pipelines connect skills into end-to-end workflows. Individual skill files | `crates/openshell-driver-vm/` | VM compute driver | Standalone libkrun-backed `ComputeDriver` subprocess (embeds its own rootfs + runtime) | | `crates/openshell-driver-mxc/` | Microsoft MXC compute driver | In-process Windows AppContainer and isolation-session compute backend | | `crates/openshell-prover/` | Policy prover | Policy verification and proof generation | +| `crates/openshell-prover-cli/` | Policy prover CLI | Standalone local maximum-boundary checks | | `crates/openshell-server-macros/` | Server macros | Compile-time helpers for gateway RPC authorization | | `crates/openshell-supervisor-middleware/` | Middleware runtime | Generic middleware registry, remote service integration, and chain execution | | `crates/openshell-supervisor-middleware-builtins/` | Built-in middleware | First-party in-process middleware implementations | diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 931d97500f..7fe523d021 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -313,11 +313,12 @@ Project requirements: ### Z3 installation -The `openshell-prover` crate links directly against Z3. The `openshell-server` -crate depends on the prover, and the `openshell-gateway` binary crate depends -on `openshell-server` in turn; both forward a `bundled-z3` feature down to -`openshell-prover/bundled-z3`. The `openshell-cli` crate does not depend on -Z3. On macOS and Linux, install the system Z3 development package; `z3-sys` +The `openshell-prover` crate and standalone `openshell-prover-cli` binary link +directly against Z3. The `openshell-server` crate depends on the prover, and +the `openshell-gateway` binary crate depends on `openshell-server` in turn. +These packages forward a `bundled-z3` feature to +`openshell-prover/bundled-z3`. The `openshell-cli` crate does not depend on Z3. +On macOS and Linux, install the system Z3 development package; `z3-sys` discovers it through `pkg-config`. ```bash @@ -336,6 +337,7 @@ compiles Z3 from source during the Rust build and requires CMake 3.16+: ```bash cargo build -p openshell-prover --features bundled-z3 +cargo build -p openshell-prover-cli --features bundled-z3 ``` For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths: @@ -458,6 +460,7 @@ These are the primary `mise` tasks for day-to-day development: | Path | Purpose | | --------------- | --------------------------------------------- | | `crates/` | Rust crates | +| `crates/openshell-prover-cli/` | Standalone local policy maximum checker | | `python/` | Python SDK and bindings | | `sdk/go/` | Go SDK (types, gRPC clients, converters) | | `sdk/typescript/` | TypeScript SDK (Connect client and generated protobuf bindings) | diff --git a/Cargo.lock b/Cargo.lock index c633b7f26c..52141b46f3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4412,11 +4412,26 @@ dependencies = [ "include_dir", "miette", "noyalib", + "openshell-core", "owo-colors", + "regorus", "serde", + "serde_json", "z3", ] +[[package]] +name = "openshell-prover-cli" +version = "0.0.0" +dependencies = [ + "clap", + "nix 0.29.0", + "openshell-prover", + "serde", + "serde_json", + "signal-hook", +] + [[package]] name = "openshell-providers" version = "0.0.0" diff --git a/Cargo.toml b/Cargo.toml index 9fbcc9a8c8..f16e268e7d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -138,6 +138,7 @@ k8s-openapi = { version = "0.24", features = ["v1_29"] } # IDs uuid = { version = "1.10", features = ["v4"] } +signal-hook = "0.3" # SMT solver (uses system libz3; enable z3/bundled via the prover's bundled-z3 feature for local dev without system z3) z3 = "0.20" diff --git a/architecture/build.md b/architecture/build.md index a5dcfe9241..4390fffd07 100644 --- a/architecture/build.md +++ b/architecture/build.md @@ -13,6 +13,7 @@ OpenShell builds these main artifacts: | Gateway binary | `crates/openshell-gateway` | | CLI binaries and system packages | `crates/openshell-cli` plus release packaging | | E2E conformance CLI | `crates/openshell-conformance-cli` | +| Standalone policy prover | `crates/openshell-prover-cli` | | Python SDK wheel | `python/openshell` | | TypeScript SDK package | `sdk/typescript` | | Gateway container image | `deploy/docker/Dockerfile.gateway` | @@ -85,6 +86,14 @@ HTTP/TLS support behind explicit build features, so default system-Z3 builds do not reintroduce bundled Mozilla roots. Release builds that need bundled Z3 continue to opt in with `bundled-z3`. +The standalone `openshell-prover` executable is distributed independently of +the main CLI. Release workflows build Linux musl x86_64 and aarch64 binaries +and a macOS Apple Silicon binary, then publish one archive per target plus a +dedicated SHA-256 manifest. Before publication, target-native jobs extract each +archive, reject host Z3 or Nix store linkage, and run a real local containment +check. The tool therefore requires neither an OpenShell installation nor a +separately installed Z3 runtime. + ## Linux Runtime Environments OpenShell uses different Linux libc environments for different host artifacts. @@ -191,7 +200,9 @@ attestation below, which describes a published image. The shared binary build action uses the default Nix shell and compiles release artifacts with `cargo auditable build --target `. Verification and upload -read binaries from `target//release/`. +read binaries from `target//release/`. The standalone prover uses this +same action, while its package workflow adds target-native extracted-archive +linkage and containment smoke checks before producing its checksum manifest. Branch E2E, Release Dev, and Release Tag image jobs stage those same artifacts instead of rebuilding binaries in Docker. Each binary build scans its output with Syft and requires at least one decoded Cargo package before uploading the diff --git a/architecture/security-policy.md b/architecture/security-policy.md index 2f1fd2ea1d..a6e222d448 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -335,7 +335,35 @@ may store such a draft, but existing merge validation rejects it when an approval attempts to add it to policy; runtime SSRF protections remain the final enforcement boundary. -## What the prover decides +## Standalone maximum-boundary checks + +The standalone `openshell-prover check` command compares a fully composed local +candidate policy with an operator-supplied local maximum. It establishes +`Allowed(candidate) ⊆ Allowed(maximum)` for the model scope reported in its +result. It does not fetch gateway state, compose provider rules, apply policy, +or decide whether an in-boundary change is eligible for automatic approval. + +The initial maximum-boundary model covers filesystem paths, L4 network +authority, and enforced REST method and path authority, including explicit REST +denies. Network containment covers runtime configurations both with and without +binary identity enforcement. Strict checks match grants and denies against the +executable and an ancestor identity, and the evidence identifies the identities +for an exceeding witness. Recognized authority outside the reviewed model +produces an unsupported result rather than being silently ignored. +Environment-dependent authority also remains unsupported when the result +depends on context that is unavailable to the local command. This includes an +unresolved workdir, binary containment that depends on image-specific symlink +resolution, and overlapping L4 and REST endpoints whose inspection selection +depends on the complete runtime endpoint set. Candidate and maximum paths use +the same sandbox namespace and mount interpretation; the checker does not +resolve them against the CLI host or verify kernel enforcement in a running +sandbox. + +This containment operation is separate from the proposal-risk queries below. +See the [standalone policy prover documentation](../docs/reference/policy-prover.mdx) +for installation, command behavior, evidence, and exit codes. + +## What the proposal prover decides The prover answers four formal questions about each proposed policy change. Each "yes" answer becomes its own categorical finding — there is diff --git a/crates/openshell-prover-cli/Cargo.toml b/crates/openshell-prover-cli/Cargo.toml new file mode 100644 index 0000000000..f2fb4304cc --- /dev/null +++ b/crates/openshell-prover-cli/Cargo.toml @@ -0,0 +1,32 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +[package] +name = "openshell-prover-cli" +description = "Standalone OpenShell policy maximum checker" +version.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true +repository.workspace = true + +[[bin]] +name = "openshell-prover" +path = "src/main.rs" + +[features] +bundled-z3 = ["openshell-prover/bundled-z3"] +prebuilt-z3 = ["openshell-prover/prebuilt-z3"] + +[dependencies] +clap.workspace = true +openshell-prover = { path = "../openshell-prover" } +serde.workspace = true +serde_json.workspace = true + +[target.'cfg(unix)'.dependencies] +nix.workspace = true +signal-hook.workspace = true + +[lints] +workspace = true diff --git a/crates/openshell-prover-cli/README.md b/crates/openshell-prover-cli/README.md new file mode 100644 index 0000000000..bdd99335b8 --- /dev/null +++ b/crates/openshell-prover-cli/README.md @@ -0,0 +1,34 @@ + + +# OpenShell policy prover CLI + +This package builds the standalone `openshell-prover` executable. It is a thin synchronous adapter around the reusable containment engine in `openshell-prover`; it owns local file loading, command parsing, result rendering, and process exit codes. + +```shell +openshell-prover check candidate.yaml --maximum maximum.yaml +openshell-prover check candidate.yaml --maximum maximum.yaml --output json +``` + +The command checks whether a fully composed candidate policy stays within an operator-supplied maximum. It does not discover a gateway, fetch policy state, or apply policy changes. + +Results use these exit codes: + +| Exit code | Meaning | +| --- | --- | +| `0` | The candidate is within the maximum. | +| `1` | The candidate exceeds the maximum. | +| `2` | Usage, input, output, or internal error. | +| `3` | Unsupported policy semantics or an inconclusive solve. | +| `130` | Interrupted with Ctrl-C on Unix; graceful JSON output reports an inconclusive cancellation. | + +Build and test the package with: + +```shell +cargo build -p openshell-prover-cli --bin openshell-prover +cargo test -p openshell-prover-cli +``` + +See the [policy prover reference](../../docs/reference/policy-prover.mdx) for installed usage and interpretation guidance. diff --git a/crates/openshell-prover-cli/src/main.rs b/crates/openshell-prover-cli/src/main.rs new file mode 100644 index 0000000000..4b3139aa48 --- /dev/null +++ b/crates/openshell-prover-cli/src/main.rs @@ -0,0 +1,571 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Standalone policy maximum checker. + +#[cfg(not(unix))] +use std::fs::File; +#[cfg(unix)] +use std::fs::OpenOptions; +use std::io::{self, Read, Write}; +use std::path::{Path, PathBuf}; +use std::process::ExitCode; +use std::sync::Arc; +use std::sync::atomic::{AtomicBool, Ordering}; +use std::time::Duration; + +use clap::{CommandFactory, Parser, Subcommand, ValueEnum}; +use openshell_prover::containment::{ + CheckOptions, CheckResult, CheckScope, ContainmentPolicy, Counterexample, parse_policy_str, +}; +use serde::Serialize; + +const MAX_POLICY_BYTES: u64 = 4 * 1024 * 1024; + +#[derive(Debug, Parser)] +#[command( + name = "openshell-prover", + about = "Verify OpenShell policy boundaries", + version +)] +struct Cli { + #[command(subcommand)] + command: Option, +} + +#[derive(Debug, Subcommand)] +enum Command { + /// Check whether a candidate policy is contained within a maximum policy. + Check { + /// Fully composed effective candidate policy. + candidate: PathBuf, + /// Operator-owned maximum policy. + #[arg(long, value_name = "FILE")] + maximum: PathBuf, + /// Result output format. + #[arg(short, long, value_enum, default_value_t = OutputFormat::Text)] + output: OutputFormat, + /// Solver time budget (integer followed by ms, s, or m). + #[arg(long, default_value = "10s", value_parser = parse_duration)] + timeout: Duration, + }, +} + +#[derive(Clone, Copy, Debug, Eq, PartialEq, ValueEnum)] +enum OutputFormat { + Text, + Json, +} + +#[derive(Debug, Serialize)] +struct Envelope<'a> { + schema_version: u32, + prover_version: &'static str, + check: &'static str, + scope: Option>, + result: &'static str, + exit_code: u8, + inputs: InputsJson, + counterexample: Option>, + reason_code: Option<&'a str>, + reason: Option<&'a str>, +} + +#[derive(Debug, Serialize)] +struct ScopeJson<'a> { + model_version: &'a str, + policy_version: u32, + domains: Vec<&'a str>, + assumptions: &'a [&'a str], +} + +#[derive(Debug, Serialize)] +struct InputsJson { + candidate: String, + maximum: String, +} + +#[derive(Debug, Serialize)] +#[serde(tag = "domain", rename_all = "snake_case")] +enum CounterexampleJson<'a> { + Filesystem { + access: &'a str, + path: &'a str, + }, + Network { + binary: Option<&'a str>, + ancestor_binary: Option<&'a str>, + binary_identity_required: bool, + host: &'a str, + port: u16, + protocol: &'a str, + method: Option<&'a str>, + path: Option<&'a str>, + }, +} + +fn main() -> ExitCode { + let cancelled = Arc::new(AtomicBool::new(false)); + #[cfg(unix)] + if let Err(error) = + signal_hook::flag::register(signal_hook::consts::signal::SIGINT, Arc::clone(&cancelled)) + { + let _ = writeln!( + io::stderr().lock(), + "openshell-prover: cannot install Ctrl-C handler: {error}" + ); + return ExitCode::from(2); + } + let cli = Cli::parse(); + let outcome = cli + .command + .map_or_else(show_help, |command| execute(command, &cancelled)); + + match outcome { + Ok(code) => ExitCode::from(code), + Err(error) => { + let _ = writeln!(io::stderr().lock(), "openshell-prover: {error}"); + ExitCode::from(2) + } + } +} + +fn show_help() -> Result { + Cli::command() + .print_help() + .map_err(|error| format!("failed to write help: {error}"))?; + writeln!(io::stdout().lock()).map_err(|error| format!("failed to write output: {error}"))?; + Ok(0) +} + +fn execute(command: Command, cancelled: &AtomicBool) -> Result { + match command { + Command::Check { + candidate, + maximum, + output, + timeout, + } => check(&candidate, &maximum, output, timeout, cancelled), + } +} + +fn check( + candidate_path: &Path, + maximum_path: &Path, + output: OutputFormat, + timeout: Duration, + cancelled: &AtomicBool, +) -> Result { + let inputs = InputsJson { + candidate: candidate_path.to_string_lossy().into_owned(), + maximum: maximum_path.to_string_lossy().into_owned(), + }; + + let candidate_source = match read_policy(candidate_path) { + Ok(source) => source, + Err(error) => return render_input_error(output, inputs, &error), + }; + if cancelled.load(Ordering::Relaxed) { + return render_cancelled(output, inputs); + } + let maximum_source = match read_policy(maximum_path) { + Ok(source) => source, + Err(error) => return render_input_error(output, inputs, &error), + }; + if cancelled.load(Ordering::Relaxed) { + return render_cancelled(output, inputs); + } + let candidate = match parse_input("candidate", &candidate_source) { + Ok(policy) => policy, + Err(error) => return render_input_error(output, inputs, &error), + }; + let maximum = match parse_input("maximum", &maximum_source) { + Ok(policy) => policy, + Err(error) => return render_input_error(output, inputs, &error), + }; + if cancelled.load(Ordering::Relaxed) { + return render_cancelled(output, inputs); + } + + let result = openshell_prover::containment::check_within_maximum_cancellable( + &maximum, + &candidate, + CheckOptions { timeout }, + cancelled, + ); + let envelope = result_envelope(&result, inputs); + render(output, &envelope)?; + Ok(envelope.exit_code) +} + +fn parse_input(label: &str, source: &str) -> Result { + parse_policy_str(source).map_err(|error| { + format!( + "invalid {label} policy: {}", + escape_terminal(&error.to_string()) + ) + }) +} + +fn read_policy(path: &Path) -> Result { + // Reject unsupported inputs before opening them where possible. On Unix, + // also use O_NONBLOCK to close the replacement race between this check and + // open(): opening a FIFO must never hang the CLI before cancellation can be + // observed. O_NONBLOCK has no effect on reads from regular files. + let path_metadata = path.metadata().map_err(|error| { + format!( + "cannot open '{}': {error}", + escape_terminal(&path.to_string_lossy()) + ) + })?; + if !path_metadata.is_file() { + return Err(format!( + "policy path '{}' is not a regular file", + escape_terminal(&path.to_string_lossy()) + )); + } + + #[cfg(unix)] + let open_result = { + use std::os::unix::fs::OpenOptionsExt as _; + OpenOptions::new() + .read(true) + .custom_flags(nix::libc::O_NONBLOCK) + .open(path) + }; + #[cfg(not(unix))] + let open_result = File::open(path); + + let mut file = open_result.map_err(|error| { + format!( + "cannot open '{}': {error}", + escape_terminal(&path.to_string_lossy()) + ) + })?; + let metadata = file + .metadata() + .map_err(|error| format!("cannot inspect policy file: {error}"))?; + if !metadata.is_file() { + return Err(format!( + "policy path '{}' is not a regular file", + escape_terminal(&path.to_string_lossy()) + )); + } + if metadata.len() > MAX_POLICY_BYTES { + return Err(format!( + "policy file exceeds the {MAX_POLICY_BYTES}-byte input limit" + )); + } + + let mut bytes = Vec::new(); + Read::by_ref(&mut file) + .take(MAX_POLICY_BYTES + 1) + .read_to_end(&mut bytes) + .map_err(|error| format!("cannot read policy file: {error}"))?; + if u64::try_from(bytes.len()).unwrap_or(u64::MAX) > MAX_POLICY_BYTES { + return Err(format!( + "policy file exceeds the {MAX_POLICY_BYTES}-byte input limit" + )); + } + String::from_utf8(bytes).map_err(|_| "policy file is not valid UTF-8".to_owned()) +} + +fn render_input_error( + output: OutputFormat, + inputs: InputsJson, + reason: &str, +) -> Result { + if output == OutputFormat::Json { + let envelope = Envelope { + schema_version: 1, + prover_version: env!("CARGO_PKG_VERSION"), + check: "maximum_boundary", + scope: None, + result: "error", + exit_code: 2, + inputs, + counterexample: None, + reason_code: Some("invalid_input"), + reason: Some(reason), + }; + render(output, &envelope)?; + } else { + writeln!(io::stderr().lock(), "openshell-prover: {reason}") + .map_err(|error| format!("failed to write diagnostic: {error}"))?; + } + Ok(2) +} + +fn render_cancelled(output: OutputFormat, inputs: InputsJson) -> Result { + let result = CheckResult::cancelled(); + let envelope = result_envelope(&result, inputs); + render(output, &envelope)?; + Ok(envelope.exit_code) +} + +fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Envelope<'_> { + let (scope, result_name, exit_code, counterexample, reason_code, reason) = match result { + CheckResult::Within(evidence) => (evidence.scope(), "within_max", 0, None, None, None), + CheckResult::Exceeds(evidence) => ( + evidence.scope(), + "exceeds_max", + 1, + Some(counterexample_json(evidence.counterexample())), + None, + None, + ), + CheckResult::Unsupported(evidence) => ( + evidence.scope(), + "unsupported", + 3, + None, + Some(evidence.reason_code().as_str()), + Some(evidence.reason()), + ), + CheckResult::Inconclusive(evidence) => { + let exit_code = + if evidence.reason_code() == openshell_prover::containment::ReasonCode::Cancelled { + 130 + } else { + 3 + }; + ( + evidence.scope(), + "inconclusive", + exit_code, + None, + Some(evidence.reason_code().as_str()), + Some(evidence.reason()), + ) + } + }; + Envelope { + schema_version: 1, + prover_version: env!("CARGO_PKG_VERSION"), + check: "maximum_boundary", + scope: Some(scope_json(scope)), + result: result_name, + exit_code, + inputs, + counterexample, + reason_code, + reason, + } +} + +fn scope_json(scope: &CheckScope) -> ScopeJson<'_> { + ScopeJson { + model_version: scope.model_version, + policy_version: scope.policy_version, + domains: scope.domains.iter().map(|domain| domain.as_str()).collect(), + assumptions: scope.assumptions, + } +} + +fn counterexample_json(counterexample: &Counterexample) -> CounterexampleJson<'_> { + match counterexample { + Counterexample::Filesystem { access, path } => CounterexampleJson::Filesystem { + access: access.as_str(), + path, + }, + Counterexample::Network { + binary, + ancestor_binary, + binary_identity_required, + host, + port, + protocol, + method, + path, + } => CounterexampleJson::Network { + binary: binary.as_deref(), + ancestor_binary: ancestor_binary.as_deref(), + binary_identity_required: *binary_identity_required, + host, + port: *port, + protocol: protocol.as_str(), + method: method.as_deref(), + path: path.as_deref(), + }, + } +} + +fn render(output: OutputFormat, envelope: &Envelope<'_>) -> Result<(), String> { + let stdout = io::stdout(); + let mut stdout = stdout.lock(); + match output { + OutputFormat::Json => { + serde_json::to_writer_pretty(&mut stdout, envelope) + .map_err(|error| format!("failed to serialize result: {error}"))?; + writeln!(stdout).map_err(|error| format!("failed to write output: {error}")) + } + OutputFormat::Text => render_text(&mut stdout, envelope), + } +} + +fn render_text(mut writer: impl Write, envelope: &Envelope<'_>) -> Result<(), String> { + writeln!(writer, "result: {}", envelope.result) + .map_err(|error| format!("failed to write output: {error}"))?; + if let Some(scope) = &envelope.scope { + writeln!( + writer, + "scope: model={} policy={} domains={}", + escape_terminal(scope.model_version), + scope.policy_version, + scope.domains.join(",") + ) + .map_err(|error| format!("failed to write output: {error}"))?; + for assumption in scope.assumptions { + writeln!(writer, "assumption: {}", escape_terminal(assumption)) + .map_err(|error| format!("failed to write output: {error}"))?; + } + } + if let Some(counterexample) = &envelope.counterexample { + match counterexample { + CounterexampleJson::Filesystem { access, path } => writeln!( + writer, + "counterexample: filesystem {access} {}", + escape_terminal(path) + ), + CounterexampleJson::Network { + binary, + ancestor_binary, + binary_identity_required, + host, + port, + protocol, + method, + path, + } => writeln!( + writer, + "counterexample: network binary={} ancestor_binary={} binary_identity_required={} host={}:{} protocol={} method={} path={}", + binary.map_or("-".to_owned(), escape_terminal), + ancestor_binary.map_or("-".to_owned(), escape_terminal), + binary_identity_required, + escape_terminal(host), + port, + escape_terminal(protocol), + method.map_or("-".to_owned(), escape_terminal), + path.map_or("-".to_owned(), escape_terminal), + ), + } + .map_err(|error| format!("failed to write output: {error}"))?; + } + if let Some(reason) = envelope.reason { + writeln!(writer, "reason: {}", escape_terminal(reason)) + .map_err(|error| format!("failed to write output: {error}"))?; + } + Ok(()) +} + +fn parse_duration(value: &str) -> Result { + let (number, multiplier) = if let Some(number) = value.strip_suffix("ms") { + (number, 1_u64) + } else if let Some(number) = value.strip_suffix('s') { + (number, 1_000) + } else if let Some(number) = value.strip_suffix('m') { + (number, 60_000) + } else { + return Err("duration must end in ms, s, or m".to_owned()); + }; + let amount = number + .parse::() + .map_err(|_| "duration must use a positive integer".to_owned())?; + let millis = amount + .checked_mul(multiplier) + .ok_or_else(|| "duration is too large".to_owned())?; + if millis == 0 { + return Err("duration must be positive".to_owned()); + } + if millis > u64::from(u32::MAX) { + return Err(format!("duration must not exceed {}ms", u32::MAX)); + } + Ok(Duration::from_millis(millis)) +} + +fn escape_terminal(value: &str) -> String { + let mut escaped = String::with_capacity(value.len()); + for character in value.chars() { + if character.is_control() { + escaped.extend(character.escape_default()); + } else { + escaped.push(character); + } + } + escaped +} + +#[cfg(test)] +mod tests { + use super::*; + use std::fs::OpenOptions; + + struct BrokenWriter; + + impl Write for BrokenWriter { + fn write(&mut self, _buffer: &[u8]) -> io::Result { + Err(io::Error::new(io::ErrorKind::BrokenPipe, "closed")) + } + + fn flush(&mut self) -> io::Result<()> { + Ok(()) + } + } + + #[test] + fn parses_supported_durations() { + assert_eq!(parse_duration("250ms"), Ok(Duration::from_millis(250))); + assert_eq!(parse_duration("2s"), Ok(Duration::from_secs(2))); + assert_eq!(parse_duration("3m"), Ok(Duration::from_mins(3))); + } + + #[test] + fn rejects_invalid_durations() { + for value in ["0ms", "1", "1.5s", "-1s", "4294967296ms"] { + assert!(parse_duration(value).is_err(), "accepted {value}"); + } + } + + #[test] + fn escapes_terminal_control_characters() { + assert_eq!(escape_terminal("a\u{1b}[31m\nb"), "a\\u{1b}[31m\\nb"); + } + + #[test] + fn rejects_oversized_policy_before_parsing() { + let path = + std::env::temp_dir().join(format!("openshell-prover-oversized-{}", std::process::id())); + let file = OpenOptions::new() + .create_new(true) + .write(true) + .open(&path) + .expect("create oversized fixture"); + file.set_len(MAX_POLICY_BYTES + 1) + .expect("size oversized fixture"); + drop(file); + + let error = read_policy(&path).expect_err("oversized input must fail"); + std::fs::remove_file(path).expect("remove oversized fixture"); + assert!(error.contains("input limit")); + } + + #[test] + fn output_failures_are_reported() { + let envelope = Envelope { + schema_version: 1, + prover_version: env!("CARGO_PKG_VERSION"), + check: "maximum_boundary", + scope: None, + result: "within_max", + exit_code: 0, + inputs: InputsJson { + candidate: "candidate.yaml".to_owned(), + maximum: "maximum.yaml".to_owned(), + }, + counterexample: None, + reason_code: None, + reason: None, + }; + assert!(render_text(BrokenWriter, &envelope).is_err()); + } +} diff --git a/crates/openshell-prover-cli/tests/cli.rs b/crates/openshell-prover-cli/tests/cli.rs new file mode 100644 index 0000000000..06c1da5c0b --- /dev/null +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -0,0 +1,304 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +use std::fmt::Write as _; +use std::fs; +use std::path::PathBuf; +#[cfg(unix)] +use std::process::Stdio; +use std::process::{Command, Output}; +#[cfg(unix)] +use std::thread; +#[cfg(unix)] +use std::time::Duration; + +use serde_json::Value; + +fn fixture(name: &str) -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("tests/fixtures") + .join(name) +} + +fn run(args: &[&str]) -> Output { + Command::new(env!("CARGO_BIN_EXE_openshell-prover")) + .args(args) + .output() + .expect("run openshell-prover") +} + +fn check_json(candidate: &str, maximum: &str) -> Output { + run(&[ + "check", + fixture(candidate).to_str().expect("UTF-8 fixture path"), + "--maximum", + fixture(maximum).to_str().expect("UTF-8 fixture path"), + "--output", + "json", + ]) +} + +#[test] +fn help_and_version_succeed() { + for args in [ + &["--help"][..], + &["--version"][..], + &["check", "--help"][..], + ] { + let output = run(args); + assert!( + output.status.success(), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + assert!(!output.stdout.is_empty()); + } +} + +#[test] +fn bare_invocation_shows_help() { + let output = run(&[]); + assert!(output.status.success()); + assert!(String::from_utf8_lossy(&output.stdout).contains("Usage:")); +} + +#[test] +fn contained_policy_returns_stable_json_and_zero() { + let output = check_json("candidate-contained.yaml", "maximum.yaml"); + assert_eq!( + output.status.code(), + Some(0), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + assert!(output.stderr.is_empty()); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["schema_version"], 1); + assert_eq!(value["check"], "maximum_boundary"); + assert_eq!(value["result"], "within_max"); + assert_eq!(value["exit_code"], 0); + assert!(value["scope"]["domains"].is_array()); + assert!(value["counterexample"].is_null()); +} + +#[test] +fn exceeding_policy_returns_counterexample_and_one() { + let output = check_json("candidate-exceeds.yaml", "maximum.yaml"); + assert_eq!( + output.status.code(), + Some(1), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "exceeds_max"); + assert_eq!(value["exit_code"], 1); + assert_eq!(value["counterexample"]["domain"], "filesystem"); +} + +#[test] +fn unsupported_policy_returns_reason_and_three() { + let output = check_json("unsupported.yaml", "maximum.yaml"); + assert_eq!( + output.status.code(), + Some(3), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "unsupported"); + assert_eq!(value["exit_code"], 3); + assert!(value["reason_code"].is_string()); + assert!(value["reason"].is_string()); +} + +#[test] +fn resource_exhaustion_is_inconclusive_and_returns_three() { + let path = std::env::temp_dir().join(format!( + "openshell-prover-resource-limit-{}.yaml", + std::process::id() + )); + let mut source = String::from("version: 1\nnetwork_policies:\n"); + for index in 0..=1_024 { + writeln!(source, " rule-{index}: {{}}").unwrap(); + } + fs::write(&path, source).expect("write resource-limit policy"); + + let output = run(&[ + "check", + path.to_str().expect("UTF-8 temporary path"), + "--maximum", + fixture("maximum.yaml").to_str().unwrap(), + "--output", + "json", + ]); + fs::remove_file(path).expect("remove resource-limit policy"); + + assert_eq!(output.status.code(), Some(3)); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "inconclusive"); + assert_eq!(value["reason_code"], "resource_limit"); +} + +#[test] +fn invalid_json_mode_input_uses_error_envelope_and_two() { + let output = check_json("invalid.yaml", "maximum.yaml"); + assert_eq!( + output.status.code(), + Some(2), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "error"); + assert_eq!(value["exit_code"], 2); + assert_eq!(value["reason_code"], "invalid_input"); +} + +#[test] +fn missing_json_mode_input_uses_error_envelope_and_two() { + let output = run(&[ + "check", + fixture("does-not-exist.yaml").to_str().unwrap(), + "--maximum", + fixture("maximum.yaml").to_str().unwrap(), + "--output", + "json", + ]); + assert_eq!(output.status.code(), Some(2)); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "error"); + assert_eq!(value["reason_code"], "invalid_input"); + assert!(value["reason"].as_str().unwrap().contains("cannot open")); +} + +#[test] +fn usage_errors_return_two() { + let output = run(&["check"]); + assert_eq!(output.status.code(), Some(2)); + assert!(output.stdout.is_empty()); + assert!(String::from_utf8_lossy(&output.stderr).contains("required")); +} + +#[test] +fn timeout_must_be_positive() { + let output = run(&[ + "check", + fixture("candidate-contained.yaml").to_str().unwrap(), + "--maximum", + fixture("maximum.yaml").to_str().unwrap(), + "--timeout", + "0ms", + ]); + assert_eq!(output.status.code(), Some(2)); + assert!(String::from_utf8_lossy(&output.stderr).contains("positive")); +} + +#[test] +fn text_diagnostics_escape_terminal_controls() { + let output = run(&[ + "check", + "missing\u{1b}[31m.yaml", + "--maximum", + fixture("maximum.yaml").to_str().unwrap(), + ]); + assert_eq!(output.status.code(), Some(2)); + assert!(!output.stderr.contains(&0x1b)); + assert!(String::from_utf8_lossy(&output.stderr).contains("\\u{1b}")); +} + +#[cfg(unix)] +#[test] +fn fifo_input_is_rejected_without_blocking() { + use std::time::Instant; + + let path = std::env::temp_dir().join(format!("openshell-prover-fifo-{}", std::process::id())); + nix::unistd::mkfifo(&path, nix::sys::stat::Mode::S_IRUSR).expect("create FIFO fixture"); + + let mut child = Command::new(env!("CARGO_BIN_EXE_openshell-prover")) + .args([ + "check", + path.to_str().expect("UTF-8 temporary path"), + "--maximum", + fixture("maximum.yaml").to_str().unwrap(), + "--output", + "json", + ]) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .expect("start prover with FIFO input"); + + let deadline = Instant::now() + Duration::from_secs(2); + loop { + if child.try_wait().expect("poll prover").is_some() { + break; + } + if Instant::now() >= deadline { + child.kill().expect("terminate blocked prover"); + let _ = child.wait(); + fs::remove_file(&path).expect("remove FIFO fixture"); + panic!("prover blocked while opening a FIFO input"); + } + thread::sleep(Duration::from_millis(10)); + } + + let output = child.wait_with_output().expect("collect prover output"); + fs::remove_file(path).expect("remove FIFO fixture"); + assert_eq!(output.status.code(), Some(2)); + assert!(output.stderr.is_empty()); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "error"); + assert_eq!(value["reason_code"], "invalid_input"); + assert!( + value["reason"] + .as_str() + .expect("string reason") + .contains("not a regular file") + ); +} + +#[cfg(unix)] +#[test] +fn sigint_interrupts_the_check_with_exit_130() { + let path = std::env::temp_dir().join(format!( + "openshell-prover-cancellation-{}.yaml", + std::process::id() + )); + let mut source = String::from("version: 1\nnetwork_policies:\n"); + for index in 0..500 { + writeln!( + source, + " rule-{index}:\n endpoints: [{{ host: host-{index}.example.com, port: 443 }}]\n binaries: [{{ path: /usr/bin/curl }}]" + ) + .unwrap(); + } + fs::write(&path, source).expect("write cancellation policy"); + + let child = Command::new(env!("CARGO_BIN_EXE_openshell-prover")) + .args([ + "check", + path.to_str().expect("UTF-8 temporary path"), + "--maximum", + path.to_str().expect("UTF-8 temporary path"), + "--output", + "json", + ]) + .stdout(Stdio::piped()) + .spawn() + .expect("start cancellable prover"); + thread::sleep(Duration::from_millis(25)); + let signal = Command::new("kill") + .args(["-s", "INT", &child.id().to_string()]) + .status() + .expect("send SIGINT"); + assert!(signal.success()); + let output = child.wait_with_output().expect("wait for cancelled prover"); + fs::remove_file(path).expect("remove cancellation policy"); + assert_eq!(output.status.code(), Some(130)); + let value: Value = + serde_json::from_slice(&output.stdout).expect("structured cancellation JSON"); + assert_eq!(value["result"], "inconclusive"); + assert_eq!(value["reason_code"], "cancelled"); + assert_eq!(value["exit_code"], 130); +} diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml new file mode 100644 index 0000000000..59fe39368f --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml @@ -0,0 +1,9 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +filesystem_policy: + read_only: + - /usr/bin + read_write: + - /tmp/cache diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-exceeds.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-exceeds.yaml new file mode 100644 index 0000000000..a59983cf93 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-exceeds.yaml @@ -0,0 +1,9 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +filesystem_policy: + read_only: + - /usr/bin + read_write: + - /workspace diff --git a/crates/openshell-prover-cli/tests/fixtures/invalid.yaml b/crates/openshell-prover-cli/tests/fixtures/invalid.yaml new file mode 100644 index 0000000000..a904b71a19 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/invalid.yaml @@ -0,0 +1,4 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: [ diff --git a/crates/openshell-prover-cli/tests/fixtures/maximum.yaml b/crates/openshell-prover-cli/tests/fixtures/maximum.yaml new file mode 100644 index 0000000000..7c49a53efc --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/maximum.yaml @@ -0,0 +1,10 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +filesystem_policy: + read_only: + - /usr + - /etc + read_write: + - /tmp diff --git a/crates/openshell-prover-cli/tests/fixtures/unsupported.yaml b/crates/openshell-prover-cli/tests/fixtures/unsupported.yaml new file mode 100644 index 0000000000..5f3ac856fe --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/unsupported.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +process: + run_as_user: sandbox diff --git a/crates/openshell-prover/Cargo.toml b/crates/openshell-prover/Cargo.toml index b620280e46..ab2101d2ac 100644 --- a/crates/openshell-prover/Cargo.toml +++ b/crates/openshell-prover/Cargo.toml @@ -23,5 +23,10 @@ owo-colors = { workspace = true } include_dir = { workspace = true } glob = { workspace = true } +[dev-dependencies] +openshell-core = { path = "../openshell-core" } +regorus = { version = "0.9", default-features = false, features = ["std", "arc", "glob"] } +serde_json = { workspace = true } + [lints] workspace = true diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index f8b45eca61..f13578b94a 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -8,6 +8,12 @@ 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. + 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 @@ -107,10 +113,12 @@ be additive — they don't displace existing categories. - 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 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 diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs new file mode 100644 index 0000000000..e95fb8589a --- /dev/null +++ b/crates/openshell-prover/src/containment.rs @@ -0,0 +1,2293 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Sound, deliberately narrow policy-containment checks. +//! +//! This module is independent of the legacy proposal-risk model. It parses the +//! authority-bearing fields it understands and fails closed when another field +//! could affect the result. + +use std::collections::BTreeMap; +use std::fmt; +use std::net::IpAddr; +use std::str::FromStr; +use std::sync::atomic::{AtomicBool, Ordering}; +use std::time::{Duration, Instant}; + +use serde::Deserialize; +use serde_yml::Value; +use z3::ast::{Bool, Int, Regexp, String as Z3String}; +use z3::{Context, Params, SatResult, Solver}; + +const READ_ONLY_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS"]; +const READ_WRITE_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH"]; +const LAYER_L4: &str = "l4"; +const LAYER_REST: &str = "rest"; +const WORKDIR_SYMBOL: &str = ""; +const MAX_POLICY_BYTES: usize = 4 * 1024 * 1024; +const MAX_YAML_DEPTH: usize = 64; +const MAX_YAML_NODES: usize = 100_000; + +/// Parser error for a containment input. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ParsePolicyError(String); + +impl fmt::Display for ParsePolicyError { + fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result { + formatter.write_str(&self.0) + } +} + +impl std::error::Error for ParsePolicyError {} + +/// Policy representation used only by maximum-boundary checking. +#[derive(Debug, Clone, Deserialize, PartialEq)] +pub struct ContainmentPolicy { + version: u32, + #[serde(default)] + filesystem_policy: FilesystemPolicy, + #[serde(default)] + network_policies: BTreeMap, + #[serde(default)] + landlock: Option, + #[serde(default)] + process: Option, + #[serde(default)] + network_middlewares: BTreeMap, + // Managed-maximum metadata changes workflow, not authority. Retain it in + // the parsed representation without letting it alter containment. + #[serde(default)] + metadata: Option, + #[serde(flatten)] + extra: BTreeMap, +} + +impl ContainmentPolicy { + /// Managed-maximum metadata retained from the input, when present. + #[must_use] + pub const fn metadata(&self) -> Option<&ManagedPolicyMetadata> { + self.metadata.as_ref() + } +} + +/// Workflow metadata carried by a managed-maximum document. +#[derive(Debug, Clone, Default, Deserialize, PartialEq, Eq)] +pub struct ManagedPolicyMetadata { + #[serde(default)] + pub policy_id: String, + #[serde(default)] + pub version: u64, + #[serde(default)] + pub allowed_modes: Vec, + #[serde(default)] + pub default_mode: String, + #[serde(default)] + pub audit_label: String, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Default, Deserialize, PartialEq)] +struct FilesystemPolicy { + #[serde(default)] + include_workdir: bool, + #[serde(default)] + read_only: Vec, + #[serde(default)] + read_write: Vec, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Deserialize, PartialEq)] +struct NetworkRule { + #[serde(default, rename = "name")] + _name: String, + #[serde(default)] + endpoints: Vec, + #[serde(default)] + binaries: Vec, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Deserialize, PartialEq)] +struct Binary { + path: String, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Deserialize, PartialEq)] +#[allow( + clippy::struct_excessive_bools, + reason = "The endpoint parser accounts for independent policy-schema toggles." +)] +struct Endpoint { + #[serde(default)] + host: String, + #[serde(default)] + path: String, + #[serde(default)] + port: u16, + #[serde(default)] + ports: Vec, + #[serde(default)] + protocol: String, + #[serde(default)] + tls: String, + #[serde(default)] + enforcement: String, + #[serde(default)] + access: String, + #[serde(default)] + rules: Vec, + #[serde(default)] + deny_rules: Vec, + #[serde(default)] + allowed_ips: Vec, + #[serde(default)] + review: Review, + #[serde(default)] + allow_encoded_slash: bool, + #[serde(default)] + websocket_credential_rewrite: bool, + #[serde(default)] + request_body_credential_rewrite: bool, + #[serde(default)] + allow_uninspected_credentials: bool, + #[serde(default)] + persisted_queries: String, + #[serde(default)] + graphql_persisted_queries: BTreeMap, + #[serde(default)] + graphql_max_body_bytes: u32, + #[serde(default)] + credential_signing: String, + #[serde(default)] + signing_service: String, + #[serde(default)] + signing_region: String, + #[serde(default)] + credential_binding: Option, + #[serde(default)] + json_rpc: Option, + #[serde(default)] + mcp: Option, + #[serde(flatten)] + extra: BTreeMap, +} + +impl Endpoint { + fn effective_ports(&self) -> Vec { + if self.ports.is_empty() { + (self.port != 0).then_some(self.port).into_iter().collect() + } else { + self.ports.clone() + } + } + + fn protocol_kind(&self) -> Protocol { + if self.protocol.is_empty() || self.protocol.eq_ignore_ascii_case("tcp") { + Protocol::L4 + } else { + Protocol::Rest + } + } +} + +#[derive(Debug, Clone, Deserialize, PartialEq)] +struct AllowRule { + allow: Allow, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Deserialize, PartialEq)] +struct Allow { + #[serde(default)] + method: String, + #[serde(default)] + path: String, + #[serde(default)] + command: String, + #[serde(default)] + review: Review, + #[serde(default)] + query: BTreeMap, + #[serde(default)] + operation_type: String, + #[serde(default)] + operation_name: String, + #[serde(default)] + fields: Vec, + #[serde(default)] + tool: Option, + #[serde(default)] + params: BTreeMap, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Deserialize, PartialEq)] +struct DenyRule { + #[serde(default)] + method: String, + #[serde(default)] + path: String, + #[serde(default)] + command: String, + #[serde(default)] + query: BTreeMap, + #[serde(default)] + operation_type: String, + #[serde(default)] + operation_name: String, + #[serde(default)] + fields: Vec, + #[serde(default)] + tool: Option, + #[serde(default)] + params: BTreeMap, + #[serde(flatten)] + extra: BTreeMap, +} + +#[derive(Debug, Clone, Default, Deserialize, PartialEq)] +struct Review { + #[serde(default, rename = "required")] + _required: bool, + #[serde(default, rename = "reason")] + _reason: String, + #[serde(flatten)] + extra: BTreeMap, +} + +/// Parse one captured YAML input for containment checking. +pub fn parse_policy_str(source: &str) -> Result { + if source.len() > MAX_POLICY_BYTES { + return Err(ParsePolicyError(format!( + "policy exceeds the {MAX_POLICY_BYTES}-byte input limit" + ))); + } + let value: Value = serde_yml::from_str(source) + .map_err(|error| ParsePolicyError(format!("invalid policy YAML: {error}")))?; + validate_yaml_shape(&value)?; + let mut policy: ContainmentPolicy = serde_yml::from_str(source) + .map_err(|error| ParsePolicyError(format!("invalid policy YAML: {error}")))?; + if policy.version != 1 { + return Err(ParsePolicyError(format!( + "unsupported policy version {}; expected version 1", + policy.version + ))); + } + normalize_filesystem_paths(&mut policy.filesystem_policy)?; + Ok(policy) +} + +fn validate_yaml_shape(root: &Value) -> Result<(), ParsePolicyError> { + let mut stack = vec![(root, 0_usize)]; + let mut nodes = 0_usize; + while let Some((value, depth)) = stack.pop() { + nodes += 1; + if nodes > MAX_YAML_NODES { + return Err(ParsePolicyError(format!( + "policy exceeds the {MAX_YAML_NODES}-node YAML limit" + ))); + } + if depth > MAX_YAML_DEPTH { + return Err(ParsePolicyError(format!( + "policy exceeds the {MAX_YAML_DEPTH}-level YAML depth limit" + ))); + } + match value { + Value::Sequence(values) => { + stack.extend(values.iter().map(|value| (value, depth + 1))); + } + Value::Mapping(values) => { + stack.extend(values.values().map(|value| (value, depth + 1))); + } + Value::Tagged(value) => stack.push((value.value(), depth + 1)), + Value::Null | Value::Bool(_) | Value::Number(_) | Value::String(_) => {} + } + } + Ok(()) +} + +fn normalize_filesystem_paths(policy: &mut FilesystemPolicy) -> Result<(), ParsePolicyError> { + for path in policy.read_only.iter_mut().chain(&mut policy.read_write) { + *path = normalize_path(path)?; + } + Ok(()) +} + +fn normalize_path(path: &str) -> Result { + if !path.starts_with('/') { + return Err(ParsePolicyError(format!( + "filesystem path '{path}' must be absolute" + ))); + } + let mut parts = Vec::new(); + for part in path.split('/') { + match part { + "" | "." => {} + ".." => { + return Err(ParsePolicyError(format!( + "filesystem path '{path}' contains an unsupported '..' segment" + ))); + } + value => parts.push(value), + } + } + Ok(if parts.is_empty() { + "/".to_owned() + } else { + format!("/{}", parts.join("/")) + }) +} + +/// Per-invocation solver limits. These never modify Z3 global parameters. +#[derive(Debug, Clone, Copy)] +pub struct CheckOptions { + pub timeout: Duration, +} + +/// Stable reason identifiers for automation. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ReasonCode { + UnsupportedPolicyShape, + UnresolvedWorkdir, + UnresolvedBinaryPath, + SolverTimeout, + SolverUnknown, + ResourceLimit, + InvalidWitness, + Cancelled, +} + +impl ReasonCode { + #[must_use] + pub const fn as_str(self) -> &'static str { + match self { + Self::UnsupportedPolicyShape => "unsupported_policy_shape", + Self::UnresolvedWorkdir => "unresolved_workdir", + Self::UnresolvedBinaryPath => "unresolved_binary_path", + Self::SolverTimeout => "solver_timeout", + Self::SolverUnknown => "solver_unknown", + Self::ResourceLimit => "resource_limit", + Self::InvalidWitness => "invalid_witness", + Self::Cancelled => "cancelled", + } + } +} + +/// Authority domains modeled by this engine version. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum CheckDomain { + Filesystem, + NetworkL4, + NetworkRest, +} + +impl CheckDomain { + #[must_use] + pub const fn as_str(self) -> &'static str { + match self { + Self::Filesystem => "filesystem", + Self::NetworkL4 => "network_l4", + Self::NetworkRest => "network_rest", + } + } +} + +/// Scope attached to every completed or recoverably incomplete check. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct CheckScope { + pub model_version: &'static str, + pub policy_version: u32, + pub domains: &'static [CheckDomain], + pub assumptions: &'static [&'static str], +} + +static DOMAINS: &[CheckDomain] = &[ + CheckDomain::Filesystem, + CheckDomain::NetworkL4, + CheckDomain::NetworkRest, +]; +static ASSUMPTIONS: &[&str] = &[ + "Candidate and maximum use the same sandbox filesystem namespace and mount interpretation.", + "Network containment covers runtime configurations with binary identity checks enabled and disabled.", + "REST witnesses use canonical request methods and paths.", +]; + +fn check_scope() -> &'static CheckScope { + static SCOPE: CheckScope = CheckScope { + model_version: "maximum-boundary-v1", + policy_version: 1, + domains: DOMAINS, + assumptions: ASSUMPTIONS, + }; + &SCOPE +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum FilesystemAccess { + Read, + Write, +} + +impl FilesystemAccess { + #[must_use] + pub const fn as_str(self) -> &'static str { + match self { + Self::Read => "read", + Self::Write => "write", + } + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Protocol { + L4, + Rest, +} + +impl Protocol { + #[must_use] + pub const fn as_str(self) -> &'static str { + match self { + Self::L4 => "l4", + Self::Rest => "rest", + } + } +} + +/// Concrete action showing why containment failed. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Counterexample { + Filesystem { + access: FilesystemAccess, + path: String, + }, + Network { + binary: Option, + ancestor_binary: Option, + binary_identity_required: bool, + host: String, + port: u16, + protocol: Protocol, + method: Option, + path: Option, + }, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct WithinEvidence; + +impl WithinEvidence { + #[must_use] + pub fn scope(&self) -> &'static CheckScope { + check_scope() + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ExceedsEvidence(Counterexample); + +impl ExceedsEvidence { + #[must_use] + pub fn scope(&self) -> &'static CheckScope { + check_scope() + } + + #[must_use] + pub const fn counterexample(&self) -> &Counterexample { + &self.0 + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ReasonEvidence { + code: ReasonCode, + reason: String, +} + +impl ReasonEvidence { + #[must_use] + pub fn scope(&self) -> &'static CheckScope { + check_scope() + } + + #[must_use] + pub const fn reason_code(&self) -> ReasonCode { + self.code + } + + #[must_use] + pub fn reason(&self) -> &str { + &self.reason + } +} + +/// Result of a maximum-boundary proof attempt. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum CheckResult { + Within(WithinEvidence), + Exceeds(ExceedsEvidence), + Unsupported(ReasonEvidence), + Inconclusive(ReasonEvidence), +} + +impl CheckResult { + /// Construct the standard typed result for a caller-observed cancellation. + #[must_use] + pub fn cancelled() -> Self { + cancelled_result() + } +} + +struct SymbolicAction { + binary: Z3String, + ancestor_binary: Z3String, + host: Z3String, + port: Int, + layer: Z3String, + method: Z3String, + path: Z3String, +} + +enum NetworkSolve { + Within, + Exceeds(Counterexample), + Incomplete(CheckResult), +} + +/// Determine whether every modeled candidate action is allowed by `maximum`. +#[must_use] +pub fn check_within_maximum( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + options: CheckOptions, +) -> CheckResult { + check_within_maximum_inner(maximum, candidate, options, None) +} + +/// Determine containment while allowing a caller-owned cancellation flag to +/// interrupt the solver. The caller remains responsible for signal handling. +#[must_use] +pub fn check_within_maximum_cancellable( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + options: CheckOptions, + cancelled: &AtomicBool, +) -> CheckResult { + check_within_maximum_inner(maximum, candidate, options, Some(cancelled)) +} + +fn check_within_maximum_inner( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + options: CheckOptions, + cancelled: Option<&AtomicBool>, +) -> CheckResult { + if let Some(reason) = unsupported_reason("maximum", maximum) { + return unsupported(reason.0, reason.1); + } + if let Some(reason) = unsupported_reason("candidate", candidate) { + return unsupported(reason.0, reason.1); + } + if let Some(reason) = resource_limit_reason(maximum, candidate) { + return CheckResult::Inconclusive(ReasonEvidence { + code: ReasonCode::ResourceLimit, + reason, + }); + } + if cancelled.is_some_and(|flag| flag.load(Ordering::Relaxed)) { + return cancelled_result(); + } + if options.timeout.is_zero() { + return CheckResult::Inconclusive(ReasonEvidence { + code: ReasonCode::SolverTimeout, + reason: "solver timeout must be positive".to_owned(), + }); + } + if let Some(reason) = unresolved_workdir_reason(maximum, candidate) { + return unsupported(ReasonCode::UnresolvedWorkdir, reason); + } + if maximum == candidate { + return CheckResult::Within(WithinEvidence); + } + if let Some(counterexample) = filesystem_counterexample(maximum, candidate) { + return CheckResult::Exceeds(ExceedsEvidence(counterexample)); + } + let started = Instant::now(); + for binary_identity_required in [false, true] { + match solve_network_mode( + maximum, + candidate, + binary_identity_required, + started, + options.timeout, + cancelled, + ) { + NetworkSolve::Within => {} + NetworkSolve::Exceeds(counterexample) => { + return CheckResult::Exceeds(ExceedsEvidence(counterexample)); + } + NetworkSolve::Incomplete(result) => return result, + } + let ambiguous_binary_paths = ambiguous_candidate_binary_paths(maximum, candidate); + if binary_identity_required && !ambiguous_binary_paths.is_empty() { + let exact_maximum = + maximum_without_ambiguous_binary_globs(maximum, candidate, &ambiguous_binary_paths); + match solve_network_mode( + &exact_maximum, + candidate, + true, + started, + options.timeout, + cancelled, + ) { + NetworkSolve::Within => {} + NetworkSolve::Exceeds(_) => { + return unsupported( + ReasonCode::UnresolvedBinaryPath, + "network containment depends on image-specific binary symlink resolution" + .to_owned(), + ); + } + NetworkSolve::Incomplete(result) => return result, + } + } + } + if unresolved_exact_deny_symlink(maximum, candidate) { + return unsupported( + ReasonCode::UnresolvedBinaryPath, + "network deny containment depends on image-specific exact binary symlink resolution" + .to_owned(), + ); + } + CheckResult::Within(WithinEvidence) +} + +fn solve_network_mode( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + binary_identity_required: bool, + started: Instant, + timeout: Duration, + cancelled: Option<&AtomicBool>, +) -> NetworkSolve { + let solver = Solver::new(); + let action = symbolic_action(if binary_identity_required { + "strict_maximum_policy_action" + } else { + "relaxed_maximum_policy_action" + }); + assert_action_domain(&solver, &action, binary_identity_required); + solver.assert(Bool::and(&[ + policy_allows(candidate, &action, binary_identity_required), + !policy_allows(maximum, &action, binary_identity_required), + ])); + + let Some(remaining) = timeout.checked_sub(started.elapsed()) else { + return NetworkSolve::Incomplete(solver_timeout_result()); + }; + let remaining_ms = u32::try_from(remaining.as_millis()).unwrap_or(u32::MAX); + if remaining_ms == 0 { + return NetworkSolve::Incomplete(solver_timeout_result()); + } + let mut params = Params::new(); + params.set_u32("timeout", remaining_ms); + solver.set_params(¶ms); + let solve_result = solver_check(&solver, cancelled); + if cancelled.is_some_and(|flag| flag.load(Ordering::Relaxed)) { + return NetworkSolve::Incomplete(cancelled_result()); + } + match solve_result { + SatResult::Unsat => NetworkSolve::Within, + SatResult::Unknown => { + let reason = solver + .get_reason_unknown() + .unwrap_or_else(|| "Z3 returned unknown".to_owned()); + let code = if reason.to_ascii_lowercase().contains("timeout") { + ReasonCode::SolverTimeout + } else { + ReasonCode::SolverUnknown + }; + NetworkSolve::Incomplete(CheckResult::Inconclusive(ReasonEvidence { code, reason })) + } + SatResult::Sat => solver + .get_model() + .and_then(|model| counterexample_from_model(&model, &action, binary_identity_required)) + .map_or_else( + || { + NetworkSolve::Incomplete(CheckResult::Inconclusive(ReasonEvidence { + code: ReasonCode::InvalidWitness, + reason: "solver returned a model that could not be decoded".to_owned(), + })) + }, + NetworkSolve::Exceeds, + ), + } +} + +fn solver_timeout_result() -> CheckResult { + CheckResult::Inconclusive(ReasonEvidence { + code: ReasonCode::SolverTimeout, + reason: "solver timeout elapsed".to_owned(), + }) +} + +fn cancelled_result() -> CheckResult { + CheckResult::Inconclusive(ReasonEvidence { + code: ReasonCode::Cancelled, + reason: "containment check was cancelled".to_owned(), + }) +} + +fn solver_check(solver: &Solver, cancelled: Option<&AtomicBool>) -> SatResult { + let Some(cancelled) = cancelled else { + return solver.check(); + }; + let finished = AtomicBool::new(false); + let context = Context::thread_local(); + let handle = context.handle(); + std::thread::scope(|scope| { + let watcher = scope.spawn(|| { + while !finished.load(Ordering::Acquire) && !cancelled.load(Ordering::Relaxed) { + std::thread::park_timeout(Duration::from_millis(10)); + } + if cancelled.load(Ordering::Relaxed) { + handle.interrupt(); + } + }); + let result = solver.check(); + finished.store(true, Ordering::Release); + watcher.thread().unpark(); + watcher.join().expect("cancellation watcher must not panic"); + result + }) +} + +fn unsupported(code: ReasonCode, reason: String) -> CheckResult { + CheckResult::Unsupported(ReasonEvidence { code, reason }) +} + +fn symbolic_action(name: &str) -> SymbolicAction { + let _context = Context::thread_local(); + SymbolicAction { + binary: Z3String::new_const(format!("{name}_binary")), + ancestor_binary: Z3String::new_const(format!("{name}_ancestor_binary")), + host: Z3String::new_const(format!("{name}_host")), + port: Int::new_const(format!("{name}_port")), + layer: Z3String::new_const(format!("{name}_layer")), + method: Z3String::new_const(format!("{name}_method")), + path: Z3String::new_const(format!("{name}_path")), + } +} + +fn assert_action_domain(solver: &Solver, action: &SymbolicAction, binary_identity_required: bool) { + if binary_identity_required { + solver.assert(action.binary.regex_matches(&glob_regex("/**", "/"))); + solver.assert(action.binary.length().le(4_096)); + solver.assert( + action + .ancestor_binary + .regex_matches(&glob_regex("/**", "/")), + ); + solver.assert(action.ancestor_binary.length().le(4_096)); + } + solver.assert(action.host.regex_matches(&host_domain_regex())); + solver.assert(action.host.length().le(253)); + solver.assert(Int::from_u64(1).le(&action.port)); + solver.assert(action.port.le(65_535)); + solver.assert(str_eq_any(&action.layer, &[LAYER_L4, LAYER_REST])); + solver.assert(!action.method.eq("")); + solver.assert( + Z3String::from_str("/") + .expect("valid Z3 string") + .prefix(&action.path), + ); + solver.assert(action.path.length().le(4_096)); + for forbidden in ["//", "/./", "/../", ";", "?", "#"] { + solver.assert(!action.path.contains(forbidden)); + } + solver.assert(!action.path.eq("/.")); + solver.assert(!action.path.eq("/..")); + solver.assert(!Z3String::from_str("/.").unwrap().suffix(&action.path)); + solver.assert(!Z3String::from_str("/..").unwrap().suffix(&action.path)); +} + +fn policy_allows( + policy: &ContainmentPolicy, + action: &SymbolicAction, + binary_identity_required: bool, +) -> Bool { + let allowed = bool_or( + policy + .network_policies + .values() + .map(|rule| rule_allows(rule, action, binary_identity_required)), + ); + let denied = bool_or( + policy + .network_policies + .values() + .map(|rule| rule_denies(rule, action, binary_identity_required)), + ); + Bool::and(&[allowed, !denied]) +} + +fn rule_allows( + rule: &NetworkRule, + action: &SymbolicAction, + binary_identity_required: bool, +) -> Bool { + Bool::and(&[ + binaries_match(rule, action, binary_identity_required), + bool_or( + rule.endpoints + .iter() + .map(|endpoint| endpoint_allows(endpoint, action)), + ), + ]) +} + +fn rule_denies( + rule: &NetworkRule, + action: &SymbolicAction, + binary_identity_required: bool, +) -> Bool { + Bool::and(&[ + binaries_match(rule, action, binary_identity_required), + bool_or( + rule.endpoints + .iter() + .map(|endpoint| endpoint_denies(endpoint, action)), + ), + ]) +} + +fn binaries_match( + rule: &NetworkRule, + action: &SymbolicAction, + binary_identity_required: bool, +) -> Bool { + if !binary_identity_required { + return Bool::from_bool(true); + } + bool_or(rule.binaries.iter().flat_map(|binary| { + let pattern = glob_regex(&binary.path, "/"); + [ + action.binary.regex_matches(&pattern), + action.ancestor_binary.regex_matches(&pattern), + ] + })) +} + +fn endpoint_allows(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { + let common = endpoint_matches_connection(endpoint, action); + match endpoint.protocol_kind() { + Protocol::L4 => common, + Protocol::Rest => Bool::and(&[ + common, + action.layer.eq(LAYER_REST), + endpoint_path_matches(endpoint, action), + rest_endpoint_allows(endpoint, action), + ]), + } +} + +fn endpoint_denies(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { + if endpoint.protocol_kind() != Protocol::Rest || endpoint.deny_rules.is_empty() { + return Bool::from_bool(false); + } + Bool::and(&[ + endpoint_matches_connection(endpoint, action), + action.layer.eq(LAYER_REST), + endpoint_path_matches(endpoint, action), + bool_or( + endpoint + .deny_rules + .iter() + .map(|deny| method_and_path_match(&deny.method, &deny.path, action)), + ), + ]) +} + +fn rest_endpoint_allows(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { + match endpoint.access.as_str() { + "read-only" => methods_match(action, READ_ONLY_METHODS, "**"), + "read-write" => methods_match(action, READ_WRITE_METHODS, "**"), + "full" => any_method_matches(action, "**"), + _ => bool_or( + endpoint + .rules + .iter() + .map(|rule| method_and_path_match(&rule.allow.method, &rule.allow.path, action)), + ), + } +} + +fn endpoint_matches_connection(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { + Bool::and(&[ + bool_or( + endpoint + .effective_ports() + .into_iter() + .map(|port| action.port.eq(Int::from_u64(u64::from(port)))), + ), + action + .host + .regex_matches(&glob_regex(&endpoint.host.to_ascii_lowercase(), ".")), + ]) +} + +fn endpoint_path_matches(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { + let path = if endpoint.path.is_empty() { + "**" + } else { + &endpoint.path + }; + action.path.regex_matches(&glob_regex(path, "/")) +} + +fn method_and_path_match(method: &str, path: &str, action: &SymbolicAction) -> Bool { + if method.is_empty() { + return Bool::from_bool(false); + } + let path = if path.is_empty() { "**" } else { path }; + if method == "*" { + any_method_matches(action, path) + } else if method.eq_ignore_ascii_case("GET") { + methods_match(action, &["GET", "HEAD"], path) + } else { + methods_match(action, &[method], path) + } +} + +fn any_method_matches(action: &SymbolicAction, path: &str) -> Bool { + action.path.regex_matches(&glob_regex(path, "/")) +} + +fn methods_match(action: &SymbolicAction, methods: &[&str], path: &str) -> Bool { + Bool::and(&[ + str_eq_any_case_insensitive(&action.method, methods), + action.path.regex_matches(&glob_regex(path, "/")), + ]) +} + +fn counterexample_from_model( + model: &z3::Model, + action: &SymbolicAction, + binary_identity_required: bool, +) -> Option { + let port = model.eval(&action.port, true)?.as_u64()?; + let layer = model.eval(&action.layer, true)?.as_string()?; + let binary = if binary_identity_required { + let binary = model.eval(&action.binary, true)?.as_string()?; + if !is_canonical_runtime_binary_path(&binary) { + return None; + } + Some(binary) + } else { + None + }; + let ancestor_binary = if binary_identity_required { + let binary = model.eval(&action.ancestor_binary, true)?.as_string()?; + if !is_canonical_runtime_binary_path(&binary) { + return None; + } + Some(binary) + } else { + None + }; + let host = model.eval(&action.host, true)?.as_string()?; + if !is_canonical_dns_host(&host) { + return None; + } + let protocol = if layer == LAYER_L4 { + Protocol::L4 + } else { + Protocol::Rest + }; + let (method, path) = if protocol == Protocol::Rest { + let method = model.eval(&action.method, true)?.as_string()?; + let path = model.eval(&action.path, true)?.as_string()?; + if !is_http_method(&method) || !is_canonical_rest_path(&path) { + return None; + } + (Some(method), Some(path)) + } else { + (None, None) + }; + Some(Counterexample::Network { + binary, + ancestor_binary, + binary_identity_required, + host, + port: u16::try_from(port).ok()?, + protocol, + method, + path, + }) +} + +fn is_canonical_runtime_binary_path(path: &str) -> bool { + path.len() <= 4 * 1024 && is_canonical_pattern_path(path) && !path.chars().any(char::is_control) +} + +fn is_canonical_dns_host(host: &str) -> bool { + !host.is_empty() + && host.len() <= 253 + && host.split('.').all(|label| { + !label.is_empty() + && label.len() <= 63 + && label + .bytes() + .all(|byte| byte.is_ascii_lowercase() || byte.is_ascii_digit() || byte == b'-') + && label + .as_bytes() + .first() + .is_some_and(u8::is_ascii_alphanumeric) + && label + .as_bytes() + .last() + .is_some_and(u8::is_ascii_alphanumeric) + }) +} + +fn is_http_method(method: &str) -> bool { + !method.is_empty() + && method.bytes().all(|byte| { + byte.is_ascii_alphanumeric() + || matches!( + byte, + b'!' | b'#' + | b'$' + | b'%' + | b'&' + | b'\'' + | b'*' + | b'+' + | b'-' + | b'.' + | b'^' + | b'_' + | b'`' + | b'|' + | b'~' + ) + }) +} + +fn is_canonical_rest_path(path: &str) -> bool { + if path.is_empty() + || path.len() > 4 * 1024 + || !path.starts_with('/') + || path.contains("//") + || path.contains(';') + || path.contains('?') + || path.contains('#') + { + return false; + } + let bytes = path.as_bytes(); + if bytes.iter().any(|byte| !(0x21..=0x7e).contains(byte)) + || path.split('/').any(|segment| matches!(segment, "." | "..")) + { + return false; + } + let mut index = 0; + while index < bytes.len() { + if bytes[index] != b'%' { + if bytes[index] != b'/' && !is_literal_canonical_pchar(bytes[index]) { + return false; + } + index += 1; + continue; + } + if index + 2 >= bytes.len() + || !bytes[index + 1].is_ascii_hexdigit() + || !bytes[index + 2].is_ascii_hexdigit() + || bytes[index + 1].is_ascii_lowercase() + || bytes[index + 2].is_ascii_lowercase() + { + return false; + } + let decoded = u8::from_str_radix(&path[index + 1..index + 3], 16).expect("checked hex"); + if decoded == b'/' + || decoded == b';' + || decoded.is_ascii_control() + || is_literal_canonical_pchar(decoded) + { + return false; + } + index += 3; + } + true +} + +fn is_literal_canonical_pchar(byte: u8) -> bool { + byte.is_ascii_alphanumeric() + || matches!( + byte, + b'-' | b'.' + | b'_' + | b'~' + | b'!' + | b'$' + | b'&' + | b'\'' + | b'(' + | b')' + | b'*' + | b'+' + | b',' + | b'=' + | b':' + | b'@' + ) +} + +fn unresolved_workdir_reason( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> Option { + let maximum_writes = &maximum.filesystem_policy.read_write; + let mut maximum_reads = maximum.filesystem_policy.read_only.clone(); + maximum_reads.extend(maximum_writes.iter().cloned()); + + if candidate.filesystem_policy.include_workdir + && !maximum.filesystem_policy.include_workdir + && !maximum_writes.iter().any(|path| path == "/") + { + return Some( + "candidate filesystem authority depends on an unresolved image workdir".to_owned(), + ); + } + if maximum.filesystem_policy.include_workdir + && (candidate + .filesystem_policy + .read_write + .iter() + .any(|path| !path_is_covered(path, maximum_writes)) + || candidate + .filesystem_policy + .read_only + .iter() + .any(|path| !path_is_covered(path, &maximum_reads))) + { + return Some( + "maximum filesystem authority depends on an unresolved image workdir".to_owned(), + ); + } + None +} + +fn ambiguous_candidate_binary_paths( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> Vec { + let maximum_binaries = maximum + .network_policies + .values() + .flat_map(|rule| &rule.binaries) + .map(|binary| binary.path.as_str()) + .collect::>(); + candidate + .network_policies + .values() + .flat_map(|rule| &rule.binaries) + .map(|binary| binary.path.as_str()) + .filter(|path| !path.contains('*')) + .filter(|path| { + maximum_binaries.iter().any(|maximum| { + maximum.contains('*') + && *maximum != "/**" + && glob::Pattern::new(maximum).is_ok_and(|pattern| pattern.matches(path)) + }) + }) + .map(str::to_owned) + .collect() +} + +fn maximum_without_ambiguous_binary_globs( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + ambiguous_candidate_paths: &[String], +) -> ContainmentPolicy { + let mut exact_maximum = maximum.clone(); + for rule in exact_maximum.network_policies.values_mut() { + let endpoints = rule.endpoints.clone(); + rule.binaries.retain(|binary| { + let shared_by_equivalent_rule = + candidate.network_policies.values().any(|candidate_rule| { + endpoint_authority_sets_equal(&candidate_rule.endpoints, &endpoints) + && candidate_rule + .binaries + .iter() + .any(|candidate_binary| candidate_binary.path == binary.path) + }); + let authorizes_ambiguous_exact = + candidate.network_policies.values().any(|candidate_rule| { + endpoint_authority_sets_overlap(&candidate_rule.endpoints, &endpoints) + && candidate_rule.binaries.iter().any(|candidate_binary| { + !candidate_binary.path.contains('*') + && ambiguous_candidate_paths.contains(&candidate_binary.path) + && glob::Pattern::new(&binary.path) + .is_ok_and(|pattern| pattern.matches(&candidate_binary.path)) + }) + }); + !binary.path.contains('*') + || binary.path == "/**" + || (shared_by_equivalent_rule && !authorizes_ambiguous_exact) + || !ambiguous_candidate_paths.iter().any(|candidate| { + glob::Pattern::new(&binary.path).is_ok_and(|pattern| pattern.matches(candidate)) + }) + }); + } + exact_maximum +} + +fn unresolved_exact_deny_symlink( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> bool { + maximum.network_policies.values().any(|maximum_rule| { + let maximum_deny_endpoints = maximum_rule + .endpoints + .iter() + .filter(|endpoint| !endpoint.deny_rules.is_empty()) + .collect::>(); + if maximum_deny_endpoints.is_empty() { + return false; + } + maximum_rule + .binaries + .iter() + .filter(|binary| !binary.path.contains('*')) + .any(|maximum_binary| { + candidate.network_policies.values().any(|candidate_rule| { + let endpoints_overlap = candidate_rule + .endpoints + .iter() + .filter(|endpoint| !endpoint.deny_rules.is_empty()) + .any(|candidate_endpoint| { + maximum_deny_endpoints.iter().any(|maximum_endpoint| { + endpoint_authority_may_overlap(candidate_endpoint, maximum_endpoint) + }) + }); + endpoints_overlap + && candidate_rule.binaries.iter().any(|candidate_binary| { + candidate_binary.path.contains('*') + && candidate_binary.path != "/**" + && glob::Pattern::new(&candidate_binary.path) + .is_ok_and(|pattern| pattern.matches(&maximum_binary.path)) + }) + }) + }) + }) +} + +fn endpoint_authority_sets_equal(left: &[Endpoint], right: &[Endpoint]) -> bool { + left.iter().all(|endpoint| { + right + .iter() + .any(|other| endpoint_authority_equal(endpoint, other)) + }) && right.iter().all(|endpoint| { + left.iter() + .any(|other| endpoint_authority_equal(endpoint, other)) + }) +} + +fn endpoint_authority_sets_overlap(left: &[Endpoint], right: &[Endpoint]) -> bool { + left.iter().any(|endpoint| { + right + .iter() + .any(|other| endpoint_authority_may_overlap(endpoint, other)) + }) +} + +fn endpoint_authority_may_overlap(left: &Endpoint, right: &Endpoint) -> bool { + let ports_overlap = left + .effective_ports() + .iter() + .any(|port| right.effective_ports().contains(port)); + let hosts_may_overlap = left.host.eq_ignore_ascii_case(&right.host) + || left.host.contains('*') + || right.host.contains('*'); + ports_overlap && hosts_may_overlap +} + +fn endpoint_authority_equal(left: &Endpoint, right: &Endpoint) -> bool { + let mut left = left.clone(); + let mut right = right.clone(); + left.review = Review::default(); + right.review = Review::default(); + for rule in &mut left.rules { + rule.allow.review = Review::default(); + } + for rule in &mut right.rules { + rule.allow.review = Review::default(); + } + let rules_equal = left.rules.iter().all(|rule| right.rules.contains(rule)) + && right.rules.iter().all(|rule| left.rules.contains(rule)); + let denies_equal = left + .deny_rules + .iter() + .all(|rule| right.deny_rules.contains(rule)) + && right + .deny_rules + .iter() + .all(|rule| left.deny_rules.contains(rule)); + left.rules.clear(); + right.rules.clear(); + left.deny_rules.clear(); + right.deny_rules.clear(); + rules_equal && denies_equal && left == right +} + +fn filesystem_counterexample( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> Option { + let mut maximum_writes = maximum.filesystem_policy.read_write.clone(); + if maximum.filesystem_policy.include_workdir { + maximum_writes.push(WORKDIR_SYMBOL.to_owned()); + } + let mut maximum_reads = maximum.filesystem_policy.read_only.clone(); + maximum_reads.extend(maximum_writes.iter().cloned()); + + candidate + .filesystem_policy + .read_write + .iter() + .find(|path| !path_is_covered(path, &maximum_writes)) + .map(|path| Counterexample::Filesystem { + access: FilesystemAccess::Write, + path: path.clone(), + }) + .or_else(|| { + candidate + .filesystem_policy + .read_only + .iter() + .find(|path| !path_is_covered(path, &maximum_reads)) + .map(|path| Counterexample::Filesystem { + access: FilesystemAccess::Read, + path: path.clone(), + }) + }) +} + +fn path_is_covered(candidate: &str, maximum_paths: &[String]) -> bool { + maximum_paths.iter().any(|maximum| { + maximum == "/" + || candidate == maximum + || candidate + .strip_prefix(maximum) + .is_some_and(|suffix| suffix.starts_with('/')) + }) +} + +fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(ReasonCode, String)> { + let unsupported = |detail: String| { + Some(( + ReasonCode::UnsupportedPolicyShape, + format!("{label} policy {detail}"), + )) + }; + if !policy.extra.is_empty() { + return unsupported(format!( + "uses unsupported top-level fields: {}", + keys(&policy.extra) + )); + } + if label == "candidate" && policy.metadata.is_some() { + return unsupported("contains managed-maximum metadata".to_owned()); + } + if policy + .metadata + .as_ref() + .is_some_and(|metadata| !metadata.extra.is_empty()) + { + return unsupported("uses unsupported managed-metadata fields".to_owned()); + } + if policy.landlock.is_some() + || policy.process.is_some() + || !policy.network_middlewares.is_empty() + { + return unsupported("uses process, Landlock, or network middleware controls".to_owned()); + } + if !policy.filesystem_policy.extra.is_empty() { + return unsupported(format!( + "uses unsupported filesystem fields: {}", + keys(&policy.filesystem_policy.extra) + )); + } + for (rule_name, rule) in &policy.network_policies { + if !rule.extra.is_empty() { + return unsupported(format!("rule '{rule_name}' uses unsupported fields")); + } + for binary in &rule.binaries { + if binary.path.is_empty() + || !is_canonical_pattern_path(&binary.path) + || !binary.extra.is_empty() + || unsupported_glob(&binary.path) + { + return unsupported(format!("rule '{rule_name}' uses an unsupported binary")); + } + } + for endpoint in &rule.endpoints { + let context = format!("rule '{rule_name}'"); + if endpoint.host.is_empty() + || endpoint.effective_ports().is_empty() + || (endpoint.port != 0 && !endpoint.ports.is_empty()) + { + return unsupported(format!("{context} has no unambiguous host and port")); + } + if unsupported_host_glob(&endpoint.host) + || unsupported_glob(&endpoint.path) + || (!endpoint.path.is_empty() && !is_canonical_pattern_path(&endpoint.path)) + { + return unsupported(format!("{context} uses an unsupported glob")); + } + if !endpoint.path.is_empty() && !endpoint.path.starts_with('/') { + return unsupported(format!("{context} uses a non-canonical endpoint path")); + } + if endpoint.host.contains(':') { + return unsupported(format!( + "{context} uses an IP-literal shape outside the DNS host model" + )); + } + if !endpoint.extra.is_empty() + || !endpoint.allowed_ips.is_empty() + || !matches!(endpoint.tls.as_str(), "" | "terminate" | "passthrough") + || endpoint.allow_encoded_slash + || endpoint.websocket_credential_rewrite + || endpoint.request_body_credential_rewrite + || endpoint.allow_uninspected_credentials + || !endpoint.persisted_queries.is_empty() + || !endpoint.graphql_persisted_queries.is_empty() + || endpoint.graphql_max_body_bytes != 0 + || !endpoint.credential_signing.is_empty() + || !endpoint.signing_service.is_empty() + || !endpoint.signing_region.is_empty() + || endpoint.credential_binding.is_some() + || endpoint.json_rpc.is_some() + || endpoint.mcp.is_some() + || !endpoint.review.extra.is_empty() + { + return unsupported(format!( + "{context} uses authority outside the initial model" + )); + } + let protocol = endpoint.protocol.to_ascii_lowercase(); + if !matches!(protocol.as_str(), "" | "tcp" | "rest") { + return unsupported(format!( + "{context} uses protocol '{}'; only L4 TCP and REST are modeled", + endpoint.protocol + )); + } + if protocol == "tcp" && endpoint.host.parse::().is_ok() { + return unsupported(format!( + "{context} uses an IP literal with explicit TCP semantics" + )); + } + if protocol == "rest" { + if endpoint.enforcement != "enforce" { + return unsupported(format!("{context} uses REST without enforced inspection")); + } + if (!endpoint.access.is_empty() && !endpoint.rules.is_empty()) + || (endpoint.access.is_empty() && endpoint.rules.is_empty()) + || (!endpoint.access.is_empty() + && !matches!( + endpoint.access.as_str(), + "read-only" | "read-write" | "full" + )) + { + return unsupported(format!("{context} has an unsupported REST allow shape")); + } + } else if !endpoint.enforcement.is_empty() + || !endpoint.access.is_empty() + || !endpoint.path.is_empty() + || !endpoint.rules.is_empty() + || !endpoint.deny_rules.is_empty() + { + return unsupported(format!("{context} mixes REST controls into L4 authority")); + } + for rule in &endpoint.rules { + if !rule.extra.is_empty() || unsupported_allow(&rule.allow) { + return unsupported(format!("{context} uses an unsupported REST allow rule")); + } + } + for rule in &endpoint.deny_rules { + if unsupported_deny(rule) { + return unsupported(format!("{context} uses an unsupported REST deny rule")); + } + } + } + } + let endpoints = policy + .network_policies + .values() + .flat_map(|rule| rule.endpoints.iter()) + .collect::>(); + if endpoints.iter().enumerate().any(|(index, endpoint)| { + endpoints[index + 1..].iter().any(|other| { + endpoint.protocol_kind() != other.protocol_kind() + && endpoint_authority_may_overlap(endpoint, other) + }) + }) { + return unsupported( + "contains overlapping L4 and REST endpoints whose inspection selection is not modeled" + .to_owned(), + ); + } + None +} + +fn resource_limit_reason( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> Option { + const MAX_RULES: usize = 1_024; + const MAX_ENDPOINTS: usize = 4_096; + const MAX_BINARIES: usize = 4_096; + const MAX_L7_RULES: usize = 16_384; + const MAX_PATTERN_BYTES: usize = 4 * 1024; + const MAX_TOTAL_PATTERN_BYTES: usize = 1024 * 1024; + + let policies = [maximum, candidate]; + let rule_count = policies + .iter() + .map(|policy| policy.network_policies.len()) + .sum::(); + let endpoint_count = policies + .iter() + .flat_map(|policy| policy.network_policies.values()) + .map(|rule| rule.endpoints.len()) + .sum::(); + let binary_count = policies + .iter() + .flat_map(|policy| policy.network_policies.values()) + .map(|rule| rule.binaries.len()) + .sum::(); + let l7_count = policies + .iter() + .flat_map(|policy| policy.network_policies.values()) + .flat_map(|rule| &rule.endpoints) + .map(|endpoint| endpoint.rules.len() + endpoint.deny_rules.len()) + .sum::(); + let mut total_pattern_bytes = 0_usize; + let mut longest_pattern = 0_usize; + for policy in policies { + let mut account = |value: &str| { + total_pattern_bytes = total_pattern_bytes.saturating_add(value.len()); + longest_pattern = longest_pattern.max(value.len()); + }; + for path in policy + .filesystem_policy + .read_only + .iter() + .chain(&policy.filesystem_policy.read_write) + { + account(path); + } + for rule in policy.network_policies.values() { + for binary in &rule.binaries { + account(&binary.path); + } + for endpoint in &rule.endpoints { + account(&endpoint.host); + account(&endpoint.path); + for rule in &endpoint.rules { + account(&rule.allow.path); + account(&rule.allow.method); + } + for rule in &endpoint.deny_rules { + account(&rule.path); + account(&rule.method); + } + } + } + } + + (rule_count > MAX_RULES + || endpoint_count > MAX_ENDPOINTS + || binary_count > MAX_BINARIES + || l7_count > MAX_L7_RULES + || longest_pattern > MAX_PATTERN_BYTES + || total_pattern_bytes > MAX_TOTAL_PATTERN_BYTES) + .then(|| { + format!( + "containment model exceeds resource limits (rules={rule_count}, endpoints={endpoint_count}, binaries={binary_count}, l7_rules={l7_count}, pattern_bytes={total_pattern_bytes}, longest_pattern={longest_pattern})" + ) + }) +} + +fn unsupported_allow(rule: &Allow) -> bool { + rule.method.is_empty() + || !rule.command.is_empty() + || !rule.query.is_empty() + || !rule.operation_type.is_empty() + || !rule.operation_name.is_empty() + || !rule.fields.is_empty() + || rule.tool.is_some() + || !rule.params.is_empty() + || !rule.extra.is_empty() + || !rule.review.extra.is_empty() + || (!rule.path.is_empty() && !rule.path.starts_with('/')) + || (!rule.path.is_empty() && !is_canonical_pattern_path(&rule.path)) + || unsupported_glob(&rule.path) +} + +fn unsupported_deny(rule: &DenyRule) -> bool { + rule.method.is_empty() + || !rule.command.is_empty() + || !rule.query.is_empty() + || !rule.operation_type.is_empty() + || !rule.operation_name.is_empty() + || !rule.fields.is_empty() + || rule.tool.is_some() + || !rule.params.is_empty() + || !rule.extra.is_empty() + || (!rule.path.is_empty() && !rule.path.starts_with('/')) + || (!rule.path.is_empty() && !is_canonical_pattern_path(&rule.path)) + || unsupported_glob(&rule.path) +} + +fn is_canonical_pattern_path(path: &str) -> bool { + path.starts_with('/') + && !path.contains("//") + && !path.split('/').any(|segment| matches!(segment, "." | "..")) +} + +fn keys(values: &BTreeMap) -> String { + values.keys().cloned().collect::>().join(", ") +} + +fn unsupported_glob(pattern: &str) -> bool { + pattern + .chars() + .any(|character| matches!(character, '?' | '[' | ']' | '{' | '}' | '\\')) +} + +fn unsupported_host_glob(pattern: &str) -> bool { + if unsupported_glob(pattern) + || pattern == "*" + || pattern == "**" + || pattern.chars().any(char::is_whitespace) + || pattern.split('.').any(str::is_empty) + { + return true; + } + pattern.split('.').enumerate().any(|(index, label)| { + (label.contains("**") && label != "**") + || (index > 0 && label.contains('*') && label != "*" && label != "**") + }) +} + +fn bool_or(values: impl IntoIterator) -> Bool { + let values = values.into_iter().collect::>(); + if values.is_empty() { + Bool::from_bool(false) + } else { + Bool::or(&values) + } +} + +fn str_eq_any(value: &Z3String, options: &[&str]) -> Bool { + bool_or(options.iter().map(|option| value.eq(*option))) +} + +fn str_eq_any_case_insensitive(value: &Z3String, options: &[&str]) -> Bool { + bool_or( + options + .iter() + .map(|option| value.eq(option.to_ascii_uppercase())), + ) +} + +fn glob_regex(pattern: &str, separator: &str) -> Regexp { + if pattern == "**" { + return Regexp::full(); + } + let mut parts = Vec::new(); + let mut chars = pattern.chars().peekable(); + while let Some(character) = chars.next() { + if character == '*' && chars.peek() == Some(&'*') { + chars.next(); + if separator == "." { + let label = non_separator_regex(separator).plus(); + parts.push(Regexp::concat(&[ + &label, + &Regexp::concat(&[&Regexp::literal("."), &label]).star(), + ])); + } else { + parts.push(Regexp::full()); + } + } else if character == '*' { + let wildcard = non_separator_regex(separator); + parts.push(wildcard.star()); + } else { + parts.push(Regexp::literal(&character.to_string())); + } + } + if parts.is_empty() { + Regexp::literal("") + } else { + let refs = parts.iter().collect::>(); + Regexp::concat(&refs) + } +} + +fn non_separator_regex(separator: &str) -> Regexp { + match separator { + "/" => Regexp::union(&[&Regexp::range(&' ', &'.'), &Regexp::range(&'0', &'~')]), + "." => Regexp::union(&[&Regexp::range(&' ', &'-'), &Regexp::range(&'/', &'~')]), + _ => Regexp::full(), + } +} + +fn host_domain_regex() -> Regexp { + let alphanumeric = Regexp::union(&[&Regexp::range(&'a', &'z'), &Regexp::range(&'0', &'9')]); + let label_character = Regexp::union(&[&alphanumeric, &Regexp::literal("-")]); + let label = Regexp::union(&[ + &alphanumeric, + &Regexp::concat(&[&alphanumeric, &label_character.star(), &alphanumeric]), + ]); + Regexp::concat(&[ + &label, + &Regexp::concat(&[&Regexp::literal("."), &label]).star(), + ]) +} + +#[cfg(test)] +mod tests { + use super::*; + use openshell_core::host_pattern::HostPattern; + use std::fmt::Write as _; + + fn parse(value: &str) -> ContainmentPolicy { + parse_policy_str(value).expect("valid policy") + } + + fn options() -> CheckOptions { + CheckOptions { + timeout: Duration::from_secs(10), + } + } + + #[test] + fn filesystem_containment_and_counterexample() { + let maximum = + parse("version: 1\nfilesystem_policy: { read_only: [/usr], read_write: [/tmp] }\n"); + let within = parse( + "version: 1\nfilesystem_policy: { read_only: [/usr/bin], read_write: [/tmp/cache] }\n", + ); + let exceeds = parse("version: 1\nfilesystem_policy: { read_write: [/workspace] }\n"); + assert!(matches!( + check_within_maximum(&maximum, &within, options()), + CheckResult::Within(_) + )); + assert!(matches!( + check_within_maximum(&maximum, &exceeds, options()), + CheckResult::Exceeds(_) + )); + } + + #[test] + fn l4_contains_rest_but_not_the_reverse() { + let l4 = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let rest = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&l4, &rest, options()), + CheckResult::Within(_) + )); + assert!(matches!( + check_within_maximum(&rest, &l4, options()), + CheckResult::Exceeds(_) + )); + } + + #[test] + fn network_containment_covers_disabled_binary_identity() { + let maximum = parse("version: 1\n"); + let candidate = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: []\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { + binary: None, + binary_identity_required: false, + .. + } + ) + )); + } + + #[test] + fn differing_binary_selectors_are_checked_when_identity_is_required() { + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/wget }]\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { + binary_identity_required: true, + .. + } + ) + )); + } + + #[test] + fn explicit_deny_removes_authority() { + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: full\n deny_rules: [{ method: DELETE, path: /** }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: DELETE, path: /private/resource } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); + } + + #[test] + fn host_wildcard_zero_length_suffix_preserves_exact_deny() { + let maximum = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: 'api*.example.com', port: 443, protocol: rest, enforcement: enforce, access: full }\n binaries: [{ path: /usr/bin/curl }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: full\n deny_rules: [{ method: GET, path: '/**' }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: 'api*.example.com', port: 443, protocol: rest, enforcement: enforce, access: full }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { host, .. } if host == "api.example.com" + ) + )); + } + + #[test] + fn ancestor_binary_can_supply_a_maximum_deny() { + let maximum = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: /usr/bin/curl }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: /usr/bin/python3 }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: /usr/bin/curl }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: /usr/bin/node }]\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { + binary: Some(binary), + ancestor_binary: Some(ancestor), + binary_identity_required: true, + .. + } if binary == "/usr/bin/curl" && ancestor == "/usr/bin/python3" + ) + )); + } + + #[test] + fn exact_maximum_deny_under_candidate_glob_requires_image_resolution() { + let maximum = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: '/**' }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: /venv/bin/python }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: '/**' }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: '/venv/bin/*' }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + )); + } + + #[test] + fn definite_network_expansion_precedes_symlink_uncertainty() { + let maximum = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: '/**' }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: /venv/bin/python }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: '/**' }]\n extra:\n endpoints: [{ host: extra.example.com, port: 443 }]\n binaries: [{ path: '/**' }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: '/venv/bin/*' }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Exceeds(_) + )); + } + + #[test] + fn overlapping_l4_and_rest_authority_is_unsupported() { + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - { host: api.example.com, port: 443 }\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnsupportedPolicyShape + )); + } + + #[test] + fn methods_longer_than_sixty_four_bytes_are_in_the_action_domain() { + let method = "X".repeat(65); + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, rules: [{ allow: { method: GET, path: '/**' } }] }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse(&format!( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - {{ host: api.example.com, port: 443, protocol: rest, enforcement: enforce, rules: [{{ allow: {{ method: {method}, path: '/**' }} }}] }}\n binaries: [{{ path: /usr/bin/curl }}]\n" + )); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { method: Some(value), .. } if value == &method + ) + )); + } + + #[test] + fn rest_methods_and_paths_must_be_narrower() { + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: GET, path: '/repos/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let narrower = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: GET, path: '/repos/NVIDIA/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let broader_method = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: POST, path: '/repos/NVIDIA/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &narrower, options()), + CheckResult::Within(_) + )); + let result = check_within_maximum(&maximum, &broader_method, options()); + assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); + } + + #[test] + fn unknown_and_environment_dependent_shapes_fail_closed() { + let unknown = parse("version: 1\nfuture_authority: true\n"); + assert!(matches!( + check_within_maximum(&unknown, &unknown, options()), + CheckResult::Unsupported(_) + )); + let workdir = parse("version: 1\nfilesystem_policy: { include_workdir: true }\n"); + let empty = parse("version: 1\n"); + assert!(matches!( + check_within_maximum(&empty, &workdir, options()), + CheckResult::Unsupported(_) + )); + let maximum_workdir = parse("version: 1\nfilesystem_policy: { include_workdir: true }\n"); + let explicit = parse("version: 1\nfilesystem_policy: { read_write: [/workspace] }\n"); + assert!(matches!( + check_within_maximum(&maximum_workdir, &explicit, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedWorkdir + )); + } + + #[test] + fn exact_binary_under_a_maximum_glob_requires_image_resolution() { + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*3' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/python3 }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + )); + } + + #[test] + fn unrelated_maximum_glob_does_not_make_exact_containment_unsupported() { + let maximum = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n unrelated:\n endpoints: [{ host: other.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Within(_) + )); + } + + #[test] + fn unrelated_universal_glob_does_not_hide_symlink_ambiguity() { + let maximum = parse( + "version: 1\nnetwork_policies:\n ambiguous:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n unrelated:\n endpoints: [{ host: unrelated.example.com, port: 80 }]\n binaries: [{ path: '/**' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + )); + } + + #[test] + fn shared_glob_does_not_hide_exact_binary_symlink_ambiguity() { + let maximum = parse( + "version: 1\nnetwork_policies:\n shared:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n shared:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }, { path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + )); + } + + #[test] + fn wildcard_endpoint_overlap_does_not_hide_symlink_ambiguity() { + let maximum = parse( + "version: 1\nnetwork_policies:\n shared:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n shared:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + )); + } + + #[test] + fn ambiguity_check_preserves_shared_unrelated_globs() { + let maximum = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n ambiguous:\n endpoints: [{ host: unrelated.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n shared:\n endpoints: [{ host: shared.example.com, port: 443 }, { host: mirror.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n shared:\n endpoints: [{ host: mirror.example.com, port: 443 }, { host: shared.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Within(_) + )); + } + + #[test] + fn reflexive_and_rule_order_invariant() { + let first = parse( + "version: 1\nnetwork_policies:\n a:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n b:\n endpoints: [{ host: api.example.org, port: 8443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let second = parse( + "version: 1\nnetwork_policies:\n b:\n endpoints: [{ host: api.example.org, port: 8443 }]\n binaries: [{ path: /usr/bin/curl }]\n a:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + let reflexive = check_within_maximum(&first, &first, options()); + assert!(matches!(reflexive, CheckResult::Within(_)), "{reflexive:?}"); + assert!(matches!( + check_within_maximum(&first, &second, options()), + CheckResult::Within(_) + )); + assert!(matches!( + check_within_maximum(&second, &first, options()), + CheckResult::Within(_) + )); + } + + #[test] + fn containment_is_transitive() { + let broad = parse("version: 1\nfilesystem_policy: { read_write: [/workspace] }\n"); + let middle = parse("version: 1\nfilesystem_policy: { read_write: [/workspace/project] }\n"); + let narrow = + parse("version: 1\nfilesystem_policy: { read_write: [/workspace/project/cache] }\n"); + assert!(matches!( + check_within_maximum(&broad, &middle, options()), + CheckResult::Within(_) + )); + assert!(matches!( + check_within_maximum(&middle, &narrow, options()), + CheckResult::Within(_) + )); + assert!(matches!( + check_within_maximum(&broad, &narrow, options()), + CheckResult::Within(_) + )); + } + + #[test] + fn removed_binary_harness_field_is_unsupported() { + let policy = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl, harness: true }]\n", + ); + assert!(matches!( + check_within_maximum(&policy, &policy, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnsupportedPolicyShape + )); + } + + #[test] + fn excessive_model_size_is_inconclusive() { + let maximum = parse("version: 1\n"); + let mut candidate = parse("version: 1\n"); + for index in 0..=1_024 { + candidate.network_policies.insert( + format!("rule-{index}"), + NetworkRule { + _name: String::new(), + endpoints: Vec::new(), + binaries: Vec::new(), + extra: BTreeMap::new(), + }, + ); + } + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Inconclusive(ref evidence) + if evidence.reason_code() == ReasonCode::ResourceLimit + )); + } + + #[test] + fn invalid_version_and_relative_path_are_input_errors() { + assert!(parse_policy_str("version: 2\n").is_err()); + assert!(parse_policy_str("version: 1\nfilesystem_policy: { read_only: [tmp] }\n").is_err()); + assert!(parse_policy_str("version: 1\nversion: 1\n").is_err()); + let mut deep = String::from("version: 1\nfuture:\n"); + for depth in 0..=MAX_YAML_DEPTH { + writeln!(deep, "{}level-{depth}:", " ".repeat(depth + 1)).unwrap(); + } + writeln!(deep, "{}true", " ".repeat(MAX_YAML_DEPTH + 2)).unwrap(); + assert!(parse_policy_str(&deep).is_err()); + } + + #[test] + fn rest_counterexamples_must_be_canonical_runtime_paths() { + for path in ["/", "/repos/NVIDIA/", "/a%20b"] { + assert!(is_canonical_rest_path(path), "rejected {path}"); + } + for path in ["/a//b", "/a/../b", "/a/./b", "/a;b", "/a%2fb", "/a%41"] { + assert!(!is_canonical_rest_path(path), "accepted {path}"); + } + } + + #[test] + fn a_pre_cancelled_check_is_inconclusive() { + let policy = parse("version: 1\n"); + let cancelled = AtomicBool::new(true); + assert!(matches!( + check_within_maximum_cancellable(&policy, &policy, options(), &cancelled), + CheckResult::Inconclusive(ref evidence) + if evidence.reason_code() == ReasonCode::Cancelled + )); + } + + #[test] + fn review_reason_and_deprecated_tls_spelling_do_not_change_authority() { + let maximum = parse( + "version: 1\nmetadata: { policy_id: ceiling, version: 7, allowed_modes: [ask], default_mode: ask, audit_label: production }\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n tls: terminate\n enforcement: enforce\n access: read-only\n review: { required: true, reason: sensitive }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules:\n - allow: { method: GET, path: '/v1/**', review: { required: true, reason: inspect } }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Within(_) + )); + let metadata = maximum.metadata().expect("managed metadata retained"); + assert_eq!(metadata.policy_id, "ceiling"); + assert_eq!(metadata.version, 7); + } + + #[test] + fn host_wildcards_do_not_cross_or_elide_labels() { + let maximum = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let nested = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: deep.api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &nested, options()), + CheckResult::Exceeds(_) + )); + let recursive = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: '**.example.com', port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + assert!(matches!( + check_within_maximum(&recursive, &nested, options()), + CheckResult::Within(_) + )); + } + + #[test] + fn host_model_matches_the_runtime_matcher() { + let cases = [ + ("api.example.com", "api.example.com"), + ("api.example.com", "other.example.com"), + ("*.example.com", "api.example.com"), + ("*.example.com", "deep.api.example.com"), + ("**.example.com", "deep.api.example.com"), + ("**.example.com", "example.com"), + ("api*.example.com", "api.example.com"), + ("api*.example.com", "api-v2.example.com"), + ]; + for (pattern, host) in cases { + let runtime = HostPattern::new(pattern).unwrap().matches(host); + let solver = Solver::new(); + let modeled = Z3String::from_str(host) + .unwrap() + .regex_matches(&glob_regex(pattern, ".")); + solver.assert(!modeled); + let prover = solver.check() == SatResult::Unsat; + assert_eq!(prover, runtime, "pattern={pattern} host={host}"); + } + } + + #[test] + fn filesystem_normalization_matches_the_runtime_helper() { + for path in ["/", "/usr//bin/", "/workspace/./cache"] { + let parsed = parse(&format!( + "version: 1\nfilesystem_policy: {{ read_only: [{path}] }}\n" + )); + assert_eq!( + parsed.filesystem_policy.read_only[0], + openshell_core::paths::normalize_path(path) + ); + } + } +} diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs index 913045fe7d..8513cdbcc3 100644 --- a/crates/openshell-prover/src/lib.rs +++ b/crates/openshell-prover/src/lib.rs @@ -8,6 +8,7 @@ //! paths and write-bypass violations. pub mod accepted_risks; +pub mod containment; pub mod credentials; pub mod finding; pub mod model; diff --git a/crates/openshell-prover/tests/runtime_parity.rs b/crates/openshell-prover/tests/runtime_parity.rs new file mode 100644 index 0000000000..8abc3514c7 --- /dev/null +++ b/crates/openshell-prover/tests/runtime_parity.rs @@ -0,0 +1,283 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Regression tests against the network supervisor's actual Rego policy. + +use openshell_prover::containment::{ + CheckOptions, CheckResult, check_within_maximum, parse_policy_str, +}; +use regorus::{Engine, Value}; +use serde_json::json; +use std::time::Duration; + +const SANDBOX_POLICY_REGO: &str = + include_str!("../../openshell-supervisor-network/data/sandbox-policy.rego"); + +fn check(maximum: &str, candidate: &str) -> CheckResult { + let maximum = parse_policy_str(maximum).expect("maximum policy should parse"); + let candidate = parse_policy_str(candidate).expect("candidate policy should parse"); + check_within_maximum( + &maximum, + &candidate, + CheckOptions { + timeout: Duration::from_secs(5), + }, + ) +} + +fn runtime_engine(policy: &str) -> Engine { + let yaml: serde_yml::Value = serde_yml::from_str(policy).expect("valid policy YAML"); + let mut data = serde_json::to_value(yaml).expect("policy converts to JSON"); + data.as_object_mut().expect("policy is an object").insert( + "runtime".to_owned(), + json!({ "require_binary_identity": true }), + ); + + let mut engine = Engine::new(); + engine + .add_policy("sandbox-policy.rego".into(), SANDBOX_POLICY_REGO.into()) + .expect("runtime Rego should compile"); + engine + .add_data_json(&data.to_string()) + .expect("runtime policy data should load"); + engine +} + +fn runtime_input(binary: &str, ancestors: &[&str], host: &str, method: &str) -> Value { + serde_json::from_value(json!({ + "exec": { + "path": binary, + "ancestors": ancestors, + "cmdline_paths": [], + }, + "network": { + "host": host, + "port": 443, + }, + "request": { + "method": method, + "path": "/", + "query_params": {}, + }, + })) + .expect("input converts to a Rego value") +} + +fn eval_bool(engine: &mut Engine, input: &Value, rule: &str) -> bool { + engine.set_input(input.clone()); + engine + .eval_rule(rule.into()) + .expect("runtime rule should evaluate") + == Value::from(true) +} + +fn eval_array_len(engine: &mut Engine, input: &Value, rule: &str) -> usize { + engine.set_input(input.clone()); + match engine + .eval_rule(rule.into()) + .expect("runtime rule should evaluate") + { + Value::Array(values) => values.len(), + Value::Undefined => 0, + value => panic!("expected array from {rule}, got {value:?}"), + } +} + +#[test] +fn intra_label_host_wildcard_matches_empty_suffix_at_runtime() { + let maximum = r#" +version: 1 +network_policies: + grant: + endpoints: + - host: api*.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{ allow: { method: GET, path: "/**" } }] + binaries: [{ path: /usr/bin/curl }] + exact_deny: + endpoints: + - host: api.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{ allow: { method: GET, path: "/**" } }] + deny_rules: [{ method: GET, path: "/**" }] + binaries: [{ path: /usr/bin/curl }] +"#; + let candidate = r#" +version: 1 +network_policies: + grant: + endpoints: + - host: api*.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{ allow: { method: GET, path: "/**" } }] + binaries: [{ path: /usr/bin/curl }] +"#; + let input = runtime_input("/usr/bin/curl", &[], "api.example.com", "GET"); + let mut maximum_runtime = runtime_engine(maximum); + let mut candidate_runtime = runtime_engine(candidate); + + assert!(eval_bool( + &mut candidate_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + assert!(!eval_bool( + &mut maximum_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + assert!(matches!(check(maximum, candidate), CheckResult::Exceeds(_))); +} + +#[test] +fn ancestor_identity_applies_to_runtime_denies() { + let maximum = policy_with_ancestor_deny("/usr/bin/python3"); + let candidate = policy_with_ancestor_deny("/usr/bin/node"); + let input = runtime_input("/usr/bin/curl", &["/usr/bin/python3"], "example.com", "GET"); + let mut maximum_runtime = runtime_engine(&maximum); + let mut candidate_runtime = runtime_engine(&candidate); + + assert!(eval_bool( + &mut candidate_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + assert!(!eval_bool( + &mut maximum_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + assert!(matches!( + check(&maximum, &candidate), + CheckResult::Exceeds(_) + )); +} + +fn policy_with_ancestor_deny(denied_binary: &str) -> String { + format!( + r#" +version: 1 +network_policies: + grant: + endpoints: + - host: example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{{ allow: {{ method: GET, path: "/**" }} }}] + binaries: [{{ path: /usr/bin/curl }}] + deny: + endpoints: + - host: example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{{ allow: {{ method: GET, path: "/**" }} }}] + deny_rules: [{{ method: "*", path: "/**" }}] + binaries: [{{ path: {denied_binary} }}] +"# + ) +} + +#[test] +fn inspected_endpoint_restricts_an_overlapping_l4_grant() { + let maximum = r#" +version: 1 +network_policies: + egress: + endpoints: + - { host: api.example.com, ports: [443] } + - host: api.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{ allow: { method: GET, path: "/**" } }] + binaries: [{ path: /usr/bin/curl }] +"#; + let candidate = r" +version: 1 +network_policies: + egress: + endpoints: + - { host: api.example.com, ports: [443] } + binaries: [{ path: /usr/bin/curl }] +"; + let input = runtime_input("/usr/bin/curl", &[], "api.example.com", "POST"); + let mut maximum_runtime = runtime_engine(maximum); + let mut candidate_runtime = runtime_engine(candidate); + + assert_eq!( + eval_array_len( + &mut candidate_runtime, + &input, + "data.openshell.sandbox._matching_endpoint_configs" + ), + 0 + ); + assert_eq!( + eval_array_len( + &mut maximum_runtime, + &input, + "data.openshell.sandbox._matching_endpoint_configs" + ), + 1 + ); + assert!(!eval_bool( + &mut maximum_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + let result = check(maximum, candidate); + assert!( + matches!(result, CheckResult::Unsupported(_)), + "overlapping inspection must be rejected explicitly: {result:?}" + ); +} + +#[test] +fn runtime_accepts_methods_longer_than_sixty_four_bytes() { + let long_method = "X".repeat(65); + let maximum = rest_method_policy("GET"); + let candidate = rest_method_policy(&long_method); + let input = runtime_input("/usr/bin/curl", &[], "api.example.com", &long_method); + let mut maximum_runtime = runtime_engine(&maximum); + let mut candidate_runtime = runtime_engine(&candidate); + + assert!(eval_bool( + &mut candidate_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + assert!(!eval_bool( + &mut maximum_runtime, + &input, + "data.openshell.sandbox.allow_request" + )); + assert!(matches!( + check(&maximum, &candidate), + CheckResult::Exceeds(_) + )); +} + +fn rest_method_policy(method: &str) -> String { + format!( + r#" +version: 1 +network_policies: + egress: + endpoints: + - host: api.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{{ allow: {{ method: "{method}", path: "/**" }} }}] + binaries: [{{ path: /usr/bin/curl }}] +"# + ) +} diff --git a/crates/openshell-supervisor-network/src/opa.rs b/crates/openshell-supervisor-network/src/opa.rs index c8f303d64f..a64a07a9a2 100644 --- a/crates/openshell-supervisor-network/src/opa.rs +++ b/crates/openshell-supervisor-network/src/opa.rs @@ -9068,6 +9068,94 @@ network_policies: ); } + #[cfg(target_os = "linux")] + #[test] + fn exact_deny_symlink_expands_but_glob_deny_does_not() { + use std::os::unix::fs::symlink; + + if !procfs_root_accessible() { + eprintln!("Skipping: /proc//root/ not accessible in this environment"); + return; + } + + let link_dir = tempfile::tempdir().unwrap(); + let target_dir = tempfile::tempdir().unwrap(); + let target = target_dir.path().join("python3"); + let link = link_dir.path().join("python"); + std::fs::write(&target, b"python binary").unwrap(); + symlink(&target, &link).unwrap(); + + let target_path = target.to_string_lossy(); + let exact_link = link.to_string_lossy(); + let candidate_glob = format!("{}/*", link_dir.path().to_string_lossy()); + let policy = |deny_binary: &str| { + format!( + r#" +version: 1 +network_policies: + grant: + endpoints: + - host: example.com + port: 443 + protocol: rest + enforcement: enforce + rules: [{{ allow: {{ method: GET, path: "/**" }} }}] + binaries: [{{ path: "{target_path}" }}] + deny: + endpoints: + - host: example.com + port: 443 + protocol: rest + enforcement: enforce + rules: [{{ allow: {{ method: GET, path: "/**" }} }}] + deny_rules: [{{ method: "*", path: "/**" }}] + binaries: [{{ path: "{deny_binary}" }}] +filesystem_policy: + include_workdir: false + read_only: [] + read_write: [] +landlock: + compatibility: best_effort +process: + run_as_user: sandbox + run_as_group: sandbox +"# + ) + }; + + let maximum = openshell_policy::parse_sandbox_policy(&policy(&exact_link)) + .expect("maximum policy should parse"); + let candidate = openshell_policy::parse_sandbox_policy(&policy(&candidate_glob)) + .expect("candidate policy should parse"); + let pid = std::process::id(); + let maximum_engine = + OpaEngine::from_proto_with_pid(&maximum, pid).expect("maximum engine should load"); + let candidate_engine = + OpaEngine::from_proto_with_pid(&candidate, pid).expect("candidate engine should load"); + let input = serde_json::json!({ + "network": { "host": "example.com", "port": 443 }, + "exec": { + "path": target_path, + "ancestors": [], + "cmdline_paths": [] + }, + "request": { + "method": "GET", + "path": "/", + "query_params": {} + } + }); + + assert!( + eval_l7(&candidate_engine, &input), + "the candidate glob must not be resolved through the exact symlink" + ); + assert!( + !eval_l7(&maximum_engine, &input), + "the maximum exact deny must expand to the resolved target" + ); + } + #[cfg(target_os = "linux")] #[test] fn reload_from_proto_with_pid_resolves_symlinks() { diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx new file mode 100644 index 0000000000..984dafebb0 --- /dev/null +++ b/docs/reference/policy-prover.mdx @@ -0,0 +1,160 @@ +--- +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 +title: "Standalone Policy Prover" +sidebar-title: "Policy Prover" +description: "Install and use the standalone OpenShell policy prover to check a local candidate policy against a managed maximum." +keywords: "Generative AI, Cybersecurity, Policy, Prover, Maximum, Containment, CI" +position: 4 +--- + +`openshell-prover` checks whether the authority in a local candidate policy is +contained within a local maximum policy. The command reads files from the host +and does not connect to an OpenShell gateway. + +The candidate must be the fully composed effective policy after the proposed +change, including any provider-contributed authority. The maximum is an +operator-owned ceiling. It does not grant authority by itself. + +## Install the Prover + +Download the archive for your platform from the +[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases) page: + +| Platform | Archive | +|---|---| +| Linux x86_64 | `openshell-prover-x86_64-unknown-linux-musl.tar.gz` | +| Linux aarch64 | `openshell-prover-aarch64-unknown-linux-musl.tar.gz` | +| macOS Apple Silicon | `openshell-prover-aarch64-apple-darwin.tar.gz` | + +Download `openshell-prover-checksums-sha256.txt` from the same release. On +Linux, verify the selected archive before extracting it: + +```shell +archive=openshell-prover-x86_64-unknown-linux-musl.tar.gz +grep " ${archive}$" openshell-prover-checksums-sha256.txt | sha256sum --check +tar -xzf "${archive}" +mkdir -p ~/.local/bin +install -m 0755 openshell-prover ~/.local/bin/openshell-prover +``` + +On macOS, use `shasum` for verification: + +```shell +archive=openshell-prover-aarch64-apple-darwin.tar.gz +grep " ${archive}$" openshell-prover-checksums-sha256.txt | shasum -a 256 --check +tar -xzf "${archive}" +mkdir -p ~/.local/bin +install -m 0755 openshell-prover ~/.local/bin/openshell-prover +``` + +The release archive includes the solver linkage required by the executable. +It does not require the main `openshell` command, a gateway configuration, or +a separate Z3 installation. + +## Check a Policy Boundary + +Create a maximum policy: + +```yaml +version: 1 +filesystem_policy: + read_only: + - /usr + - /etc + read_write: + - /tmp +``` + +Create the fully composed candidate policy: + +```yaml +version: 1 +filesystem_policy: + read_only: + - /usr/bin + read_write: + - /tmp/cache +``` + +Run the check: + +```shell +openshell-prover check candidate.yaml --maximum maximum.yaml +``` + +A contained candidate prints `result: within_max` and exits with status `0`. +Use JSON when a script consumes the result: + +```shell +openshell-prover check candidate.yaml \ + --maximum maximum.yaml \ + --output json +``` + +The JSON object includes the result, exit code, input paths, prover version, +model scope, checked policy version, modeled domains, and assumptions. An +exceeding result also includes a filesystem or network counterexample. +Automation should use `result` and `reason_code` instead of parsing the +human-readable explanation. + +The solver has a finite 10-second default budget. Set a different positive +budget with an integer followed by `ms`, `s`, or `m`: + +```shell +openshell-prover check candidate.yaml \ + --maximum maximum.yaml \ + --timeout 30s \ + --output json +``` + +## Exit Codes + +| Exit | Result | Meaning | +|---|---|---| +| `0` | `within_max` | Containment was established for the reported model scope. | +| `1` | `exceeds_max` | The candidate exceeds the maximum; inspect the counterexample. | +| `2` | `error` | Arguments, input files, policy syntax, or command execution prevented a valid check. | +| `3` | `unsupported` or `inconclusive` | The model cannot soundly cover the policy shape, or the solver did not reach a determination. | +| `130` | `inconclusive` when graceful handling completes | The user interrupted the command with Ctrl-C on Unix; a second or very early interruption may prevent output. | + +Only exit `0` means the verification succeeded. Treat unsupported and +inconclusive results as failures in CI. + +## Interpretation and Limits + +The initial containment model covers filesystem paths, L4 network authority, +and enforced REST method and path authority, including explicit REST denies. +The result object reports the domains used for each check. Policies that use +recognized authority outside that model return `unsupported` rather than +silently ignoring it. + +Containment means `Allowed(candidate)` is a subset of `Allowed(maximum)` under +the reported model. It does not establish least privilege, automatic approval +eligibility, semantic safety, or equivalence to a running sandbox's kernel +state. In particular: + +- The command does not fetch the current sandbox policy or compose provider + rules. The caller must supply the effective candidate. +- The command does not apply, approve, or persist a policy. +- A policy inside a review-required region can pass containment and still + require human review. +- Environment-dependent authority, such as an unresolved image workdir, + returns `unsupported` when the result depends on that missing context. +- Binary comparisons that can change when an image resolves an exact selector + through a symlink return `unsupported`. This covers exact candidate grants + under maximum globs and exact maximum denies replaced by candidate globs. + Use matching exact canonical paths when possible. +- Policies with overlapping L4 and enforced REST endpoints return + `unsupported` because inspection selection depends on the complete set of + matching runtime endpoint configurations. +- Network containment checks both supported runtime configurations: binary + identity enforcement enabled and disabled. When enabled, grants and denies + match the executable or an ancestor identity. Network counterexamples report + the configuration and identities that expose the additional authority. +- Both files are interpreted in the same sandbox filesystem namespace and + mount model. The CLI does not resolve sandbox paths against the host. + +Use the [Policy Schema Reference](/reference/policy-schema) for the full policy +language. A successful prover result covers only the scope reported in its +evidence. From a86633f767b89f1a053b99ad4e21020748b5e0c6 Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 20:10:01 +0000 Subject: [PATCH 02/12] refactor(prover): simplify check scope schema Signed-off-by: Johnny Greco --- crates/openshell-prover-cli/src/main.rs | 6 ------ crates/openshell-prover-cli/tests/cli.rs | 9 ++++++++- crates/openshell-prover/src/containment.rs | 8 -------- docs/reference/policy-prover.mdx | 10 ++++++---- 4 files changed, 14 insertions(+), 19 deletions(-) diff --git a/crates/openshell-prover-cli/src/main.rs b/crates/openshell-prover-cli/src/main.rs index 4b3139aa48..3209112a8c 100644 --- a/crates/openshell-prover-cli/src/main.rs +++ b/crates/openshell-prover-cli/src/main.rs @@ -76,7 +76,6 @@ struct ScopeJson<'a> { model_version: &'a str, policy_version: u32, domains: Vec<&'a str>, - assumptions: &'a [&'a str], } #[derive(Debug, Serialize)] @@ -358,7 +357,6 @@ fn scope_json(scope: &CheckScope) -> ScopeJson<'_> { model_version: scope.model_version, policy_version: scope.policy_version, domains: scope.domains.iter().map(|domain| domain.as_str()).collect(), - assumptions: scope.assumptions, } } @@ -415,10 +413,6 @@ fn render_text(mut writer: impl Write, envelope: &Envelope<'_>) -> Result<(), St scope.domains.join(",") ) .map_err(|error| format!("failed to write output: {error}"))?; - for assumption in scope.assumptions { - writeln!(writer, "assumption: {}", escape_terminal(assumption)) - .map_err(|error| format!("failed to write output: {error}"))?; - } } if let Some(counterexample) = &envelope.counterexample { match counterexample { diff --git a/crates/openshell-prover-cli/tests/cli.rs b/crates/openshell-prover-cli/tests/cli.rs index 06c1da5c0b..cf4c6aba1b 100644 --- a/crates/openshell-prover-cli/tests/cli.rs +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -77,7 +77,14 @@ fn contained_policy_returns_stable_json_and_zero() { assert_eq!(value["check"], "maximum_boundary"); assert_eq!(value["result"], "within_max"); assert_eq!(value["exit_code"], 0); - assert!(value["scope"]["domains"].is_array()); + assert_eq!( + value["scope"], + serde_json::json!({ + "model_version": "maximum-boundary-v1", + "policy_version": 1, + "domains": ["filesystem", "network_l4", "network_rest"] + }) + ); assert!(value["counterexample"].is_null()); } diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index e95fb8589a..8d28cfdc98 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -406,7 +406,6 @@ pub struct CheckScope { pub model_version: &'static str, pub policy_version: u32, pub domains: &'static [CheckDomain], - pub assumptions: &'static [&'static str], } static DOMAINS: &[CheckDomain] = &[ @@ -414,18 +413,11 @@ static DOMAINS: &[CheckDomain] = &[ CheckDomain::NetworkL4, CheckDomain::NetworkRest, ]; -static ASSUMPTIONS: &[&str] = &[ - "Candidate and maximum use the same sandbox filesystem namespace and mount interpretation.", - "Network containment covers runtime configurations with binary identity checks enabled and disabled.", - "REST witnesses use canonical request methods and paths.", -]; - fn check_scope() -> &'static CheckScope { static SCOPE: CheckScope = CheckScope { model_version: "maximum-boundary-v1", policy_version: 1, domains: DOMAINS, - assumptions: ASSUMPTIONS, }; &SCOPE } diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx index 984dafebb0..8b5351aec6 100644 --- a/docs/reference/policy-prover.mdx +++ b/docs/reference/policy-prover.mdx @@ -93,10 +93,11 @@ openshell-prover check candidate.yaml \ ``` The JSON object includes the result, exit code, input paths, prover version, -model scope, checked policy version, modeled domains, and assumptions. An -exceeding result also includes a filesystem or network counterexample. -Automation should use `result` and `reason_code` instead of parsing the -human-readable explanation. +model version, checked policy version, and modeled domains. The documented +semantics and environmental conditions for that scope are tied to its model +version. An exceeding result also includes a filesystem or network +counterexample. Automation should use `result` and `reason_code` instead of +parsing the human-readable explanation. The solver has a finite 10-second default budget. Set a different positive budget with an integer followed by `ms`, `s`, or `m`: @@ -152,6 +153,7 @@ state. In particular: identity enforcement enabled and disabled. When enabled, grants and denies match the executable or an ancestor identity. Network counterexamples report the configuration and identities that expose the additional authority. +- REST containment witnesses use canonical request methods and paths. - Both files are interpreted in the same sandbox filesystem namespace and mount model. The CLI does not resolve sandbox paths against the host. From f620c2f13b277c68df18b9d97ac805c86f62dd2b Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 21:36:57 +0000 Subject: [PATCH 03/12] fix(prover): align containment and cancellation with runtime Signed-off-by: Johnny Greco --- architecture/security-policy.md | 10 +- crates/openshell-prover-cli/tests/cli.rs | 100 ++++++-- .../tests/fixtures/candidate-contained.yaml | 4 +- .../tests/fixtures/maximum-no-write.yaml | 7 + crates/openshell-prover/src/containment.rs | 231 +++++++++++++++--- .../openshell-prover/tests/runtime_parity.rs | 62 +++++ docs/reference/policy-prover.mdx | 15 +- 7 files changed, 365 insertions(+), 64 deletions(-) create mode 100644 crates/openshell-prover-cli/tests/fixtures/maximum-no-write.yaml diff --git a/architecture/security-policy.md b/architecture/security-policy.md index a6e222d448..1b810372fc 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -352,12 +352,16 @@ for an exceeding witness. Recognized authority outside the reviewed model produces an unsupported result rather than being silently ignored. Environment-dependent authority also remains unsupported when the result depends on context that is unavailable to the local command. This includes an -unresolved workdir, binary containment that depends on image-specific symlink -resolution, and overlapping L4 and REST endpoints whose inspection selection +unresolved workdir, filesystem or binary containment that depends on image-specific +path resolution, and overlapping L4 and REST endpoints whose inspection selection depends on the complete runtime endpoint set. Candidate and maximum paths use the same sandbox namespace and mount interpretation; the checker does not resolve them against the CLI host or verify kernel enforcement in a running -sandbox. +sandbox. Filesystem checks assume stable path resolution when enforcement rules +are created. They support matching paths, grant removal, write-to-read reduction, +and a maximum root grant. Other comparisons between paths remain unsupported; +lexical ancestry or distinctness alone cannot establish resolved ancestry or +distinctness. Adding access when the maximum grants none produces a counterexample. This containment operation is separate from the proposal-risk queries below. See the [standalone policy prover documentation](../docs/reference/policy-prover.mdx) diff --git a/crates/openshell-prover-cli/tests/cli.rs b/crates/openshell-prover-cli/tests/cli.rs index cf4c6aba1b..0e74311bdf 100644 --- a/crates/openshell-prover-cli/tests/cli.rs +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -90,7 +90,7 @@ fn contained_policy_returns_stable_json_and_zero() { #[test] fn exceeding_policy_returns_counterexample_and_one() { - let output = check_json("candidate-exceeds.yaml", "maximum.yaml"); + let output = check_json("candidate-exceeds.yaml", "maximum-no-write.yaml"); assert_eq!( output.status.code(), Some(1), @@ -268,40 +268,71 @@ fn fifo_input_is_rejected_without_blocking() { #[cfg(unix)] #[test] fn sigint_interrupts_the_check_with_exit_130() { - let path = std::env::temp_dir().join(format!( - "openshell-prover-cancellation-{}.yaml", + let directory = std::env::temp_dir().join(format!( + "openshell-prover-cancellation-{}", std::process::id() )); - let mut source = String::from("version: 1\nnetwork_policies:\n"); - for index in 0..500 { - writeln!( - source, - " rule-{index}:\n endpoints: [{{ host: host-{index}.example.com, port: 443 }}]\n binaries: [{{ path: /usr/bin/curl }}]" + fs::create_dir_all(&directory).unwrap(); + let policy = |paths: Vec| { + serde_json::json!({ + "version": 1, + "network_policies": {"many": { + "binaries": [{"path": "/usr/bin/curl"}], + "endpoints": [{"host": "api.example.com", "port": 443, + "protocol": "rest", "enforcement": "enforce", + "rules": paths.into_iter().map(|path| serde_json::json!({ + "allow": {"method": "GET", "path": path} + })).collect::>() + }] + }} + }) + }; + let candidate = directory.join("candidate.yaml"); + let maximum = directory.join("maximum.yaml"); + fs::write( + &candidate, + policy(vec!["/route*/**/tail*".into()]).to_string(), + ) + .unwrap(); + fs::write( + &maximum, + policy( + (0..300) + .map(|index| format!("/route{index}/**/tail*")) + .collect(), ) - .unwrap(); - } - fs::write(&path, source).expect("write cancellation policy"); + .to_string(), + ) + .unwrap(); - let child = Command::new(env!("CARGO_BIN_EXE_openshell-prover")) + let mut child = Command::new(env!("CARGO_BIN_EXE_openshell-prover")) .args([ "check", - path.to_str().expect("UTF-8 temporary path"), + candidate.to_str().expect("UTF-8 temporary path"), "--maximum", - path.to_str().expect("UTF-8 temporary path"), + maximum.to_str().expect("UTF-8 temporary path"), "--output", "json", + "--timeout", + "10s", ]) .stdout(Stdio::piped()) .spawn() .expect("start cancellable prover"); - thread::sleep(Duration::from_millis(25)); + // Different policies force a real solve; an identical pair can exit via + // the equality shortcut before SIGINT ever exercises Z3's signal handling. + thread::sleep(Duration::from_millis(500)); + assert!( + child.try_wait().unwrap().is_none(), + "fixture must still be solving when interrupted" + ); let signal = Command::new("kill") .args(["-s", "INT", &child.id().to_string()]) .status() .expect("send SIGINT"); assert!(signal.success()); let output = child.wait_with_output().expect("wait for cancelled prover"); - fs::remove_file(path).expect("remove cancellation policy"); + fs::remove_dir_all(directory).expect("remove cancellation policies"); assert_eq!(output.status.code(), Some(130)); let value: Value = serde_json::from_slice(&output.stdout).expect("structured cancellation JSON"); @@ -309,3 +340,40 @@ fn sigint_interrupts_the_check_with_exit_130() { assert_eq!(value["reason_code"], "cancelled"); assert_eq!(value["exit_code"], 130); } + +#[cfg(unix)] +#[test] +fn symlink_descendants_require_sandbox_path_resolution() { + let directory = + std::env::temp_dir().join(format!("openshell-prover-symlink-{}", std::process::id())); + let safe = directory.join("safe"); + let outside = directory.join("outside"); + fs::create_dir_all(&safe).unwrap(); + fs::create_dir_all(&outside).unwrap(); + std::os::unix::fs::symlink(&outside, safe.join("link")).unwrap(); + for access in ["read_only", "read_write"] { + let candidate = directory.join("candidate.yaml"); + let maximum = directory.join("maximum.yaml"); + for (file, path) in [(&candidate, safe.join("link")), (&maximum, safe.clone())] { + fs::write( + file, + serde_json::json!({"version": 1, "filesystem_policy": {access: [path]}}) + .to_string(), + ) + .unwrap(); + } + let output = run(&[ + "check", + candidate.to_str().unwrap(), + "--maximum", + maximum.to_str().unwrap(), + "--output", + "json", + ]); + assert_eq!(output.status.code(), Some(3)); + let value: Value = serde_json::from_slice(&output.stdout).unwrap(); + assert_eq!(value["result"], "unsupported"); + assert_eq!(value["reason_code"], "unresolved_filesystem_path"); + } + fs::remove_dir_all(directory).unwrap(); +} diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml index 59fe39368f..308d88f1ba 100644 --- a/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-contained.yaml @@ -4,6 +4,6 @@ version: 1 filesystem_policy: read_only: - - /usr/bin + - /usr read_write: - - /tmp/cache + - /tmp diff --git a/crates/openshell-prover-cli/tests/fixtures/maximum-no-write.yaml b/crates/openshell-prover-cli/tests/fixtures/maximum-no-write.yaml new file mode 100644 index 0000000000..9af13cd154 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/maximum-no-write.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +filesystem_policy: + read_only: + - /usr diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index 8d28cfdc98..c9afc4c12f 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -358,6 +358,7 @@ pub enum ReasonCode { UnsupportedPolicyShape, UnresolvedWorkdir, UnresolvedBinaryPath, + UnresolvedFilesystemPath, SolverTimeout, SolverUnknown, ResourceLimit, @@ -372,6 +373,7 @@ impl ReasonCode { Self::UnsupportedPolicyShape => "unsupported_policy_shape", Self::UnresolvedWorkdir => "unresolved_workdir", Self::UnresolvedBinaryPath => "unresolved_binary_path", + Self::UnresolvedFilesystemPath => "unresolved_filesystem_path", Self::SolverTimeout => "solver_timeout", Self::SolverUnknown => "solver_unknown", Self::ResourceLimit => "resource_limit", @@ -609,8 +611,9 @@ fn check_within_maximum_inner( if maximum == candidate { return CheckResult::Within(WithinEvidence); } - if let Some(counterexample) = filesystem_counterexample(maximum, candidate) { - return CheckResult::Exceeds(ExceedsEvidence(counterexample)); + let filesystem_result = check_filesystem(maximum, candidate); + if let Some(result @ CheckResult::Exceeds(_)) = filesystem_result { + return result; } let started = Instant::now(); for binary_identity_required in [false, true] { @@ -659,7 +662,7 @@ fn check_within_maximum_inner( .to_owned(), ); } - CheckResult::Within(WithinEvidence) + filesystem_result.unwrap_or(CheckResult::Within(WithinEvidence)) } fn solve_network_mode( @@ -691,6 +694,11 @@ fn solve_network_mode( } let mut params = Params::new(); params.set_u32("timeout", remaining_ms); + if cancelled.is_some() { + // The caller owns SIGINT. Z3's handler would replace it during check(), + // leaving the cancellation flag unset even when the solve is interrupted. + params.set_bool("ctrl_c", false); + } solver.set_params(¶ms); let solve_result = solver_check(&solver, cancelled); if cancelled.is_some_and(|flag| flag.load(Ordering::Relaxed)) { @@ -1341,10 +1349,10 @@ fn endpoint_authority_equal(left: &Endpoint, right: &Endpoint) -> bool { rules_equal && denies_equal && left == right } -fn filesystem_counterexample( +fn check_filesystem( maximum: &ContainmentPolicy, candidate: &ContainmentPolicy, -) -> Option { +) -> Option { let mut maximum_writes = maximum.filesystem_policy.read_write.clone(); if maximum.filesystem_policy.include_workdir { maximum_writes.push(WORKDIR_SYMBOL.to_owned()); @@ -1352,36 +1360,49 @@ fn filesystem_counterexample( let mut maximum_reads = maximum.filesystem_policy.read_only.clone(); maximum_reads.extend(maximum_writes.iter().cloned()); - candidate - .filesystem_policy - .read_write - .iter() - .find(|path| !path_is_covered(path, &maximum_writes)) - .map(|path| Counterexample::Filesystem { - access: FilesystemAccess::Write, - path: path.clone(), - }) - .or_else(|| { - candidate - .filesystem_policy - .read_only - .iter() - .find(|path| !path_is_covered(path, &maximum_reads)) - .map(|path| Counterexample::Filesystem { - access: FilesystemAccess::Read, - path: path.clone(), - }) - }) + let mut unresolved = None; + for (access, candidates, maxima) in [ + ( + FilesystemAccess::Write, + &candidate.filesystem_policy.read_write, + &maximum_writes, + ), + ( + FilesystemAccess::Read, + &candidate.filesystem_policy.read_only, + &maximum_reads, + ), + ] { + for path in candidates { + if path_is_covered(path, maxima) { + continue; + } + if maxima.is_empty() { + return Some(CheckResult::Exceeds(ExceedsEvidence( + Counterexample::Filesystem { + access, + path: path.clone(), + }, + ))); + } + // Landlock resolves paths in the sandbox. Lexical descendants can + // point outside an ancestor, and unrelated paths can alias it. + unresolved = Some(unsupported( + ReasonCode::UnresolvedFilesystemPath, + format!( + "filesystem {access} containment for '{path}' depends on sandbox path resolution; use matching paths in candidate and maximum", + access = access.as_str() + ), + )); + } + } + unresolved } fn path_is_covered(candidate: &str, maximum_paths: &[String]) -> bool { - maximum_paths.iter().any(|maximum| { - maximum == "/" - || candidate == maximum - || candidate - .strip_prefix(maximum) - .is_some_and(|suffix| suffix.starts_with('/')) - }) + maximum_paths + .iter() + .any(|maximum| maximum == "/" || candidate == maximum) } fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(ReasonCode, String)> { @@ -1707,6 +1728,9 @@ fn glob_regex(pattern: &str, separator: &str) -> Regexp { if pattern == "**" { return Regexp::full(); } + if separator == "/" { + return path_glob_regex(pattern); + } let mut parts = Vec::new(); let mut chars = pattern.chars().peekable(); while let Some(character) = chars.next() { @@ -1736,6 +1760,46 @@ fn glob_regex(pattern: &str, separator: &str) -> Regexp { } } +fn path_glob_regex(pattern: &str) -> Regexp { + let mut parts = Vec::new(); + let mut segments = pattern.split('/').peekable(); + while let Some(segment) = segments.next() { + if segment == "**" { + // glob.match collapses consecutive recursive components. A middle + // ** includes its following slash and can match zero directories. + while segments.peek() == Some(&"**") { + segments.next(); + } + let recursive = Regexp::full(); + parts.push(if segments.peek().is_some() { + Regexp::union(&[ + &Regexp::literal(""), + &Regexp::concat(&[&recursive, &Regexp::literal("/")]), + ]) + } else { + recursive + }); + } else { + for character in segment.chars() { + // Embedded stars, including **, cannot cross a separator. + parts.push(if character == '*' { + non_separator_regex("/").star() + } else { + Regexp::literal(&character.to_string()) + }); + } + if segments.peek().is_some() { + parts.push(Regexp::literal("/")); + } + } + } + if parts.is_empty() { + Regexp::literal("") + } else { + Regexp::concat(&parts.iter().collect::>()) + } +} + fn non_separator_regex(separator: &str) -> Regexp { match separator { "/" => Regexp::union(&[&Regexp::range(&' ', &'.'), &Regexp::range(&'0', &'~')]), @@ -1777,16 +1841,14 @@ mod tests { fn filesystem_containment_and_counterexample() { let maximum = parse("version: 1\nfilesystem_policy: { read_only: [/usr], read_write: [/tmp] }\n"); - let within = parse( - "version: 1\nfilesystem_policy: { read_only: [/usr/bin], read_write: [/tmp/cache] }\n", - ); + let within = parse("version: 1\nfilesystem_policy: { read_only: [/usr, /tmp] }\n"); let exceeds = parse("version: 1\nfilesystem_policy: { read_write: [/workspace] }\n"); assert!(matches!( check_within_maximum(&maximum, &within, options()), CheckResult::Within(_) )); assert!(matches!( - check_within_maximum(&maximum, &exceeds, options()), + check_within_maximum(&parse("version: 1\n"), &exceeds, options()), CheckResult::Exceeds(_) )); } @@ -2122,10 +2184,9 @@ mod tests { #[test] fn containment_is_transitive() { - let broad = parse("version: 1\nfilesystem_policy: { read_write: [/workspace] }\n"); - let middle = parse("version: 1\nfilesystem_policy: { read_write: [/workspace/project] }\n"); - let narrow = - parse("version: 1\nfilesystem_policy: { read_write: [/workspace/project/cache] }\n"); + let broad = parse("version: 1\nfilesystem_policy: { read_write: [/workspace, /tmp] }\n"); + let middle = parse("version: 1\nfilesystem_policy: { read_write: [/workspace] }\n"); + let narrow = parse("version: 1\nfilesystem_policy: { read_only: [/workspace] }\n"); assert!(matches!( check_within_maximum(&broad, &middle, options()), CheckResult::Within(_) @@ -2282,4 +2343,94 @@ mod tests { ); } } + + #[test] + fn filesystem_comparisons_do_not_assume_path_ancestry_or_distinctness() { + for access in ["read_only", "read_write"] { + let maximum = parse(&format!( + "version: 1\nfilesystem_policy: {{ {access}: [/safe] }}\n" + )); + for path in [ + "/safe/link", + "/safe/child/file", + "/elsewhere", + "/safe-prefix", + ] { + let candidate = parse(&format!( + "version: 1\nfilesystem_policy: {{ {access}: [{path}] }}\n" + )); + assert!( + matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedFilesystemPath + ), + "access={access} path={path}" + ); + } + let matching = parse(&format!( + "version: 1\nfilesystem_policy: {{ {access}: [/safe, /safe] }}\n" + )); + assert!(matches!( + check_within_maximum(&maximum, &matching, options()), + CheckResult::Within(_) + )); + let root = parse(&format!( + "version: 1\nfilesystem_policy: {{ {access}: [/] }}\n" + )); + assert!(matches!( + check_within_maximum(&root, &maximum, options()), + CheckResult::Within(_) + )); + } + } + + #[test] + fn path_globs_match_the_runtime_builtin() { + let mut runtime = regorus::Engine::new(); + for pattern in [ + "/a/**/b", + "/**/b", + "/a/**/**/b", + "/a/**", + "/a/**/**", + "/a/**/", + "/a/*/b", + "/a/x**/b", + "/a/**x/b", + "/a/***/b", + "/a/**/x*/**/b", + ] { + for path in [ + "/a/b", + "/a/x/b", + "/a/x/y/b", + "/b", + "/a/", + "/a", + "/a/xb", + "/a/x/z/xb/y/b", + "/a/c", + ] { + let query = format!( + "glob.match({}, [\"/\"], {})", + serde_json::to_string(pattern).unwrap(), + serde_json::to_string(path).unwrap() + ); + let actual = runtime.eval_query(query, false).unwrap(); + let expected = actual.result[0].expressions[0].value == regorus::Value::from(true); + let solver = Solver::new(); + solver.assert( + Z3String::from_str(path) + .unwrap() + .regex_matches(&glob_regex(pattern, "/")), + ); + assert_eq!( + solver.check() == SatResult::Sat, + expected, + "pattern={pattern} path={path}" + ); + } + } + } } diff --git a/crates/openshell-prover/tests/runtime_parity.rs b/crates/openshell-prover/tests/runtime_parity.rs index 8abc3514c7..bd90156999 100644 --- a/crates/openshell-prover/tests/runtime_parity.rs +++ b/crates/openshell-prover/tests/runtime_parity.rs @@ -83,6 +83,68 @@ fn eval_array_len(engine: &mut Engine, input: &Value, rule: &str) -> usize { } } +#[test] +fn recursive_path_globs_preserve_zero_directory_grants_and_denies() { + let policy = |grant: &str, deny: Option<&str>, endpoint: &str| { + json!({ + "version": 1, + "network_policies": {"n": { + "binaries": [{"path": "/usr/bin/curl"}], + "endpoints": [{ + "host": "api.example.com", "ports": [443], + "protocol": "rest", "enforcement": "enforce", "path": endpoint, + "rules": [{"allow": {"method": "GET", "path": grant}}], + "deny_rules": deny.into_iter().map(|path| json!({"method": "GET", "path": path})).collect::>() + }] + }} + }).to_string() + }; + for (maximum, candidate, within) in [ + ( + policy("/**", Some("/a/**/b"), ""), + policy("/a/b", None, ""), + false, + ), + ( + policy("/a/**/b", Some("/a/b"), ""), + policy("/a/**/b", None, ""), + false, + ), + (policy("/a/**/b", None, ""), policy("/a/b", None, ""), true), + ( + policy("/**", None, "/a/**/b"), + policy("/a/b", None, ""), + true, + ), + ] { + let input: Value = serde_json::from_value(json!({ + "exec": {"path": "/usr/bin/curl", "ancestors": [], "cmdline_paths": []}, + "network": {"host": "api.example.com", "port": 443}, + "request": {"method": "GET", "path": "/a/b", "query_params": {}} + })) + .unwrap(); + assert!(eval_bool( + &mut runtime_engine(&candidate), + &input, + "data.openshell.sandbox.allow_request" + )); + assert_eq!( + eval_bool( + &mut runtime_engine(&maximum), + &input, + "data.openshell.sandbox.allow_request" + ), + within + ); + let result = check(&maximum, &candidate); + if within { + assert!(matches!(result, CheckResult::Within(_)), "{result:?}"); + } else { + assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); + } + } +} + #[test] fn intra_label_host_wildcard_matches_empty_suffix_at_runtime() { let maximum = r#" diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx index 8b5351aec6..bf69ac1d95 100644 --- a/docs/reference/policy-prover.mdx +++ b/docs/reference/policy-prover.mdx @@ -72,9 +72,9 @@ Create the fully composed candidate policy: version: 1 filesystem_policy: read_only: - - /usr/bin + - /usr read_write: - - /tmp/cache + - /tmp ``` Run the check: @@ -155,7 +155,16 @@ state. In particular: the configuration and identities that expose the additional authority. - REST containment witnesses use canonical request methods and paths. - Both files are interpreted in the same sandbox filesystem namespace and - mount model. The CLI does not resolve sandbox paths against the host. + mount model, with stable path resolution when enforcement rules are created. + The CLI does not resolve sandbox paths against the host. +- Filesystem containment supports removing grants and reducing write grants to + read-only grants at matching paths. A maximum grant for `/` also covers other + paths for the same access. Comparisons between different paths otherwise + return `unsupported` with `reason_code: unresolved_filesystem_path`: a lexical + child can resolve outside its parent through a symlink, and unrelated paths + can resolve to the same object. This includes narrowing `/tmp` to `/tmp/cache`. + If the maximum grants no access of the requested kind, adding that access + returns `exceeds_max`. Use the [Policy Schema Reference](/reference/policy-schema) for the full policy language. A successful prover result covers only the scope reported in its From 51c3e0feb50de11914b8a86c397914f2e9b04aeb Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 22:33:11 +0000 Subject: [PATCH 04/12] fix(prover): stabilize containment checks in CI Signed-off-by: Johnny Greco --- crates/openshell-prover/src/containment.rs | 308 +++++++++++++-------- 1 file changed, 197 insertions(+), 111 deletions(-) diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index c9afc4c12f..c78a0a27fb 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -631,28 +631,12 @@ fn check_within_maximum_inner( } NetworkSolve::Incomplete(result) => return result, } - let ambiguous_binary_paths = ambiguous_candidate_binary_paths(maximum, candidate); - if binary_identity_required && !ambiguous_binary_paths.is_empty() { - let exact_maximum = - maximum_without_ambiguous_binary_globs(maximum, candidate, &ambiguous_binary_paths); - match solve_network_mode( - &exact_maximum, - candidate, - true, - started, - options.timeout, - cancelled, - ) { - NetworkSolve::Within => {} - NetworkSolve::Exceeds(_) => { - return unsupported( - ReasonCode::UnresolvedBinaryPath, - "network containment depends on image-specific binary symlink resolution" - .to_owned(), - ); - } - NetworkSolve::Incomplete(result) => return result, - } + if binary_identity_required && has_ambiguous_candidate_binary_path(maximum, candidate) { + return unsupported( + ReasonCode::UnresolvedBinaryPath, + "network containment depends on image-specific binary symlink resolution" + .to_owned(), + ); } } if unresolved_exact_deny_symlink(maximum, candidate) { @@ -673,6 +657,9 @@ fn solve_network_mode( timeout: Duration, cancelled: Option<&AtomicBool>, ) -> NetworkSolve { + if network_is_structurally_contained(maximum, candidate, binary_identity_required) { + return NetworkSolve::Within; + } let solver = Solver::new(); let action = symbolic_action(if binary_identity_required { "strict_maximum_policy_action" @@ -774,6 +761,100 @@ fn unsupported(code: ReasonCode, reason: String) -> CheckResult { CheckResult::Unsupported(ReasonEvidence { code, reason }) } +/// Prove straightforward REST containment without invoking the solver. This +/// covers the common case where selectors are identical and the candidate only +/// narrows explicit method/path grants. More complex unions still use Z3. +fn network_is_structurally_contained( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + binary_identity_required: bool, +) -> bool { + if maximum + .network_policies + .values() + .flat_map(|rule| &rule.endpoints) + .any(|endpoint| !endpoint.deny_rules.is_empty()) + { + return false; + } + candidate.network_policies.values().all(|candidate_rule| { + maximum.network_policies.values().any(|maximum_rule| { + rule_structurally_contains(maximum_rule, candidate_rule, binary_identity_required) + }) + }) +} + +fn rule_structurally_contains( + maximum: &NetworkRule, + candidate: &NetworkRule, + binary_identity_required: bool, +) -> bool { + (!binary_identity_required + || candidate.binaries.iter().all(|candidate_binary| { + maximum + .binaries + .iter() + .any(|maximum_binary| maximum_binary.path == candidate_binary.path) + })) + && candidate.endpoints.iter().all(|candidate_endpoint| { + maximum.endpoints.iter().any(|maximum_endpoint| { + rest_endpoint_structurally_contains(maximum_endpoint, candidate_endpoint) + }) + }) +} + +fn rest_endpoint_structurally_contains(maximum: &Endpoint, candidate: &Endpoint) -> bool { + if maximum.protocol_kind() != Protocol::Rest + || candidate.protocol_kind() != Protocol::Rest + || !maximum.host.eq_ignore_ascii_case(&candidate.host) + || maximum.path != candidate.path + || !candidate + .effective_ports() + .iter() + .all(|port| maximum.effective_ports().contains(port)) + || !maximum.access.is_empty() + || !candidate.access.is_empty() + || !maximum.deny_rules.is_empty() + || !candidate.deny_rules.is_empty() + { + return false; + } + + candidate.rules.iter().all(|candidate_rule| { + if candidate_rule.allow.method.is_empty() { + return false; + } + maximum.rules.iter().any(|maximum_rule| { + method_pattern_contains(&maximum_rule.allow.method, &candidate_rule.allow.method) + && path_pattern_contains(&maximum_rule.allow.path, &candidate_rule.allow.path) + }) + }) +} + +fn method_pattern_contains(maximum: &str, candidate: &str) -> bool { + maximum == "*" + || maximum.eq_ignore_ascii_case(candidate) + || (maximum.eq_ignore_ascii_case("GET") && candidate.eq_ignore_ascii_case("HEAD")) +} + +fn path_pattern_contains(maximum: &str, candidate: &str) -> bool { + // Inputs are already validated. Keep this sufficient proof deliberately + // limited to equality and a terminal recursive path segment. + let maximum = if maximum.is_empty() { "**" } else { maximum }; + let candidate = if candidate.is_empty() { + "**" + } else { + candidate + }; + maximum == candidate + || maximum == "**" + || maximum.strip_suffix("/**").is_some_and(|prefix| { + candidate + .strip_prefix(prefix) + .is_some_and(|suffix| suffix.starts_with('/')) + }) +} + fn symbolic_action(name: &str) -> SymbolicAction { let _context = Context::thread_local(); SymbolicAction { @@ -1186,69 +1267,37 @@ fn unresolved_workdir_reason( None } -fn ambiguous_candidate_binary_paths( +fn has_ambiguous_candidate_binary_path( maximum: &ContainmentPolicy, candidate: &ContainmentPolicy, -) -> Vec { - let maximum_binaries = maximum - .network_policies - .values() - .flat_map(|rule| &rule.binaries) - .map(|binary| binary.path.as_str()) - .collect::>(); - candidate - .network_policies - .values() - .flat_map(|rule| &rule.binaries) - .map(|binary| binary.path.as_str()) - .filter(|path| !path.contains('*')) - .filter(|path| { - maximum_binaries.iter().any(|maximum| { - maximum.contains('*') - && *maximum != "/**" - && glob::Pattern::new(maximum).is_ok_and(|pattern| pattern.matches(path)) - }) - }) - .map(str::to_owned) - .collect() -} - -fn maximum_without_ambiguous_binary_globs( - maximum: &ContainmentPolicy, - candidate: &ContainmentPolicy, - ambiguous_candidate_paths: &[String], -) -> ContainmentPolicy { - let mut exact_maximum = maximum.clone(); - for rule in exact_maximum.network_policies.values_mut() { - let endpoints = rule.endpoints.clone(); - rule.binaries.retain(|binary| { - let shared_by_equivalent_rule = - candidate.network_policies.values().any(|candidate_rule| { - endpoint_authority_sets_equal(&candidate_rule.endpoints, &endpoints) - && candidate_rule - .binaries - .iter() - .any(|candidate_binary| candidate_binary.path == binary.path) - }); - let authorizes_ambiguous_exact = +) -> bool { + maximum.network_policies.values().any(|maximum_rule| { + maximum_rule + .binaries + .iter() + .filter(|binary| binary.path.contains('*') && binary.path != "/**") + .any(|maximum_binary| { candidate.network_policies.values().any(|candidate_rule| { - endpoint_authority_sets_overlap(&candidate_rule.endpoints, &endpoints) - && candidate_rule.binaries.iter().any(|candidate_binary| { - !candidate_binary.path.contains('*') - && ambiguous_candidate_paths.contains(&candidate_binary.path) - && glob::Pattern::new(&binary.path) - .is_ok_and(|pattern| pattern.matches(&candidate_binary.path)) - }) - }); - !binary.path.contains('*') - || binary.path == "/**" - || (shared_by_equivalent_rule && !authorizes_ambiguous_exact) - || !ambiguous_candidate_paths.iter().any(|candidate| { - glob::Pattern::new(&binary.path).is_ok_and(|pattern| pattern.matches(candidate)) + endpoint_authority_sets_overlap( + &candidate_rule.endpoints, + &maximum_rule.endpoints, + ) && candidate_rule.binaries.iter().any(|candidate_binary| { + !candidate_binary.path.contains('*') + && glob::Pattern::new(&maximum_binary.path) + .is_ok_and(|pattern| pattern.matches(&candidate_binary.path)) + && !maximum.network_policies.values().any(|exact_rule| { + endpoint_authority_sets_equal( + &candidate_rule.endpoints, + &exact_rule.endpoints, + ) && exact_rule + .binaries + .iter() + .any(|exact_binary| exact_binary.path == candidate_binary.path) + }) + }) }) - }); - } - exact_maximum + }) + }) } fn unresolved_exact_deny_symlink( @@ -1291,6 +1340,14 @@ fn unresolved_exact_deny_symlink( }) } +fn endpoint_authority_sets_overlap(left: &[Endpoint], right: &[Endpoint]) -> bool { + left.iter().any(|endpoint| { + right + .iter() + .any(|other| endpoint_authority_may_overlap(endpoint, other)) + }) +} + fn endpoint_authority_sets_equal(left: &[Endpoint], right: &[Endpoint]) -> bool { left.iter().all(|endpoint| { right @@ -1302,14 +1359,6 @@ fn endpoint_authority_sets_equal(left: &[Endpoint], right: &[Endpoint]) -> bool }) } -fn endpoint_authority_sets_overlap(left: &[Endpoint], right: &[Endpoint]) -> bool { - left.iter().any(|endpoint| { - right - .iter() - .any(|other| endpoint_authority_may_overlap(endpoint, other)) - }) -} - fn endpoint_authority_may_overlap(left: &Endpoint, right: &Endpoint) -> bool { let ports_overlap = left .effective_ports() @@ -1954,19 +2003,23 @@ mod tests { "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: read-only }\n binaries: [{ path: /usr/bin/curl }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: read-only\n deny_rules: [{ method: '*', path: '/**' }]\n binaries: [{ path: /usr/bin/node }]\n", ); let result = check_within_maximum(&maximum, &candidate, options()); - assert!(matches!( - result, - CheckResult::Exceeds(ref evidence) - if matches!( - evidence.counterexample(), - Counterexample::Network { - binary: Some(binary), - ancestor_binary: Some(ancestor), - binary_identity_required: true, - .. - } if binary == "/usr/bin/curl" && ancestor == "/usr/bin/python3" - ) - )); + assert!( + matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { + binary: Some(binary), + ancestor_binary: Some(ancestor), + binary_identity_required: true, + .. + } if (binary == "/usr/bin/curl" && ancestor == "/usr/bin/python3") + || (binary == "/usr/bin/python3" && ancestor == "/usr/bin/curl") + ) + ), + "{result:?}" + ); } #[test] @@ -2044,14 +2097,31 @@ mod tests { let broader_method = parse( "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: POST, path: '/repos/NVIDIA/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", ); - assert!(matches!( - check_within_maximum(&maximum, &narrower, options()), - CheckResult::Within(_) - )); + let result = check_within_maximum(&maximum, &narrower, options()); + assert!(matches!(result, CheckResult::Within(_)), "{result:?}"); let result = check_within_maximum(&maximum, &broader_method, options()); assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); } + #[test] + fn structural_path_containment_requires_a_recursive_segment_boundary() { + assert!(path_pattern_contains("/repos/**", "/repos/NVIDIA/**")); + assert!(!path_pattern_contains("/repos/**", "/repository/NVIDIA/**")); + assert!(!path_pattern_contains("/repos**", "/repos/NVIDIA/**")); + } + + #[test] + fn structural_fast_path_does_not_ignore_separate_maximum_denies() { + let maximum = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, rules: [{ allow: { method: GET, path: '/repos/**' } }] }\n binaries: [{ path: /usr/bin/curl }]\n deny:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, access: full, deny_rules: [{ method: GET, path: '/repos/private/**' }] }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, rules: [{ allow: { method: GET, path: '/repos/private/**' } }] }\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); + } + #[test] fn unknown_and_environment_dependent_shapes_fail_closed() { let unknown = parse("version: 1\nfuture_authority: true\n"); @@ -2082,11 +2152,15 @@ mod tests { let candidate = parse( "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/python3 }]\n", ); - assert!(matches!( - check_within_maximum(&maximum, &candidate, options()), - CheckResult::Unsupported(ref evidence) - if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath - )); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + ), + "{result:?}" + ); } #[test] @@ -2103,6 +2177,18 @@ mod tests { )); } + #[test] + fn redundant_maximum_glob_does_not_hide_equivalent_exact_containment() { + let maximum = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n glob:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!(matches!(result, CheckResult::Within(_)), "{result:?}"); + } + #[test] fn unrelated_universal_glob_does_not_hide_symlink_ambiguity() { let maximum = parse( From 72cf7cf7f917e72a04e93d835b6fd058cd080ddd Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 22:49:06 +0000 Subject: [PATCH 05/12] test(prover): avoid solver in fast-path guard test Signed-off-by: Johnny Greco --- crates/openshell-prover/src/containment.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index c78a0a27fb..d9cf376069 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -2118,8 +2118,9 @@ mod tests { let candidate = parse( "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, rules: [{ allow: { method: GET, path: '/repos/private/**' } }] }\n binaries: [{ path: /usr/bin/curl }]\n", ); - let result = check_within_maximum(&maximum, &candidate, options()); - assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); + assert!(!network_is_structurally_contained( + &maximum, &candidate, true + )); } #[test] From ccb88dce9d9ab7b530ad2088e657b46596dee717 Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 23:33:28 +0000 Subject: [PATCH 06/12] fix(prover): align string containment with runtime Signed-off-by: Johnny Greco --- .../workflows/package-release-binaries.yml | 24 ++ architecture/security-policy.md | 12 +- crates/openshell-prover-cli/tests/cli.rs | 62 +++ .../fixtures/candidate-underscore-host.yaml | 11 + .../candidate-unicode-network-selector.yaml | 11 + .../tests/fixtures/maximum-empty.yaml | 4 + crates/openshell-prover/README.md | 9 + crates/openshell-prover/src/containment.rs | 369 ++++++++++++++++-- .../openshell-prover/tests/runtime_parity.rs | 123 +++++- docs/reference/policy-prover.mdx | 12 + 10 files changed, 601 insertions(+), 36 deletions(-) create mode 100644 crates/openshell-prover-cli/tests/fixtures/candidate-underscore-host.yaml create mode 100644 crates/openshell-prover-cli/tests/fixtures/candidate-unicode-network-selector.yaml create mode 100644 crates/openshell-prover-cli/tests/fixtures/maximum-empty.yaml diff --git a/.github/workflows/package-release-binaries.yml b/.github/workflows/package-release-binaries.yml index fc791f9f48..4b7007e4c2 100644 --- a/.github/workflows/package-release-binaries.yml +++ b/.github/workflows/package-release-binaries.yml @@ -143,6 +143,30 @@ jobs: --output json > result.json grep -q '"result"[[:space:]]*:[[:space:]]*"within_max"' result.json + if extracted/openshell-prover check \ + crates/openshell-prover-cli/tests/fixtures/candidate-underscore-host.yaml \ + --maximum crates/openshell-prover-cli/tests/fixtures/maximum-empty.yaml \ + --output json > underscore.json; then + echo "ERROR: underscore host unexpectedly stayed within an empty maximum" >&2 + exit 1 + else + test "$?" = 1 + fi + grep -q '"result"[[:space:]]*:[[:space:]]*"exceeds_max"' underscore.json + grep -q '"host"[[:space:]]*:[[:space:]]*"api_internal.example.com"' underscore.json + + if extracted/openshell-prover check \ + crates/openshell-prover-cli/tests/fixtures/candidate-unicode-network-selector.yaml \ + --maximum crates/openshell-prover-cli/tests/fixtures/maximum-empty.yaml \ + --output json > unicode.json; then + echo "ERROR: non-ASCII network selector unexpectedly produced a definitive result" >&2 + exit 1 + else + test "$?" = 3 + fi + grep -q '"result"[[:space:]]*:[[:space:]]*"unsupported"' unicode.json + grep -q '"reason_code"[[:space:]]*:[[:space:]]*"unsupported_policy_shape"' unicode.json + prover-checksums: name: Package prover checksums needs: smoke-prover diff --git a/architecture/security-policy.md b/architecture/security-policy.md index 1b810372fc..3e67801397 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -348,8 +348,13 @@ authority, and enforced REST method and path authority, including explicit REST denies. Network containment covers runtime configurations both with and without binary identity enforcement. Strict checks match grants and denies against the executable and an ancestor identity, and the evidence identifies the identities -for an exceeding witness. Recognized authority outside the reviewed model -produces an unsupported result rather than being silently ignored. +for an exceeding witness. Network binary selectors, endpoint host and path +selectors, and REST allow and deny method and path selectors must use ASCII +literals. This restriction applies to both inputs, including deny-only rules; +other Unicode policy text and filesystem paths are unaffected. ASCII wildcard +selectors still cover non-ASCII runtime values matched by the policy engine. +Recognized authority outside the reviewed model produces an unsupported result +rather than being silently ignored. Environment-dependent authority also remains unsupported when the result depends on context that is unavailable to the local command. This includes an unresolved workdir, filesystem or binary containment that depends on image-specific @@ -362,6 +367,9 @@ are created. They support matching paths, grant removal, write-to-read reduction and a maximum root grant. Other comparisons between paths remain unsupported; lexical ancestry or distinctness alone cannot establish resolved ancestry or distinctness. Adding access when the maximum grants none produces a counterexample. +If the solver produces a string that cannot be decoded and checked faithfully, +the command returns an inconclusive `invalid_witness` result instead of publishing +the value as counterexample evidence. This containment operation is separate from the proposal-risk queries below. See the [standalone policy prover documentation](../docs/reference/policy-prover.mdx) diff --git a/crates/openshell-prover-cli/tests/cli.rs b/crates/openshell-prover-cli/tests/cli.rs index 0e74311bdf..7d776f2d83 100644 --- a/crates/openshell-prover-cli/tests/cli.rs +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -119,6 +119,68 @@ fn unsupported_policy_returns_reason_and_three() { assert!(value["reason"].is_string()); } +#[test] +fn underscore_host_exceeds_an_empty_maximum() { + let output = check_json("candidate-underscore-host.yaml", "maximum-empty.yaml"); + assert_eq!( + output.status.code(), + Some(1), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "exceeds_max"); + assert_eq!(value["counterexample"]["host"], "api_internal.example.com"); +} + +#[test] +fn non_ascii_network_literals_are_unsupported_in_both_inputs() { + for (candidate, maximum, input_label) in [ + ( + "candidate-unicode-network-selector.yaml", + "maximum-empty.yaml", + "candidate", + ), + ( + "maximum-empty.yaml", + "candidate-unicode-network-selector.yaml", + "maximum", + ), + ] { + let output = check_json(candidate, maximum); + assert_eq!( + output.status.code(), + Some(3), + "{input_label} stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "unsupported"); + assert_eq!(value["reason_code"], "unsupported_policy_shape"); + assert!( + value["reason"] + .as_str() + .is_some_and(|reason| reason.contains(input_label) && reason.contains("non-ASCII")), + "{value}" + ); + } + + let output = run(&[ + "check", + fixture("candidate-unicode-network-selector.yaml") + .to_str() + .unwrap(), + "--maximum", + fixture("maximum-empty.yaml").to_str().unwrap(), + ]); + assert_eq!(output.status.code(), Some(3)); + assert!(output.stderr.is_empty()); + let text = String::from_utf8(output.stdout).expect("UTF-8 text output"); + assert!(text.contains("result: unsupported"), "{text}"); + assert!(text.contains("candidate policy"), "{text}"); + assert!(text.contains("non-ASCII"), "{text}"); +} + #[test] fn resource_exhaustion_is_inconclusive_and_returns_three() { let path = std::env::temp_dir().join(format!( diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-underscore-host.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-underscore-host.yaml new file mode 100644 index 0000000000..d2f2d37a84 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-underscore-host.yaml @@ -0,0 +1,11 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +network_policies: + underscore-host: + endpoints: + - host: api_internal.example.com + port: 443 + binaries: + - path: /usr/bin/curl diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-unicode-network-selector.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-unicode-network-selector.yaml new file mode 100644 index 0000000000..bba84da6e9 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-unicode-network-selector.yaml @@ -0,0 +1,11 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +network_policies: + unicode-binary: + endpoints: + - host: api.example.com + port: 443 + binaries: + - path: /usr/bin/é* diff --git a/crates/openshell-prover-cli/tests/fixtures/maximum-empty.yaml b/crates/openshell-prover-cli/tests/fixtures/maximum-empty.yaml new file mode 100644 index 0000000000..458bab0e43 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/maximum-empty.yaml @@ -0,0 +1,4 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index f13578b94a..65a38bd765 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -14,6 +14,15 @@ fully composed candidate policy stays within an operator-supplied maximum. The 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. 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 diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index d9cf376069..d64118baad 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -16,7 +16,7 @@ use std::time::{Duration, Instant}; use serde::Deserialize; use serde_yml::Value; -use z3::ast::{Bool, Int, Regexp, String as Z3String}; +use z3::ast::{Ast, Bool, Int, Regexp, String as Z3String}; use z3::{Context, Params, SatResult, Solver}; const READ_ONLY_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS"]; @@ -707,6 +707,9 @@ fn solve_network_mode( SatResult::Sat => solver .get_model() .and_then(|model| counterexample_from_model(&model, &action, binary_identity_required)) + .filter(|counterexample| { + counterexample_satisfies_predicate(maximum, candidate, counterexample) + }) .map_or_else( || { NetworkSolve::Incomplete(CheckResult::Inconclusive(ReasonEvidence { @@ -1065,9 +1068,9 @@ fn counterexample_from_model( binary_identity_required: bool, ) -> Option { let port = model.eval(&action.port, true)?.as_u64()?; - let layer = model.eval(&action.layer, true)?.as_string()?; + let layer = model_string_exact(model, &action.layer)?; let binary = if binary_identity_required { - let binary = model.eval(&action.binary, true)?.as_string()?; + let binary = model_string_exact(model, &action.binary)?; if !is_canonical_runtime_binary_path(&binary) { return None; } @@ -1076,7 +1079,7 @@ fn counterexample_from_model( None }; let ancestor_binary = if binary_identity_required { - let binary = model.eval(&action.ancestor_binary, true)?.as_string()?; + let binary = model_string_exact(model, &action.ancestor_binary)?; if !is_canonical_runtime_binary_path(&binary) { return None; } @@ -1084,7 +1087,7 @@ fn counterexample_from_model( } else { None }; - let host = model.eval(&action.host, true)?.as_string()?; + let host = model_string_exact(model, &action.host)?; if !is_canonical_dns_host(&host) { return None; } @@ -1094,8 +1097,8 @@ fn counterexample_from_model( Protocol::Rest }; let (method, path) = if protocol == Protocol::Rest { - let method = model.eval(&action.method, true)?.as_string()?; - let path = model.eval(&action.path, true)?.as_string()?; + let method = model_string_exact(model, &action.method)?; + let path = model_string_exact(model, &action.path)?; if !is_http_method(&method) || !is_canonical_rest_path(&path) { return None; } @@ -1115,6 +1118,52 @@ fn counterexample_from_model( }) } +/// Decode a model string only when encoding it again produces the exact same +/// solver value. `as_string` uses a lossy C-string boundary in the Rust Z3 +/// binding, so accepting its output alone could publish an altered witness. +fn model_string_exact(model: &z3::Model, value: &Z3String) -> Option { + let evaluated = model.eval(value, true)?; + let decoded = evaluated.as_string()?; + let reconstructed = Z3String::from_str(&decoded).ok()?; + (evaluated.eq(reconstructed).simplify().as_bool() == Some(true)).then_some(decoded) +} + +fn counterexample_satisfies_predicate( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + counterexample: &Counterexample, +) -> bool { + let Counterexample::Network { + binary, + ancestor_binary, + binary_identity_required, + host, + port, + protocol, + method, + path, + } = counterexample + else { + return false; + }; + let concrete = SymbolicAction { + binary: Z3String::from_str(binary.as_deref().unwrap_or("")).unwrap(), + ancestor_binary: Z3String::from_str(ancestor_binary.as_deref().unwrap_or("")).unwrap(), + host: Z3String::from_str(host).unwrap(), + port: Int::from_u64(u64::from(*port)), + layer: Z3String::from_str(protocol.as_str()).unwrap(), + method: Z3String::from_str(method.as_deref().unwrap_or("GET")).unwrap(), + path: Z3String::from_str(path.as_deref().unwrap_or("/")).unwrap(), + }; + Bool::and(&[ + policy_allows(candidate, &concrete, *binary_identity_required), + !policy_allows(maximum, &concrete, *binary_identity_required), + ]) + .simplify() + .as_bool() + == Some(true) +} + fn is_canonical_runtime_binary_path(path: &str) -> bool { path.len() <= 4 * 1024 && is_canonical_pattern_path(path) && !path.chars().any(char::is_control) } @@ -1125,17 +1174,13 @@ fn is_canonical_dns_host(host: &str) -> bool { && host.split('.').all(|label| { !label.is_empty() && label.len() <= 63 - && label - .bytes() - .all(|byte| byte.is_ascii_lowercase() || byte.is_ascii_digit() || byte == b'-') - && label - .as_bytes() - .first() - .is_some_and(u8::is_ascii_alphanumeric) - && label - .as_bytes() - .last() - .is_some_and(u8::is_ascii_alphanumeric) + && label.bytes().all(|byte| { + byte.is_ascii_lowercase() + || byte.is_ascii_digit() + || matches!(byte, b'-' | b'_') + }) + && label.as_bytes().first().is_some_and(|byte| *byte != b'-') + && label.as_bytes().last().is_some_and(|byte| *byte != b'-') }) } @@ -1494,6 +1539,11 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason return unsupported(format!("rule '{rule_name}' uses unsupported fields")); } for binary in &rule.binaries { + if !binary.path.is_ascii() { + return unsupported(format!( + "rule '{rule_name}' binary path contains a non-ASCII literal" + )); + } if binary.path.is_empty() || !is_canonical_pattern_path(&binary.path) || !binary.extra.is_empty() @@ -1504,14 +1554,28 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason } for endpoint in &rule.endpoints { let context = format!("rule '{rule_name}'"); + if !endpoint.host.is_ascii() { + return unsupported(format!( + "{context} endpoint host contains a non-ASCII literal" + )); + } + if !endpoint.path.is_ascii() { + return unsupported(format!( + "{context} endpoint path contains a non-ASCII literal" + )); + } if endpoint.host.is_empty() || endpoint.effective_ports().is_empty() || (endpoint.port != 0 && !endpoint.ports.is_empty()) { return unsupported(format!("{context} has no unambiguous host and port")); } - if unsupported_host_glob(&endpoint.host) - || unsupported_glob(&endpoint.path) + if unsupported_host_glob(&endpoint.host) { + return unsupported(format!( + "{context} endpoint host uses an unsupported pattern" + )); + } + if unsupported_glob(&endpoint.path) || (!endpoint.path.is_empty() && !is_canonical_pattern_path(&endpoint.path)) { return unsupported(format!("{context} uses an unsupported glob")); @@ -1581,11 +1645,31 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason return unsupported(format!("{context} mixes REST controls into L4 authority")); } for rule in &endpoint.rules { + if !rule.allow.method.is_ascii() { + return unsupported(format!( + "{context} REST allow method contains a non-ASCII literal" + )); + } + if !rule.allow.path.is_ascii() { + return unsupported(format!( + "{context} REST allow path contains a non-ASCII literal" + )); + } if !rule.extra.is_empty() || unsupported_allow(&rule.allow) { return unsupported(format!("{context} uses an unsupported REST allow rule")); } } for rule in &endpoint.deny_rules { + if !rule.method.is_ascii() { + return unsupported(format!( + "{context} REST deny method contains a non-ASCII literal" + )); + } + if !rule.path.is_ascii() { + return unsupported(format!( + "{context} REST deny path contains a non-ASCII literal" + )); + } if unsupported_deny(rule) { return unsupported(format!("{context} uses an unsupported REST deny rule")); } @@ -1746,10 +1830,26 @@ fn unsupported_host_glob(pattern: &str) -> bool { { return true; } - pattern.split('.').enumerate().any(|(index, label)| { - (label.contains("**") && label != "**") - || (index > 0 && label.contains('*') && label != "*" && label != "**") - }) + let labels = pattern.split('.').collect::>(); + let minimum_name_len = labels + .iter() + .map(|label| label.bytes().filter(|byte| *byte != b'*').count().max(1)) + .sum::() + + labels.len().saturating_sub(1); + minimum_name_len > 253 + || labels.iter().enumerate().any(|(index, label)| { + let first = label.as_bytes().first().copied(); + let last = label.as_bytes().last().copied(); + let minimum_label_len = label.bytes().filter(|byte| *byte != b'*').count().max(1); + minimum_label_len > 63 + || !label + .bytes() + .all(|byte| byte.is_ascii_alphanumeric() || matches!(byte, b'-' | b'_' | b'*')) + || first == Some(b'-') + || last == Some(b'-') + || (label.contains("**") && *label != "**") + || (index > 0 && label.contains('*') && *label != "*" && *label != "**") + }) } fn bool_or(values: impl IntoIterator) -> Bool { @@ -1850,19 +1950,31 @@ fn path_glob_regex(pattern: &str) -> Regexp { } fn non_separator_regex(separator: &str) -> Regexp { - match separator { - "/" => Regexp::union(&[&Regexp::range(&' ', &'.'), &Regexp::range(&'0', &'~')]), - "." => Regexp::union(&[&Regexp::range(&' ', &'-'), &Regexp::range(&'/', &'~')]), - _ => Regexp::full(), - } + // Runtime globs match Unicode values. Describe a non-empty separator-free + // sequence from Z3's full string language instead of limiting wildcards to + // character ranges. This works with both supported Z3 versions; callers' + // `star` and `plus` operations preserve the runtime wildcard languages. + let contains_separator = Regexp::concat(&[ + &Regexp::full(), + &Regexp::literal(separator), + &Regexp::full(), + ]); + Regexp::intersect(&[ + &contains_separator.complement(), + &Regexp::literal("").complement(), + ]) } fn host_domain_regex() -> Regexp { let alphanumeric = Regexp::union(&[&Regexp::range(&'a', &'z'), &Regexp::range(&'0', &'9')]); - let label_character = Regexp::union(&[&alphanumeric, &Regexp::literal("-")]); + // Actions represent canonical resolver inputs, not every raw value the + // proxy parser or Rego glob builtin can compare. Supported endpoint globs + // are therefore modeled over this same resolver-oriented host domain. + let label_edge = Regexp::union(&[&alphanumeric, &Regexp::literal("_")]); + let label_character = Regexp::union(&[&label_edge, &Regexp::literal("-")]); let label = Regexp::union(&[ - &alphanumeric, - &Regexp::concat(&[&alphanumeric, &label_character.star(), &alphanumeric]), + &label_edge, + &Regexp::concat(&[&label_edge, &label_character.r#loop(0, 61), &label_edge]), ]); Regexp::concat(&[ &label, @@ -1941,6 +2053,113 @@ mod tests { )); } + #[test] + fn underscore_hosts_are_present_in_the_full_action_domain() { + let cases = [ + ("api_internal.example.com", ""), + ("_service.example.com", "tcp"), + ("a_b.test", "rest"), + ]; + + for (host, protocol) in cases { + let endpoint = if protocol == "rest" { + format!( + "{{ host: {host}, port: 443, protocol: rest, enforcement: enforce, access: read-only }}" + ) + } else if protocol == "tcp" { + format!("{{ host: {host}, port: 443, protocol: tcp }}") + } else { + format!("{{ host: {host}, port: 443 }}") + }; + let candidate = parse(&format!( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{endpoint}]\n binaries: []\n" + )); + let result = check_within_maximum(&parse("version: 1\n"), &candidate, options()); + assert!( + matches!( + result, + CheckResult::Exceeds(ref evidence) + if matches!( + evidence.counterexample(), + Counterexample::Network { host: witness, .. } if witness == host + ) + ), + "protocol={protocol:?} host={host}: {result:?}" + ); + } + } + + #[test] + fn underscore_hosts_preserve_exact_and_wildcard_containment() { + let maximum = parse( + "version: 1\nnetwork_policies:\n maximum:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: []\n", + ); + let candidate = parse( + "version: 1\nnetwork_policies:\n candidate:\n endpoints: [{ host: api_internal.example.com, port: 443 }]\n binaries: []\n", + ); + assert!(matches!( + check_within_maximum(&maximum, &candidate, options()), + CheckResult::Within(_) + )); + + let exact_maximum = parse( + "version: 1\nnetwork_policies:\n maximum:\n endpoints: [{ host: _service.example.com, port: 443, protocol: tcp }]\n binaries: []\n", + ); + let exact_candidate = parse( + "version: 1\nnetwork_policies:\n candidate:\n endpoints: [{ host: _service.example.com, port: 443, protocol: tcp }]\n binaries: []\n", + ); + assert!(matches!( + check_within_maximum(&exact_maximum, &exact_candidate, options()), + CheckResult::Within(_) + )); + } + + #[test] + fn host_domain_enforces_modeled_label_and_name_boundaries() { + let maximum_length = format!( + "{}.{}.{}.{}", + "a".repeat(63), + "b".repeat(63), + "c".repeat(63), + "d".repeat(61) + ); + assert_eq!(maximum_length.len(), 253); + assert!(is_canonical_dns_host(&maximum_length)); + assert!(!unsupported_host_glob(&maximum_length)); + assert!(is_canonical_dns_host("_service.example.com")); + assert!(is_canonical_dns_host("api-internal.example.com")); + + let oversized_label = format!("{}.example.com", "a".repeat(64)); + assert!(!is_canonical_dns_host(&oversized_label)); + assert!(unsupported_host_glob(&oversized_label)); + + let oversized_name = format!( + "{}.{}.{}.{}", + "a".repeat(63), + "b".repeat(63), + "c".repeat(63), + "d".repeat(62) + ); + assert_eq!(oversized_name.len(), 254); + assert!(!is_canonical_dns_host(&oversized_name)); + assert!(unsupported_host_glob(&oversized_name)); + assert!(unsupported_host_glob("api$.example.com")); + for unsupported in ["-api.example.com", "api-.example.com"] { + assert!(!is_canonical_dns_host(unsupported)); + assert!(unsupported_host_glob(unsupported)); + + let candidate = parse(&format!( + "version: 1\nnetwork_policies:\n n:\n endpoints: [{{ host: {unsupported}, port: 443 }}]\n binaries: []\n" + )); + assert!(matches!( + check_within_maximum(&parse("version: 1\n"), &candidate, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnsupportedPolicyShape + && evidence.reason().contains("endpoint host") + )); + } + } + #[test] fn differing_binary_selectors_are_checked_when_identity_is_required() { let maximum = parse( @@ -2405,6 +2624,9 @@ mod tests { ("**.example.com", "example.com"), ("api*.example.com", "api.example.com"), ("api*.example.com", "api-v2.example.com"), + ("api*.example.com", "api_internal.example.com"), + ("*.example.com", "_service.example.com"), + ("api-internal.example.com", "api-internal.example.com"), ]; for (pattern, host) in cases { let runtime = HostPattern::new(pattern).unwrap().matches(host); @@ -2498,6 +2720,10 @@ mod tests { "/a/xb", "/a/x/z/xb/y/b", "/a/c", + "/a/é/b", + "/a/汉/b", + "/a/e\u{301}/b", + "/a/😀/b", ] { let query = format!( "glob.match({}, [\"/\"], {})", @@ -2520,4 +2746,83 @@ mod tests { } } } + + #[test] + fn z3_string_boundary_decodes_exactly_or_fails_closed() { + for (expected, exactly_decodable) in [ + ("ascii", true), + (r"a\b", true), + ("é", false), + ("e\u{301}", false), + ("𐐷", false), + ("😀", false), + ] { + let solver = Solver::new(); + let value = Z3String::fresh_const("round_trip"); + solver.assert(value.eq(Z3String::from_str(expected).unwrap())); + assert_eq!(solver.check(), SatResult::Sat, "value={expected:?}"); + let model = solver.get_model().unwrap(); + let decoded = model_string_exact(&model, &value); + if exactly_decodable { + assert_eq!(decoded.as_deref(), Some(expected), "value={expected:?}"); + } else if let Some(decoded) = decoded { + assert_eq!(decoded, expected, "value={expected:?}"); + } + } + } + + #[test] + fn unicode_network_literals_are_unsupported_in_both_inputs() { + let policies = [ + ( + "binary path", + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: '/usr/bin/é*' }]\n", + ), + ( + "endpoint host", + "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: 'é.example.com', port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", + ), + ( + "endpoint path", + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - { host: api.example.com, port: 443, protocol: rest, enforcement: enforce, path: '/é/**', access: full }\n binaries: [{ path: /usr/bin/curl }]\n", + ), + ( + "REST allow method", + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: 'GÉT', path: '/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ), + ( + "REST allow path", + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: GET, path: '/é/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ), + ( + "REST deny method", + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: GET, path: '/**' } }]\n deny_rules: [{ method: 'DÉLETE', path: '/**' }]\n binaries: [{ path: /usr/bin/curl }]\n", + ), + ( + "REST deny path", + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: GET, path: '/**' } }]\n deny_rules: [{ method: GET, path: '/é/**' }]\n binaries: [{ path: /usr/bin/curl }]\n", + ), + ]; + let empty = parse("version: 1\n"); + for (field, yaml) in policies { + let policy = parse(yaml); + for (maximum, candidate, label) in [ + (&policy, &empty, "maximum"), + (&empty, &policy, "candidate"), + (&policy, &policy, "maximum"), + ] { + let result = check_within_maximum(maximum, candidate, options()); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnsupportedPolicyShape + && evidence.reason().contains(label) + && evidence.reason().contains(field) + ), + "field={field} input={label} result={result:?}" + ); + } + } + } } diff --git a/crates/openshell-prover/tests/runtime_parity.rs b/crates/openshell-prover/tests/runtime_parity.rs index bd90156999..3eef1cbbfb 100644 --- a/crates/openshell-prover/tests/runtime_parity.rs +++ b/crates/openshell-prover/tests/runtime_parity.rs @@ -4,7 +4,7 @@ //! Regression tests against the network supervisor's actual Rego policy. use openshell_prover::containment::{ - CheckOptions, CheckResult, check_within_maximum, parse_policy_str, + CheckOptions, CheckResult, Counterexample, check_within_maximum, parse_policy_str, }; use regorus::{Engine, Value}; use serde_json::json; @@ -26,11 +26,15 @@ fn check(maximum: &str, candidate: &str) -> CheckResult { } fn runtime_engine(policy: &str) -> Engine { + runtime_engine_with_identity(policy, true) +} + +fn runtime_engine_with_identity(policy: &str, require_binary_identity: bool) -> Engine { let yaml: serde_yml::Value = serde_yml::from_str(policy).expect("valid policy YAML"); let mut data = serde_json::to_value(yaml).expect("policy converts to JSON"); data.as_object_mut().expect("policy is an object").insert( "runtime".to_owned(), - json!({ "require_binary_identity": true }), + json!({ "require_binary_identity": require_binary_identity }), ); let mut engine = Engine::new(); @@ -83,6 +87,43 @@ fn eval_array_len(engine: &mut Engine, input: &Value, rule: &str) -> usize { } } +#[test] +fn underscore_host_counterexample_replays_at_runtime() { + let maximum = "version: 1\n"; + let candidate = r" +version: 1 +network_policies: + egress: + endpoints: [{ host: api_internal.example.com, ports: [443] }] + binaries: [{ path: /usr/bin/curl }] +"; + let result = check(maximum, candidate); + let CheckResult::Exceeds(evidence) = result else { + panic!("expected exceeding witness, got {result:?}"); + }; + let Counterexample::Network { + host, + binary_identity_required, + .. + } = evidence.counterexample() + else { + panic!("expected a network counterexample"); + }; + assert_eq!(host, "api_internal.example.com"); + + let input = runtime_input("/usr/bin/curl", &[], host, "GET"); + assert!(eval_bool( + &mut runtime_engine_with_identity(candidate, *binary_identity_required), + &input, + "data.openshell.sandbox.allow_network" + )); + assert!(!eval_bool( + &mut runtime_engine_with_identity(maximum, *binary_identity_required), + &input, + "data.openshell.sandbox.allow_network" + )); +} + #[test] fn recursive_path_globs_preserve_zero_directory_grants_and_denies() { let policy = |grant: &str, deny: Option<&str>, endpoint: &str| { @@ -145,6 +186,84 @@ fn recursive_path_globs_preserve_zero_directory_grants_and_denies() { } } +#[test] +fn ascii_wildcards_match_unicode_runtime_paths_in_allows_and_denies() { + let candidate = r#" +version: 1 +network_policies: + grant: + endpoints: + - host: api.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{ allow: { method: GET, path: "/items/*" } }] + binaries: [{ path: /usr/bin/curl }] +"#; + let maximum = r#" +version: 1 +network_policies: + grant: + endpoints: + - host: api.example.com + ports: [443] + protocol: rest + enforcement: enforce + rules: [{ allow: { method: GET, path: "/**" } }] + deny_rules: [{ method: GET, path: "/items/*" }] + binaries: [{ path: /usr/bin/curl }] +"#; + + for path in ["/items/é", "/items/汉", "/items/e\u{301}", "/items/😀"] { + let input: Value = serde_json::from_value(json!({ + "exec": {"path": "/usr/bin/curl", "ancestors": [], "cmdline_paths": []}, + "network": {"host": "api.example.com", "port": 443}, + "request": {"method": "GET", "path": path, "query_params": {}} + })) + .unwrap(); + assert!( + eval_bool( + &mut runtime_engine(candidate), + &input, + "data.openshell.sandbox.allow_request" + ), + "candidate should allow {path:?}" + ); + assert!( + !eval_bool( + &mut runtime_engine(maximum), + &input, + "data.openshell.sandbox.allow_request" + ), + "maximum should deny {path:?}" + ); + } + assert!(matches!(check(maximum, candidate), CheckResult::Exceeds(_))); + + let binary_wildcard = r#" +version: 1 +network_policies: + grant: + endpoints: [{ host: api.example.com, ports: [443] }] + binaries: [{ path: "/usr/bin/*" }] +"#; + for binary in [ + "/usr/bin/é", + "/usr/bin/汉", + "/usr/bin/e\u{301}", + "/usr/bin/😀", + ] { + assert!( + eval_bool( + &mut runtime_engine(binary_wildcard), + &runtime_input(binary, &[], "api.example.com", "GET"), + "data.openshell.sandbox.allow_network" + ), + "runtime binary wildcard should allow {binary:?}" + ); + } +} + #[test] fn intra_label_host_wildcard_matches_empty_suffix_at_runtime() { let maximum = r#" diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx index bf69ac1d95..a279192a74 100644 --- a/docs/reference/policy-prover.mdx +++ b/docs/reference/policy-prover.mdx @@ -130,6 +130,15 @@ The result object reports the domains used for each check. Policies that use recognized authority outside that model return `unsupported` rather than silently ignoring it. +Network binary selectors, endpoint host and path selectors, and REST allow and +deny method and path selectors must use ASCII literals in both the candidate and +maximum. A non-ASCII literal in one of these fields returns `unsupported` with +`reason_code: unsupported_policy_shape`, including when it appears only in a +deny. This is a prover-model limitation, not a general policy validation rule: +filesystem paths and unrelated policy text retain their existing Unicode +behavior. ASCII wildcard selectors still cover non-ASCII runtime values matched +by the policy engine. + Containment means `Allowed(candidate)` is a subset of `Allowed(maximum)` under the reported model. It does not establish least privilege, automatic approval eligibility, semantic safety, or equivalence to a running sandbox's kernel @@ -154,6 +163,9 @@ state. In particular: match the executable or an ancestor identity. Network counterexamples report the configuration and identities that expose the additional authority. - REST containment witnesses use canonical request methods and paths. +- If a solver string cannot be decoded and validated faithfully, the command + returns `inconclusive` with `reason_code: invalid_witness` instead of emitting + a counterexample. - Both files are interpreted in the same sandbox filesystem namespace and mount model, with stable path resolution when enforcement rules are created. The CLI does not resolve sandbox paths against the host. From fd2880fc48040dca429d7ef1949599a095b2086b Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Fri, 11 Sep 2026 23:46:09 +0000 Subject: [PATCH 07/12] fix(prover): reject ambiguous z3 string escapes Signed-off-by: Johnny Greco --- crates/openshell-prover/src/containment.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index d64118baad..357c7a0f9c 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -1124,6 +1124,13 @@ fn counterexample_from_model( fn model_string_exact(model: &z3::Model, value: &Z3String) -> Option { let evaluated = model.eval(value, true)?; let decoded = evaluated.as_string()?; + // Some Z3 versions expose non-ASCII UTF-8 bytes through `Z3_get_string` + // as `\u{..}` sequences. The binding does not distinguish that encoding + // from literal text, so do not risk publishing the serialization as a + // concrete witness. + if decoded.contains("\\u{") { + return None; + } let reconstructed = Z3String::from_str(&decoded).ok()?; (evaluated.eq(reconstructed).simplify().as_bool() == Some(true)).then_some(decoded) } From 8036d8fc14cd53b5d67889f087b1667a02466829 Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Sat, 12 Sep 2026 01:06:06 +0000 Subject: [PATCH 08/12] fix(prover): align containment with runtime boundaries Signed-off-by: Johnny Greco --- architecture/security-policy.md | 5 +- crates/openshell-prover/README.md | 3 +- crates/openshell-prover/src/containment.rs | 201 ++++++++++++++------- docs/reference/policy-prover.mdx | 9 +- 4 files changed, 148 insertions(+), 70 deletions(-) diff --git a/architecture/security-policy.md b/architecture/security-policy.md index 3e67801397..ff002497f7 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -351,8 +351,9 @@ executable and an ancestor identity, and the evidence identifies the identities for an exceeding witness. Network binary selectors, endpoint host and path selectors, and REST allow and deny method and path selectors must use ASCII literals. This restriction applies to both inputs, including deny-only rules; -other Unicode policy text and filesystem paths are unaffected. ASCII wildcard -selectors still cover non-ASCII runtime values matched by the policy engine. +embedded NUL bytes in those fields are also unsupported. Other Unicode policy +text and filesystem paths are unaffected. ASCII wildcard selectors still cover +non-ASCII runtime values matched by the policy engine. Recognized authority outside the reviewed model produces an unsupported result rather than being silently ignored. Environment-dependent authority also remains unsupported when the result diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index 65a38bd765..b7bfe6dbe7 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -18,7 +18,8 @@ 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. ASCII wildcards are modeled over the +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. diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index 357c7a0f9c..16d52a32ed 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -87,7 +87,7 @@ pub struct ManagedPolicyMetadata { extra: BTreeMap, } -#[derive(Debug, Clone, Default, Deserialize, PartialEq)] +#[derive(Debug, Clone, Deserialize, PartialEq)] struct FilesystemPolicy { #[serde(default)] include_workdir: bool, @@ -99,6 +99,20 @@ struct FilesystemPolicy { extra: BTreeMap, } +impl Default for FilesystemPolicy { + fn default() -> Self { + Self { + // Match the runtime default when `filesystem_policy` is absent. + // Serde still uses `false` for an omitted `include_workdir` field + // inside an explicitly present filesystem policy. + include_workdir: true, + read_only: Vec::new(), + read_write: Vec::new(), + extra: BTreeMap::new(), + } + } +} + #[derive(Debug, Clone, Deserialize, PartialEq)] struct NetworkRule { #[serde(default, rename = "name")] @@ -882,8 +896,9 @@ fn assert_action_domain(solver: &Solver, action: &SymbolicAction, binary_identit ); solver.assert(action.ancestor_binary.length().le(4_096)); } - solver.assert(action.host.regex_matches(&host_domain_regex())); - solver.assert(action.host.length().le(253)); + // Keep `action.host` unconstrained: the runtime applies host globs to raw + // proxy input before DNS validation, so DNS structure and resolver length + // limits are not properties of the action domain. solver.assert(Int::from_u64(1).le(&action.port)); solver.assert(action.port.le(65_535)); solver.assert(str_eq_any(&action.layer, &[LAYER_L4, LAYER_REST])); @@ -1546,10 +1561,8 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason return unsupported(format!("rule '{rule_name}' uses unsupported fields")); } for binary in &rule.binaries { - if !binary.path.is_ascii() { - return unsupported(format!( - "rule '{rule_name}' binary path contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&binary.path) { + return unsupported(format!("rule '{rule_name}' binary path {reason}")); } if binary.path.is_empty() || !is_canonical_pattern_path(&binary.path) @@ -1561,15 +1574,11 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason } for endpoint in &rule.endpoints { let context = format!("rule '{rule_name}'"); - if !endpoint.host.is_ascii() { - return unsupported(format!( - "{context} endpoint host contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&endpoint.host) { + return unsupported(format!("{context} endpoint host {reason}")); } - if !endpoint.path.is_ascii() { - return unsupported(format!( - "{context} endpoint path contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&endpoint.path) { + return unsupported(format!("{context} endpoint path {reason}")); } if endpoint.host.is_empty() || endpoint.effective_ports().is_empty() @@ -1652,30 +1661,22 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason return unsupported(format!("{context} mixes REST controls into L4 authority")); } for rule in &endpoint.rules { - if !rule.allow.method.is_ascii() { - return unsupported(format!( - "{context} REST allow method contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&rule.allow.method) { + return unsupported(format!("{context} REST allow method {reason}")); } - if !rule.allow.path.is_ascii() { - return unsupported(format!( - "{context} REST allow path contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&rule.allow.path) { + return unsupported(format!("{context} REST allow path {reason}")); } if !rule.extra.is_empty() || unsupported_allow(&rule.allow) { return unsupported(format!("{context} uses an unsupported REST allow rule")); } } for rule in &endpoint.deny_rules { - if !rule.method.is_ascii() { - return unsupported(format!( - "{context} REST deny method contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&rule.method) { + return unsupported(format!("{context} REST deny method {reason}")); } - if !rule.path.is_ascii() { - return unsupported(format!( - "{context} REST deny path contains a non-ASCII literal" - )); + if let Some(reason) = unsupported_network_literal(&rule.path) { + return unsupported(format!("{context} REST deny path {reason}")); } if unsupported_deny(rule) { return unsupported(format!("{context} uses an unsupported REST deny rule")); @@ -1702,6 +1703,16 @@ fn unsupported_reason(label: &str, policy: &ContainmentPolicy) -> Option<(Reason None } +fn unsupported_network_literal(value: &str) -> Option<&'static str> { + if !value.is_ascii() { + Some("contains a non-ASCII literal") + } else if value.contains('\0') { + Some("contains an embedded NUL byte") + } else { + None + } +} + fn resource_limit_reason( maximum: &ContainmentPolicy, candidate: &ContainmentPolicy, @@ -1892,15 +1903,7 @@ fn glob_regex(pattern: &str, separator: &str) -> Regexp { while let Some(character) = chars.next() { if character == '*' && chars.peek() == Some(&'*') { chars.next(); - if separator == "." { - let label = non_separator_regex(separator).plus(); - parts.push(Regexp::concat(&[ - &label, - &Regexp::concat(&[&Regexp::literal("."), &label]).star(), - ])); - } else { - parts.push(Regexp::full()); - } + parts.push(Regexp::full()); } else if character == '*' { let wildcard = non_separator_regex(separator); parts.push(wildcard.star()); @@ -1972,27 +1975,9 @@ fn non_separator_regex(separator: &str) -> Regexp { ]) } -fn host_domain_regex() -> Regexp { - let alphanumeric = Regexp::union(&[&Regexp::range(&'a', &'z'), &Regexp::range(&'0', &'9')]); - // Actions represent canonical resolver inputs, not every raw value the - // proxy parser or Rego glob builtin can compare. Supported endpoint globs - // are therefore modeled over this same resolver-oriented host domain. - let label_edge = Regexp::union(&[&alphanumeric, &Regexp::literal("_")]); - let label_character = Regexp::union(&[&label_edge, &Regexp::literal("-")]); - let label = Regexp::union(&[ - &label_edge, - &Regexp::concat(&[&label_edge, &label_character.r#loop(0, 61), &label_edge]), - ]); - Regexp::concat(&[ - &label, - &Regexp::concat(&[&Regexp::literal("."), &label]).star(), - ]) -} - #[cfg(test)] mod tests { use super::*; - use openshell_core::host_pattern::HostPattern; use std::fmt::Write as _; fn parse(value: &str) -> ContainmentPolicy { @@ -2016,11 +2001,30 @@ mod tests { CheckResult::Within(_) )); assert!(matches!( - check_within_maximum(&parse("version: 1\n"), &exceeds, options()), + check_within_maximum( + &parse("version: 1\nfilesystem_policy: {}\n"), + &exceeds, + options() + ), CheckResult::Exceeds(_) )); } + #[test] + fn absent_filesystem_policy_uses_the_runtime_workdir_default() { + let omitted = parse("version: 1\n"); + assert!(omitted.filesystem_policy.include_workdir); + + let explicit = parse("version: 1\nfilesystem_policy: {}\n"); + assert!(!explicit.filesystem_policy.include_workdir); + + assert!(matches!( + check_within_maximum(&explicit, &omitted, options()), + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedWorkdir + )); + } + #[test] fn l4_contains_rest_but_not_the_reverse() { let l4 = parse( @@ -2122,7 +2126,30 @@ mod tests { } #[test] - fn host_domain_enforces_modeled_label_and_name_boundaries() { + fn host_action_domain_covers_noncanonical_wildcard_matches() { + for (pattern, host) in [ + ("*.example.com", ".example.com".to_owned()), + ("**.example.com", "api..example.com".to_owned()), + ("*.example.com", "é.example.com".to_owned()), + ("*.example.com", "$service.example.com".to_owned()), + ("*.example.com", "-api.example.com".to_owned()), + ("*.example.com", format!("{}.example.com", "a".repeat(242))), + ] { + let solver = Solver::new(); + let action = symbolic_action("host_superset"); + assert_action_domain(&solver, &action, false); + solver.assert(action.host.eq(Z3String::from_str(&host).unwrap())); + solver.assert(action.host.regex_matches(&glob_regex(pattern, "."))); + assert_eq!( + solver.check(), + SatResult::Sat, + "pattern={pattern:?} host={host:?}" + ); + } + } + + #[test] + fn host_literals_enforce_modeled_label_and_name_boundaries() { let maximum_length = format!( "{}.{}.{}.{}", "a".repeat(63), @@ -2357,7 +2384,7 @@ mod tests { CheckResult::Unsupported(_) )); let workdir = parse("version: 1\nfilesystem_policy: { include_workdir: true }\n"); - let empty = parse("version: 1\n"); + let empty = parse("version: 1\nfilesystem_policy: {}\n"); assert!(matches!( check_within_maximum(&empty, &workdir, options()), CheckResult::Unsupported(_) @@ -2633,17 +2660,29 @@ mod tests { ("api*.example.com", "api-v2.example.com"), ("api*.example.com", "api_internal.example.com"), ("*.example.com", "_service.example.com"), + ("*.example.com", ".example.com"), + ("**.example.com", "api..example.com"), + ("*.example.com", "é.example.com"), + ("*.example.com", "$service.example.com"), + ("*.example.com", "-api.example.com"), ("api-internal.example.com", "api-internal.example.com"), ]; + let mut runtime = regorus::Engine::new(); for (pattern, host) in cases { - let runtime = HostPattern::new(pattern).unwrap().matches(host); + let query = format!( + "glob.match({}, [\".\"], {})", + serde_json::to_string(pattern).unwrap(), + serde_json::to_string(host).unwrap() + ); + let actual = runtime.eval_query(query, false).unwrap(); + let expected = actual.result[0].expressions[0].value == regorus::Value::from(true); let solver = Solver::new(); let modeled = Z3String::from_str(host) .unwrap() .regex_matches(&glob_regex(pattern, ".")); solver.assert(!modeled); let prover = solver.check() == SatResult::Unsat; - assert_eq!(prover, runtime, "pattern={pattern} host={host}"); + assert_eq!(prover, expected, "pattern={pattern} host={host}"); } } @@ -2832,4 +2871,40 @@ mod tests { } } } + + #[test] + fn embedded_nul_network_literal_is_unsupported_before_solving() { + assert_eq!(unsupported_network_literal("ascii"), None); + assert_eq!( + unsupported_network_literal("é"), + Some("contains a non-ASCII literal") + ); + assert_eq!( + unsupported_network_literal("G\0ET"), + Some("contains an embedded NUL byte") + ); + + let policy = parse( + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: \"G\\0ET\", path: '/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ); + let empty = parse("version: 1\n"); + for (maximum, candidate, label) in [ + (&policy, &empty, "maximum"), + (&empty, &policy, "candidate"), + (&policy, &policy, "maximum"), + ] { + let result = check_within_maximum(maximum, candidate, options()); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnsupportedPolicyShape + && evidence.reason().contains(label) + && evidence.reason().contains("REST allow method") + && evidence.reason().contains("NUL") + ), + "input={label} result={result:?}" + ); + } + } } diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx index a279192a74..c881060a62 100644 --- a/docs/reference/policy-prover.mdx +++ b/docs/reference/policy-prover.mdx @@ -134,10 +134,11 @@ Network binary selectors, endpoint host and path selectors, and REST allow and deny method and path selectors must use ASCII literals in both the candidate and maximum. A non-ASCII literal in one of these fields returns `unsupported` with `reason_code: unsupported_policy_shape`, including when it appears only in a -deny. This is a prover-model limitation, not a general policy validation rule: -filesystem paths and unrelated policy text retain their existing Unicode -behavior. ASCII wildcard selectors still cover non-ASCII runtime values matched -by the policy engine. +deny. Embedded NUL bytes in these fields are also unsupported. This is a +prover-model limitation, not a general policy validation rule: filesystem paths +and unrelated policy text retain their existing Unicode behavior. ASCII +wildcard selectors still cover non-ASCII runtime values matched by the policy +engine. Containment means `Allowed(candidate)` is a subset of `Allowed(maximum)` under the reported model. It does not establish least privilege, automatic approval From 5764a6b6d5962b60e080de353553bc3d3e76183c Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Sat, 12 Sep 2026 01:06:43 +0000 Subject: [PATCH 09/12] fix(prover-cli): harden cancellation and invalid input Signed-off-by: Johnny Greco --- crates/openshell-prover-cli/src/main.rs | 9 +++++-- crates/openshell-prover-cli/tests/cli.rs | 31 +++++++++++++++++++++++- 2 files changed, 37 insertions(+), 3 deletions(-) diff --git a/crates/openshell-prover-cli/src/main.rs b/crates/openshell-prover-cli/src/main.rs index 3209112a8c..55f8a54dc1 100644 --- a/crates/openshell-prover-cli/src/main.rs +++ b/crates/openshell-prover-cli/src/main.rs @@ -106,9 +106,14 @@ enum CounterexampleJson<'a> { fn main() -> ExitCode { let cancelled = Arc::new(AtomicBool::new(false)); #[cfg(unix)] - if let Err(error) = + if let Err(error) = signal_hook::flag::register_conditional_shutdown( + signal_hook::consts::signal::SIGINT, + 130, + Arc::clone(&cancelled), + ) + .and_then(|_| { signal_hook::flag::register(signal_hook::consts::signal::SIGINT, Arc::clone(&cancelled)) - { + }) { let _ = writeln!( io::stderr().lock(), "openshell-prover: cannot install Ctrl-C handler: {error}" diff --git a/crates/openshell-prover-cli/tests/cli.rs b/crates/openshell-prover-cli/tests/cli.rs index 7d776f2d83..f973f2698b 100644 --- a/crates/openshell-prover-cli/tests/cli.rs +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -181,6 +181,35 @@ fn non_ascii_network_literals_are_unsupported_in_both_inputs() { assert!(text.contains("non-ASCII"), "{text}"); } +#[test] +fn embedded_nul_network_literal_is_unsupported_without_panicking() { + let path = std::env::temp_dir().join(format!( + "openshell-prover-nul-selector-{}.yaml", + std::process::id() + )); + fs::write( + &path, + "version: 1\nnetwork_policies:\n n:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n rules: [{ allow: { method: \"G\\0ET\", path: '/**' } }]\n binaries: [{ path: /usr/bin/curl }]\n", + ) + .expect("write NUL selector policy"); + let output = run(&[ + "check", + path.to_str().expect("UTF-8 temporary path"), + "--maximum", + fixture("maximum-empty.yaml").to_str().unwrap(), + "--output", + "json", + ]); + fs::remove_file(path).expect("remove NUL selector policy"); + + assert_eq!(output.status.code(), Some(3)); + assert!(output.stderr.is_empty()); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["result"], "unsupported"); + assert_eq!(value["reason_code"], "unsupported_policy_shape"); + assert!(value["reason"].as_str().unwrap().contains("NUL")); +} + #[test] fn resource_exhaustion_is_inconclusive_and_returns_three() { let path = std::env::temp_dir().join(format!( @@ -394,13 +423,13 @@ fn sigint_interrupts_the_check_with_exit_130() { .expect("send SIGINT"); assert!(signal.success()); let output = child.wait_with_output().expect("wait for cancelled prover"); - fs::remove_dir_all(directory).expect("remove cancellation policies"); assert_eq!(output.status.code(), Some(130)); let value: Value = serde_json::from_slice(&output.stdout).expect("structured cancellation JSON"); assert_eq!(value["result"], "inconclusive"); assert_eq!(value["reason_code"], "cancelled"); assert_eq!(value["exit_code"], 130); + fs::remove_dir_all(directory).expect("remove cancellation policies"); } #[cfg(unix)] From 1c21e6e8929a529dae7f780d95423c41710b7789 Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Sat, 12 Sep 2026 02:04:12 +0000 Subject: [PATCH 10/12] feat(packaging): install policy prover with OpenShell Signed-off-by: Johnny Greco --- .github/workflows/build-rpm.yml | 11 ++++++++++- .github/workflows/conformance.yml | 17 ++++++++++++++++- .github/workflows/deb-package.yml | 9 ++++++++- .github/workflows/release-dev.yml | 13 ++++++++++--- .github/workflows/release-tag.yml | 11 ++++++++--- .github/workflows/rpm-package.yml | 3 +++ architecture/build.md | 15 ++++++++------- deploy/deb/control.in | 5 +++-- docs/about/installation.mdx | 8 ++++---- docs/reference/support-matrix.mdx | 14 +++++++++++++- install.sh | 20 ++++++++++++++++---- openshell.spec | 21 +++++++++++++++++++++ python/openshell/release_formula_test.py | 12 ++++++++++++ tasks/scripts/package-deb-install.sh | 5 ++++- tasks/scripts/package-deb.sh | 3 +++ tasks/scripts/release.py | 19 +++++++++++++++++++ tasks/scripts/test-install-sh.sh | 11 +++++++++++ tasks/scripts/test-packaging-assets.sh | 11 ++++++++++- 18 files changed, 179 insertions(+), 29 deletions(-) diff --git a/.github/workflows/build-rpm.yml b/.github/workflows/build-rpm.yml index 71aa04dddf..0b07af3160 100644 --- a/.github/workflows/build-rpm.yml +++ b/.github/workflows/build-rpm.yml @@ -21,6 +21,9 @@ on: gateway-target: required: true type: string + prover-target: + required: true + type: string rpm-version: required: false type: string @@ -81,10 +84,16 @@ jobs: name: openshell-gateway-${{ inputs.gateway-target }} path: package-binaries/ + - name: Download prover artifact + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: openshell-prover-${{ inputs.prover-target }} + path: package-binaries/ + - name: Configure package inputs run: | set -euo pipefail - chmod +x package-binaries/openshell{,-gateway} + chmod +x package-binaries/openshell{,-gateway,-prover} ls -lah package-binaries - name: Mark workspace safe for git diff --git a/.github/workflows/conformance.yml b/.github/workflows/conformance.yml index 242f8c7d01..cfab36aa7f 100644 --- a/.github/workflows/conformance.yml +++ b/.github/workflows/conformance.yml @@ -97,8 +97,22 @@ jobs: checkout-ref: ${{ github.sha }} secrets: inherit + build-prover: + needs: version + permissions: + contents: read + uses: ./.github/workflows/build-binaries.yml + with: + package: openshell-prover-cli + binary: openshell-prover + triple: x86_64-unknown-linux-musl + runner: linux-amd64-cpu8 + cargo-version: ${{ needs.version.outputs.cargo }} + checkout-ref: ${{ github.sha }} + secrets: inherit + build-rpm: - needs: [version, build-cli, build-gateway] + needs: [version, build-cli, build-gateway, build-prover] permissions: contents: read uses: ./.github/workflows/build-rpm.yml @@ -108,6 +122,7 @@ jobs: runner: linux-amd64-cpu8 cli-target: x86_64-unknown-linux-musl gateway-target: x86_64-unknown-linux-gnu + prover-target: x86_64-unknown-linux-musl cargo-version: ${{ needs.version.outputs.cargo }} rpm-version: ${{ needs.version.outputs.rpm_version }} rpm-release: ${{ needs.version.outputs.rpm_release }} diff --git a/.github/workflows/deb-package.yml b/.github/workflows/deb-package.yml index 7008acd4ed..1ec52dc3a1 100644 --- a/.github/workflows/deb-package.yml +++ b/.github/workflows/deb-package.yml @@ -58,6 +58,12 @@ jobs: name: openshell-gateway-${{ matrix.gnu_target }} path: package-binaries/ + - name: Download prover artifact + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: openshell-prover-${{ matrix.cli_target }} + path: package-binaries/ + - name: Download VM driver artifact uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 with: @@ -67,7 +73,7 @@ jobs: - name: Configure package inputs run: | set -euo pipefail - chmod +x package-binaries/openshell{,-gateway,-driver-vm} + chmod +x package-binaries/openshell{,-gateway,-prover,-driver-vm} ls -lah package-binaries - name: Build Debian package @@ -75,6 +81,7 @@ jobs: set -euo pipefail OPENSHELL_CLI_BINARY="${PWD}/package-binaries/openshell" \ OPENSHELL_GATEWAY_BINARY="${PWD}/package-binaries/openshell-gateway" \ + OPENSHELL_PROVER_BINARY="${PWD}/package-binaries/openshell-prover" \ OPENSHELL_DRIVER_VM_BINARY="${PWD}/package-binaries/openshell-driver-vm" \ OPENSHELL_DEB_VERSION="${INPUTS_DEB_VERSION}" \ OPENSHELL_DEB_ARCH="${{ matrix.deb_arch }}" \ diff --git a/.github/workflows/release-dev.yml b/.github/workflows/release-dev.yml index b411674448..1ca128a1d4 100644 --- a/.github/workflows/release-dev.yml +++ b/.github/workflows/release-dev.yml @@ -253,7 +253,7 @@ jobs: build-deb: name: Build Debian Packages - needs: [compute-versions, build-cli, build-gateway, build-vm-driver] + needs: [compute-versions, build-cli, build-prover, build-gateway, build-vm-driver] uses: ./.github/workflows/deb-package.yml with: deb-version: ${{ needs.compute-versions.outputs.deb_version }} @@ -273,7 +273,7 @@ jobs: build-rpm: name: Build RPM Packages - needs: [compute-versions, build-cli, build-gateway] + needs: [compute-versions, build-cli, build-prover, build-gateway] uses: ./.github/workflows/rpm-package.yml with: checkout-ref: ${{ github.sha }} @@ -335,6 +335,7 @@ jobs: set -euo pipefail apt-get update apt-get install -y --no-install-recommends ./package-input/*.deb + openshell-prover --version LD_BIND_NOW=1 openshell-gateway --version /usr/libexec/openshell/openshell-driver-vm --version @@ -349,7 +350,11 @@ jobs: if: matrix.kind == 'rpm' run: | set -euo pipefail - dnf install -y ./package-input/openshell-[0-9]*.rpm ./package-input/openshell-gateway-*.rpm + dnf install -y \ + ./package-input/openshell-[0-9]*.rpm \ + ./package-input/openshell-gateway-*.rpm \ + ./package-input/openshell-prover-*.rpm + openshell-prover --version LD_BIND_NOW=1 openshell-gateway --version - name: Download Python wheel artifact @@ -481,6 +486,8 @@ jobs: move_one openshell-dev-aarch64.rpm release/openshell-[0-9]*.aarch64.rpm move_one openshell-gateway-dev-x86_64.rpm release/openshell-gateway-[0-9]*.x86_64.rpm move_one openshell-gateway-dev-aarch64.rpm release/openshell-gateway-[0-9]*.aarch64.rpm + move_one openshell-prover-dev-x86_64.rpm release/openshell-prover-[0-9]*.x86_64.rpm + move_one openshell-prover-dev-aarch64.rpm release/openshell-prover-[0-9]*.aarch64.rpm ls -la release/ diff --git a/.github/workflows/release-tag.yml b/.github/workflows/release-tag.yml index 66ef2803eb..70a8152aa2 100644 --- a/.github/workflows/release-tag.yml +++ b/.github/workflows/release-tag.yml @@ -306,7 +306,7 @@ jobs: build-deb: name: Build Debian Packages - needs: [compute-versions, build-cli, build-gateway, build-vm-driver] + needs: [compute-versions, build-cli, build-prover, build-gateway, build-vm-driver] uses: ./.github/workflows/deb-package.yml with: deb-version: ${{ needs.compute-versions.outputs.deb_version }} @@ -327,7 +327,7 @@ jobs: build-rpm: name: Build RPM Packages - needs: [compute-versions, build-cli, build-gateway] + needs: [compute-versions, build-cli, build-prover, build-gateway] uses: ./.github/workflows/rpm-package.yml with: checkout-ref: ${{ inputs.tag || github.ref }} @@ -432,6 +432,7 @@ jobs: set -euo pipefail apt-get update apt-get install -y --no-install-recommends ./package-input/*.deb + openshell-prover --version LD_BIND_NOW=1 openshell-gateway --version /usr/libexec/openshell/openshell-driver-vm --version @@ -446,7 +447,11 @@ jobs: if: matrix.kind == 'rpm' run: | set -euo pipefail - dnf install -y ./package-input/openshell-[0-9]*.rpm ./package-input/openshell-gateway-*.rpm + dnf install -y \ + ./package-input/openshell-[0-9]*.rpm \ + ./package-input/openshell-gateway-*.rpm \ + ./package-input/openshell-prover-*.rpm + openshell-prover --version LD_BIND_NOW=1 openshell-gateway --version - name: Download Python wheel artifact diff --git a/.github/workflows/rpm-package.yml b/.github/workflows/rpm-package.yml index 5cda9a88c3..5e2e50ac59 100644 --- a/.github/workflows/rpm-package.yml +++ b/.github/workflows/rpm-package.yml @@ -40,10 +40,12 @@ jobs: runner: linux-amd64-cpu8 cli_target: x86_64-unknown-linux-musl gateway_target: x86_64-unknown-linux-gnu + prover_target: x86_64-unknown-linux-musl - arch: aarch64 runner: linux-arm64-cpu8 cli_target: aarch64-unknown-linux-musl gateway_target: aarch64-unknown-linux-gnu + prover_target: aarch64-unknown-linux-musl uses: ./.github/workflows/build-rpm.yml with: checkout-ref: ${{ inputs.checkout-ref }} @@ -51,6 +53,7 @@ jobs: runner: ${{ matrix.runner }} cli-target: ${{ matrix.cli_target }} gateway-target: ${{ matrix.gateway_target }} + prover-target: ${{ matrix.prover_target }} rpm-version: ${{ inputs.rpm-version }} rpm-release: ${{ inputs.rpm-release }} cargo-version: ${{ inputs.cargo-version }} diff --git a/architecture/build.md b/architecture/build.md index 4390fffd07..3f9e8f8b3b 100644 --- a/architecture/build.md +++ b/architecture/build.md @@ -86,13 +86,14 @@ HTTP/TLS support behind explicit build features, so default system-Z3 builds do not reintroduce bundled Mozilla roots. Release builds that need bundled Z3 continue to opt in with `bundled-z3`. -The standalone `openshell-prover` executable is distributed independently of -the main CLI. Release workflows build Linux musl x86_64 and aarch64 binaries -and a macOS Apple Silicon binary, then publish one archive per target plus a -dedicated SHA-256 manifest. Before publication, target-native jobs extract each -archive, reject host Z3 or Nix store linkage, and run a real local containment -check. The tool therefore requires neither an OpenShell installation nor a -separately installed Z3 runtime. +Release workflows build the standalone `openshell-prover` executable for Linux +musl x86_64 and aarch64 and macOS Apple Silicon. The standard Debian, RPM, and +Homebrew installations include it, following the same package-managed pattern +as `openshell-gateway`. Releases also publish one standalone archive per target +plus a dedicated SHA-256 manifest. Before publication, target-native jobs +extract each archive, reject host Z3 or Nix store linkage, and run a real local +containment check. The standalone artifact therefore requires neither an +OpenShell installation nor a separately installed Z3 runtime. ## Linux Runtime Environments diff --git a/deploy/deb/control.in b/deploy/deb/control.in index 9f77f8775d..e0975d4d4d 100644 --- a/deploy/deb/control.in +++ b/deploy/deb/control.in @@ -9,8 +9,9 @@ Homepage: https://github.com/NVIDIA/OpenShell Description: Safe, sandboxed runtimes for autonomous AI agents OpenShell provides host-side command-line and gateway components for launching and managing policy-enforced AI agent sandboxes. The package - installs the openshell CLI, openshell-gateway daemon, and the VM compute - driver helper, plus a per-user systemd unit for running the gateway. + installs the openshell CLI, standalone policy prover, openshell-gateway daemon, + and the VM compute driver helper, plus a per-user systemd unit for running the + gateway. . The systemd unit is user-scope (under /usr/lib/systemd/user/). To start it, run `systemctl --user enable --now openshell-gateway`. diff --git a/docs/about/installation.mdx b/docs/about/installation.mdx index a40d908fa3..33b4dfc95f 100644 --- a/docs/about/installation.mdx +++ b/docs/about/installation.mdx @@ -16,7 +16,7 @@ Install OpenShell with a single command: curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh ``` -The script detects your operating system and installs the OpenShell CLI and gateway with your native package manager. It then starts the local gateway server so you can begin creating sandboxes. +The script detects your operating system and installs the OpenShell CLI, standalone policy prover, and gateway with your native package manager. It then starts the local gateway server so you can begin creating sandboxes. You can also download release artifacts directly from the [OpenShell GitHub Releases](https://github.com/NVIDIA/OpenShell/releases) page. @@ -42,7 +42,7 @@ For detailed driver behavior, refer to [Sandbox Compute Drivers](/reference/sand ## macOS -On macOS, the install script uses Homebrew. The Homebrew package installs the `openshell` CLI, the gateway binary, and a Homebrew-managed gateway service. +On macOS, the install script uses Homebrew. The Homebrew package installs the `openshell` CLI, `openshell-prover`, the gateway binary, and a Homebrew-managed gateway service. The Homebrew service uses the gateway's built-in `127.0.0.1:17670` listener and generates a local mTLS bundle on install. The installer registers `https://localhost:17670` with the CLI so TLS uses a DNS name covered by the generated certificate. The formula creates a Homebrew prefix config, such as `/opt/homebrew/var/openshell/gateway.toml`, without overriding `bind_address`. Docker Desktop and Podman Machine reuse the primary listener for sandbox callbacks when they can reach it. The gateway reads `~/.config/openshell/gateway.toml` instead when that file exists. Homebrew upgrades migrate exact package-generated schema-v1 prefix configs, including the affected IPv6 variant. They preserve edited prefix configs and all user configs. Follow the [schema version 2 migration steps](/reference/gateway-config#migrate-to-schema-version-2) for an edited v1 file. @@ -57,9 +57,9 @@ brew services restart openshell ## Linux -On Fedora and RHEL, the install script uses RPM packages. The RPM installs the `openshell` CLI, the `openshell-gateway` daemon, and a systemd user service. +On Fedora and RHEL, the install script uses RPM packages. The RPMs install the `openshell` CLI, `openshell-prover`, the `openshell-gateway` daemon, and a systemd user service. -On Debian and Ubuntu, the install script uses a Debian package. The Debian package installs the `openshell` CLI, the `openshell-gateway` daemon, VM sandbox support, and a systemd user service. +On Debian and Ubuntu, the install script uses a Debian package. The Debian package installs the `openshell` CLI, `openshell-prover`, the `openshell-gateway` daemon, VM sandbox support, and a systemd user service. Linux packages require glibc 2.28 or newer. The installer checks libc before downloading packages and exits with an error on older glibc versions, Alpine, musl-based distributions, or unknown libc environments. diff --git a/docs/reference/support-matrix.mdx b/docs/reference/support-matrix.mdx index cfa5b69549..22fd35bcae 100644 --- a/docs/reference/support-matrix.mdx +++ b/docs/reference/support-matrix.mdx @@ -10,7 +10,7 @@ This page lists the host platform, compute driver, software, runtime, and kernel ## Supported Platforms -OpenShell publishes multi-architecture gateway images for `linux/amd64` and `linux/arm64`. The CLI, package-managed gateway, and standalone gateway binary are supported on the following host platforms: +OpenShell publishes multi-architecture gateway images for `linux/amd64` and `linux/arm64`. The CLI, policy prover, package-managed gateway, and standalone gateway binary are supported on the following host platforms: | Platform | Architecture | Status | | -------------------------------- | --------------------- | --------- | @@ -35,6 +35,18 @@ These artifacts are attached to GitHub releases. Kubernetes deployments should u On Linux, `openshell-gateway` requires glibc 2.28 or newer. Compatible systems include, for example, Ubuntu 20.04+, RHEL 8+, Rocky Linux 8+, Amazon Linux 2023+, and Fedora 32+. +## Standalone Policy Prover + +OpenShell publishes standalone `openshell-prover` release assets for manual download on these platforms: + +| Platform | Artifact pattern | +| --------------------- | ----------------------------------------------------- | +| Linux x86_64 (amd64) | `openshell-prover-x86_64-unknown-linux-musl.tar.gz` | +| Linux aarch64 (arm64) | `openshell-prover-aarch64-unknown-linux-musl.tar.gz` | +| macOS Apple Silicon | `openshell-prover-aarch64-apple-darwin.tar.gz` | + +These artifacts are attached to GitHub releases. The Linux binaries are static and do not require glibc. All prover archives include the required solver linkage. + ## Compute Drivers The gateway can manage sandboxes through several compute drivers. diff --git a/install.sh b/install.sh index faa10c3e3b..7f86736148 100755 --- a/install.sh +++ b/install.sh @@ -583,6 +583,10 @@ find_rpm_asset() { _dev_name="openshell-gateway-dev-${_arch}.rpm" _fallback_re="^openshell-gateway-[0-9].*\\.${_arch}\\.rpm$" ;; + openshell-prover) + _dev_name="openshell-prover-dev-${_arch}.rpm" + _fallback_re="^openshell-prover-[0-9].*\\.${_arch}\\.rpm$" + ;; *) error "unknown RPM package selector: ${_package}" ;; @@ -944,9 +948,14 @@ install_linux_rpm() { error "no openshell-gateway RPM package found for architecture: ${_arch}" fi - info "selected ${_rpm_file} and ${_gateway_rpm_file}" + _prover_rpm_file="$(find_rpm_asset "${_tmpdir}/${CHECKSUMS_NAME}" "$_arch" openshell-prover)" + if [ -z "$_prover_rpm_file" ]; then + error "no openshell-prover RPM package found for architecture: ${_arch}" + fi + + info "selected ${_rpm_file}, ${_gateway_rpm_file}, and ${_prover_rpm_file}" - for _package_file in "$_rpm_file" "$_gateway_rpm_file"; do + for _package_file in "$_rpm_file" "$_gateway_rpm_file" "$_prover_rpm_file"; do _package_url="${GITHUB_URL}/releases/download/${RELEASE_TAG}/${_package_file}" _package_path="${_tmpdir}/${_package_file}" @@ -960,8 +969,11 @@ install_linux_rpm() { verify_checksum "$_package_path" "${_tmpdir}/${CHECKSUMS_NAME}" "$_package_file" done - info "installing ${_rpm_file} and ${_gateway_rpm_file}..." - install_rpm_packages "${_tmpdir}/${_rpm_file}" "${_tmpdir}/${_gateway_rpm_file}" + info "installing ${_rpm_file}, ${_gateway_rpm_file}, and ${_prover_rpm_file}..." + install_rpm_packages \ + "${_tmpdir}/${_rpm_file}" \ + "${_tmpdir}/${_gateway_rpm_file}" \ + "${_tmpdir}/${_prover_rpm_file}" info "installed ${APP_NAME} RPM packages from ${RELEASE_TAG}" start_user_gateway } diff --git a/openshell.spec b/openshell.spec index ce35f73791..ee9d7d5f5a 100644 --- a/openshell.spec +++ b/openshell.spec @@ -58,6 +58,14 @@ lifecycle management. This package installs Podman-oriented defaults in gateway TOML while leaving compute driver selection to gateway auto-detection or explicit operator configuration. +# --- Standalone policy prover sub-package --- +%package prover +Summary: Standalone OpenShell policy boundary prover + +%description prover +OpenShell policy prover for checking whether a local candidate policy stays +within an operator-supplied maximum without connecting to a gateway. + # --- Python SDK sub-package --- %package -n python3-%{name} Summary: OpenShell Python SDK for agent execution and management @@ -87,6 +95,7 @@ grep -q 'version = "%{openshell_cargo_version}"' Cargo.toml || (echo "ERROR: Car %build test -x "${OPENSHELL_PREBUILT_BINARIES_DIR}/openshell" test -x "${OPENSHELL_PREBUILT_BINARIES_DIR}/openshell-gateway" +test -x "${OPENSHELL_PREBUILT_BINARIES_DIR}/openshell-prover" # Generate vendored crate manifest and license metadata. # cargo-vendor.txt is consumed by an RPM generator (from cargo-rpm-macros) @@ -103,6 +112,9 @@ pandoc -s -t man deploy/man/openshell-gateway.8.md -o openshell-gateway.8 # --- CLI binary --- install -Dpm 0755 "${OPENSHELL_PREBUILT_BINARIES_DIR}/%{name}" %{buildroot}%{_bindir}/%{name} +# --- Standalone policy prover --- +install -Dpm 0755 "${OPENSHELL_PREBUILT_BINARIES_DIR}/%{name}-prover" %{buildroot}%{_bindir}/%{name}-prover + # --- Gateway binary --- install -Dpm 0755 "${OPENSHELL_PREBUILT_BINARIES_DIR}/%{name}-gateway" %{buildroot}%{_bindir}/%{name}-gateway @@ -209,6 +221,9 @@ touch %{buildroot}%{python3_sitelib}/%{name}-%{openshell_python_version}.dist-in # Smoke-test the CLI binary %{buildroot}%{_bindir}/%{name} --version +# Smoke-test the standalone policy prover +%{buildroot}%{_bindir}/%{name}-prover --version + # Smoke-test the gateway binary %{buildroot}%{_bindir}/%{name}-gateway --version @@ -246,6 +261,12 @@ grep -q 'gateway.toml.default.v1' %{buildroot}%{_userunitdir}/%{name}-gateway.se %{_bindir}/%{name} %{_mandir}/man1/openshell.1* +%files prover +%license LICENSE +%license LICENSE.dependencies +%license cargo-vendor.txt +%{_bindir}/%{name}-prover + %files gateway %license LICENSE %license LICENSE.dependencies diff --git a/python/openshell/release_formula_test.py b/python/openshell/release_formula_test.py index 6848097451..671577d708 100644 --- a/python/openshell/release_formula_test.py +++ b/python/openshell/release_formula_test.py @@ -29,6 +29,10 @@ def test_generate_homebrew_formula_uses_tagged_macos_driver_asset_without_defaul "d" * 64 + " openshell-gateway-aarch64-apple-darwin.tar.gz\n", encoding="utf-8", ) + (release_dir / "openshell-prover-checksums-sha256.txt").write_text( + "e" * 64 + " openshell-prover-aarch64-apple-darwin.tar.gz\n", + encoding="utf-8", + ) repo_root = Path(__file__).resolve().parents[2] output = tmp_path / "openshell.rb" @@ -53,6 +57,14 @@ def test_generate_homebrew_formula_uses_tagged_macos_driver_asset_without_defaul "v0.0.10/openshell-driver-vm-aarch64-apple-darwin.tar.gz" ) in formula assert 'sha256 "' + "b" * 64 + '"' in formula + assert ( + "https://github.com/NVIDIA/OpenShell/releases/download/" + "v0.0.10/openshell-prover-aarch64-apple-darwin.tar.gz" + ) in formula + assert 'sha256 "' + "e" * 64 + '"' in formula + assert 'resource("openshell-prover").stage' in formula + assert 'bin.install "openshell-prover"' in formula + assert "#{bin}/openshell-prover --version" in formula assert "OPENSHELL_COMPUTE_DRIVER: " not in formula assert 'OPENSHELL_GATEWAY_CONFIG: "#{var}/openshell/gateway.toml"' not in formula assert "init-gateway-config.sh" not in formula diff --git a/tasks/scripts/package-deb-install.sh b/tasks/scripts/package-deb-install.sh index e20d409bbd..bd95a13e49 100755 --- a/tasks/scripts/package-deb-install.sh +++ b/tasks/scripts/package-deb-install.sh @@ -7,7 +7,7 @@ # or on the gateway-as-a-service flow. # # Steps: -# 1. cargo build --release the three binaries that go into the deb. +# 1. cargo build --release the four binaries that go into the deb. # 2. Run tasks/scripts/package-deb.sh against those binaries. # 3. sudo dpkg -i the resulting artifact. # 4. Start the packaged user gateway service and register it locally. @@ -57,11 +57,13 @@ echo "==> Building release binaries" cargo build --release \ -p openshell-cli \ -p openshell-gateway \ + -p openshell-prover-cli \ -p openshell-driver-vm echo "==> Building Debian package" OPENSHELL_CLI_BINARY="${repo_root}/target/release/openshell" \ OPENSHELL_GATEWAY_BINARY="${repo_root}/target/release/openshell-gateway" \ + OPENSHELL_PROVER_BINARY="${repo_root}/target/release/openshell-prover" \ OPENSHELL_DRIVER_VM_BINARY="${repo_root}/target/release/openshell-driver-vm" \ OPENSHELL_DEB_VERSION="$VERSION" \ OPENSHELL_DEB_ARCH="$ARCH" \ @@ -79,6 +81,7 @@ sudo dpkg -i "$deb_path" openshell --version openshell-gateway --version +openshell-prover --version echo "==> Starting user gateway service" systemctl --user daemon-reload diff --git a/tasks/scripts/package-deb.sh b/tasks/scripts/package-deb.sh index 3e20f6256e..c2492dd242 100755 --- a/tasks/scripts/package-deb.sh +++ b/tasks/scripts/package-deb.sh @@ -21,6 +21,7 @@ Build the openshell Debian package. Required environment: OPENSHELL_CLI_BINARY Path to openshell OPENSHELL_GATEWAY_BINARY Path to openshell-gateway + OPENSHELL_PROVER_BINARY Path to openshell-prover OPENSHELL_DRIVER_VM_BINARY Path to openshell-driver-vm OPENSHELL_DEB_VERSION Debian package version @@ -69,6 +70,7 @@ infer_deb_arch() { require_env OPENSHELL_CLI_BINARY require_env OPENSHELL_GATEWAY_BINARY +require_env OPENSHELL_PROVER_BINARY require_env OPENSHELL_DRIVER_VM_BINARY require_env OPENSHELL_DEB_VERSION @@ -110,6 +112,7 @@ mkdir -p "$pkgroot/DEBIAN" # Binaries. stage_binary "$OPENSHELL_CLI_BINARY" "$pkgroot/usr/bin/openshell" stage_binary "$OPENSHELL_GATEWAY_BINARY" "$pkgroot/usr/bin/openshell-gateway" +stage_binary "$OPENSHELL_PROVER_BINARY" "$pkgroot/usr/bin/openshell-prover" stage_binary "$OPENSHELL_DRIVER_VM_BINARY" "$pkgroot/usr/libexec/openshell/openshell-driver-vm" # Per-user systemd unit. Each user enables it via `systemctl --user`. diff --git a/tasks/scripts/release.py b/tasks/scripts/release.py index 3b0afe5ecd..78695824c2 100644 --- a/tasks/scripts/release.py +++ b/tasks/scripts/release.py @@ -37,6 +37,7 @@ class Versions: HOMEBREW_CLI_ASSET = f"openshell-{HOMEBREW_TARGET}.tar.gz" HOMEBREW_GATEWAY_ASSET = f"openshell-gateway-{HOMEBREW_TARGET}.tar.gz" HOMEBREW_DRIVER_VM_ASSET = f"openshell-driver-vm-{HOMEBREW_TARGET}.tar.gz" +HOMEBREW_PROVER_ASSET = f"openshell-prover-{HOMEBREW_TARGET}.tar.gz" GITHUB_RELEASE_DOWNLOADS = "https://github.com/NVIDIA/OpenShell/releases/download" LOCAL_GATEWAY_PORT = 17670 _SHA256_RE = re.compile(r"^[0-9a-fA-F]{64}$") @@ -310,6 +311,7 @@ def render_homebrew_formula( cli_sha256: str, gateway_sha256: str, driver_vm_sha256: str, + prover_sha256: str, ) -> str: if not _RELEASE_TAG_RE.fullmatch(release_tag): raise ValueError(f"release tag contains unsupported characters: {release_tag}") @@ -341,6 +343,11 @@ class Openshell < Formula sha256 "{driver_vm_sha256}" end + resource "openshell-prover" do + url "{_asset_url(release_tag, HOMEBREW_PROVER_ASSET)}" + sha256 "{prover_sha256}" + end + def install odie "OpenShell Homebrew formula currently supports macOS only" unless OS.mac? @@ -354,6 +361,10 @@ def install libexec.install "openshell-driver-vm" end + resource("openshell-prover").stage do + bin.install "openshell-prover" + end + (libexec/"openshell-gateway-homebrew-service").write <<~SH #!/bin/sh set -eu @@ -475,6 +486,7 @@ def caveats test do assert_match "openshell ", shell_output("#{{bin}}/openshell --version") + assert_match "openshell-prover ", shell_output("#{{bin}}/openshell-prover --version") end end """ @@ -488,8 +500,10 @@ def generate_homebrew_formula( ) -> None: checksums_path = release_dir / "openshell-checksums-sha256.txt" gateway_checksums_path = release_dir / "openshell-gateway-checksums-sha256.txt" + prover_checksums_path = release_dir / "openshell-prover-checksums-sha256.txt" checksums = _parse_sha256_file(checksums_path) gateway_checksums = _parse_sha256_file(gateway_checksums_path) + prover_checksums = _parse_sha256_file(prover_checksums_path) formula = render_homebrew_formula( release_tag=release_tag, @@ -504,6 +518,11 @@ def generate_homebrew_formula( HOMEBREW_DRIVER_VM_ASSET, checksums_path, ), + prover_sha256=_required_checksum( + prover_checksums, + HOMEBREW_PROVER_ASSET, + prover_checksums_path, + ), ) output.parent.mkdir(parents=True, exist_ok=True) output.write_text(formula, encoding="utf-8") diff --git a/tasks/scripts/test-install-sh.sh b/tasks/scripts/test-install-sh.sh index 5a20399b6a..b9d5f980ff 100755 --- a/tasks/scripts/test-install-sh.sh +++ b/tasks/scripts/test-install-sh.sh @@ -110,4 +110,15 @@ if [ "$(PLATFORM=linux local_gateway_endpoint)" != "https://127.0.0.1:17670" ]; exit 1 fi +cat >"${tmpdir}/checksums" <<'EOF' +aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa openshell-dev-x86_64.rpm +bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb openshell-gateway-dev-x86_64.rpm +cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc openshell-prover-dev-x86_64.rpm +EOF + +if [ "$(find_rpm_asset "${tmpdir}/checksums" x86_64 openshell-prover)" != "openshell-prover-dev-x86_64.rpm" ]; then + echo "FAIL: RPM prover package selection" >&2 + exit 1 +fi + echo "install.sh focused tests passed" diff --git a/tasks/scripts/test-packaging-assets.sh b/tasks/scripts/test-packaging-assets.sh index 9c9d3011fd..02ecdb007f 100755 --- a/tasks/scripts/test-packaging-assets.sh +++ b/tasks/scripts/test-packaging-assets.sh @@ -58,6 +58,9 @@ assert_contains \ "$spec" \ 'ExecStartPre=/usr/bin/openshell-gateway generate-certs --output-dir ${OPENSHELL_LOCAL_TLS_DIR} --server-san host.openshell.internal' assert_contains "$spec" 'ExecStartPre=/usr/bin/openshell-gateway config preflight' +assert_contains "$spec" '%package prover' +assert_contains "$spec" '%files prover' +assert_contains "$spec" '%{_bindir}/%{name}-prover' assert_not_contains "$spec" '%%S/openshell/tls' # Schema-v2 package startup wiring. @@ -95,12 +98,13 @@ if command -v dpkg-deb >/dev/null 2>&1; then package_work=$(mktemp -d "${TMPDIR:-/tmp}/openshell-package-assets.XXXXXX") trap 'rm -rf "$package_work"' EXIT mkdir -p "$package_work/bin" "$package_work/output" - for binary in openshell openshell-gateway openshell-driver-vm; do + for binary in openshell openshell-gateway openshell-prover openshell-driver-vm; do printf '#!/bin/sh\nexit 0\n' >"$package_work/bin/$binary" chmod +x "$package_work/bin/$binary" done OPENSHELL_CLI_BINARY="$package_work/bin/openshell" \ OPENSHELL_GATEWAY_BINARY="$package_work/bin/openshell-gateway" \ + OPENSHELL_PROVER_BINARY="$package_work/bin/openshell-prover" \ OPENSHELL_DRIVER_VM_BINARY="$package_work/bin/openshell-driver-vm" \ OPENSHELL_DEB_VERSION=0.0.0 \ OPENSHELL_DEB_ARCH=amd64 \ @@ -113,6 +117,11 @@ if command -v dpkg-deb >/dev/null 2>&1; then echo "FAIL: package-deb did not stage the current Debian service" >&2 exit 1 fi + if ! dpkg-deb --fsys-tarfile "$package_work/output/openshell_0.0.0_amd64.deb" \ + | tar -tf - | grep -x './usr/bin/openshell-prover' >/dev/null; then + echo "FAIL: package-deb did not stage openshell-prover" >&2 + exit 1 + fi else echo "SKIP: dpkg-deb unavailable; Debian artifact staging requires its assigned lane" fi From ae699e1a7cbef8b4656bc0035104c056b92c3549 Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Sat, 12 Sep 2026 02:04:42 +0000 Subject: [PATCH 11/12] docs(prover): clarify installation and check results Signed-off-by: Johnny Greco --- architecture/security-policy.md | 35 +++----------- crates/openshell-prover/README.md | 4 +- docs/reference/policy-prover.mdx | 78 ++++++++++++++++++++----------- 3 files changed, 59 insertions(+), 58 deletions(-) diff --git a/architecture/security-policy.md b/architecture/security-policy.md index ff002497f7..75b7ff86df 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -343,38 +343,15 @@ candidate policy with an operator-supplied local maximum. It establishes result. It does not fetch gateway state, compose provider rules, apply policy, or decide whether an in-boundary change is eligible for automatic approval. -The initial maximum-boundary model covers filesystem paths, L4 network -authority, and enforced REST method and path authority, including explicit REST -denies. Network containment covers runtime configurations both with and without -binary identity enforcement. Strict checks match grants and denies against the -executable and an ancestor identity, and the evidence identifies the identities -for an exceeding witness. Network binary selectors, endpoint host and path -selectors, and REST allow and deny method and path selectors must use ASCII -literals. This restriction applies to both inputs, including deny-only rules; -embedded NUL bytes in those fields are also unsupported. Other Unicode policy -text and filesystem paths are unaffected. ASCII wildcard selectors still cover -non-ASCII runtime values matched by the policy engine. -Recognized authority outside the reviewed model produces an unsupported result -rather than being silently ignored. -Environment-dependent authority also remains unsupported when the result -depends on context that is unavailable to the local command. This includes an -unresolved workdir, filesystem or binary containment that depends on image-specific -path resolution, and overlapping L4 and REST endpoints whose inspection selection -depends on the complete runtime endpoint set. Candidate and maximum paths use -the same sandbox namespace and mount interpretation; the checker does not -resolve them against the CLI host or verify kernel enforcement in a running -sandbox. Filesystem checks assume stable path resolution when enforcement rules -are created. They support matching paths, grant removal, write-to-read reduction, -and a maximum root grant. Other comparisons between paths remain unsupported; -lexical ancestry or distinctness alone cannot establish resolved ancestry or -distinctness. Adding access when the maximum grants none produces a counterexample. -If the solver produces a string that cannot be decoded and checked faithfully, -the command returns an inconclusive `invalid_witness` result instead of publishing -the value as counterexample evidence. +The initial model covers filesystem paths, L4 network authority, and enforced +REST method and path authority. It returns explicit unsupported or inconclusive +results when a sound decision depends on authority or runtime context outside +the model. The result records the model version and covered domains so callers +can bind a successful check to those semantics. This containment operation is separate from the proposal-risk queries below. See the [standalone policy prover documentation](../docs/reference/policy-prover.mdx) -for installation, command behavior, evidence, and exit codes. +for installation, command behavior, model limitations, evidence, and exit codes. ## What the proposal prover decides diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index b7bfe6dbe7..4944c21a7f 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -63,8 +63,8 @@ pub struct ExfilPath { } ``` -The gateway's `finding_delta` keys paths by `(category, binary, -host:port, category, method)` so that adding a new method on an +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). diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx index c881060a62..3cdf4c3b9b 100644 --- a/docs/reference/policy-prover.mdx +++ b/docs/reference/policy-prover.mdx @@ -18,35 +18,18 @@ operator-owned ceiling. It does not grant authority by itself. ## Install the Prover -Download the archive for your platform from the -[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases) page: - -| Platform | Archive | -|---|---| -| Linux x86_64 | `openshell-prover-x86_64-unknown-linux-musl.tar.gz` | -| Linux aarch64 | `openshell-prover-aarch64-unknown-linux-musl.tar.gz` | -| macOS Apple Silicon | `openshell-prover-aarch64-apple-darwin.tar.gz` | - -Download `openshell-prover-checksums-sha256.txt` from the same release. On -Linux, verify the selected archive before extracting it: +The standard OpenShell installer includes `openshell-prover`: ```shell -archive=openshell-prover-x86_64-unknown-linux-musl.tar.gz -grep " ${archive}$" openshell-prover-checksums-sha256.txt | sha256sum --check -tar -xzf "${archive}" -mkdir -p ~/.local/bin -install -m 0755 openshell-prover ~/.local/bin/openshell-prover +curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh +openshell-prover --version ``` -On macOS, use `shasum` for verification: - -```shell -archive=openshell-prover-aarch64-apple-darwin.tar.gz -grep " ${archive}$" openshell-prover-checksums-sha256.txt | shasum -a 256 --check -tar -xzf "${archive}" -mkdir -p ~/.local/bin -install -m 0755 openshell-prover ~/.local/bin/openshell-prover -``` +The prover remains independent of the gateway at runtime. If you only need the +standalone binary, use the artifacts listed in the +[Support Matrix](/reference/support-matrix#standalone-policy-prover). These +artifacts and `openshell-prover-checksums-sha256.txt` are attached to +[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases). The release archive includes the solver linkage required by the executable. It does not require the main `openshell` command, a gateway configuration, or @@ -54,7 +37,7 @@ a separate Z3 installation. ## Check a Policy Boundary -Create a maximum policy: +Create `maximum.yaml` with this maximum policy: ```yaml version: 1 @@ -66,7 +49,7 @@ filesystem_policy: - /tmp ``` -Create the fully composed candidate policy: +Create `candidate.yaml` with this contained candidate: ```yaml version: 1 @@ -84,6 +67,36 @@ openshell-prover check candidate.yaml --maximum maximum.yaml ``` A contained candidate prints `result: within_max` and exits with status `0`. +To see an exceeding result and its counterexample, replace `candidate.yaml` +with a policy that makes `/etc` writable even though the maximum grants only +read access: + +```yaml +version: 1 +filesystem_policy: + read_only: + - /usr + read_write: + - /tmp + - /etc +``` + +```shell +openshell-prover check candidate.yaml --maximum maximum.yaml +``` + +To check the current effective policy of an existing sandbox, export it without +display metadata: + +```shell +openshell sandbox get my-sandbox --policy-only > candidate.yaml +openshell-prover check candidate.yaml --maximum maximum.yaml +``` + +This export includes provider-contributed rules. For a proposed change that is +not active, supply the complete post-change effective policy. The standalone +prover does not compose a base policy with provider rules. + Use JSON when a script consumes the result: ```shell @@ -99,6 +112,17 @@ version. An exceeding result also includes a filesystem or network counterexample. Automation should use `result` and `reason_code` instead of parsing the human-readable explanation. +| Field | When populated | +|---|---| +| `counterexample` | An object for `exceeds_max`; otherwise `null`. | +| `reason_code` | A stable identifier for an emitted `error`, `unsupported`, or `inconclusive` result; otherwise `null`. | +| `reason` | A human-readable explanation paired with `reason_code`; otherwise `null`. | + +The stable reason codes are `invalid_input`, `unsupported_policy_shape`, +`unresolved_workdir`, `unresolved_binary_path`, +`unresolved_filesystem_path`, `solver_timeout`, `solver_unknown`, +`resource_limit`, `invalid_witness`, and `cancelled`. + The solver has a finite 10-second default budget. Set a different positive budget with an integer followed by `ms`, `s`, or `m`: From ad953f64ec51948ce324f825cd8699cc73a2db4a Mon Sep 17 00:00:00 2001 From: Johnny Greco Date: Sat, 12 Sep 2026 02:12:25 +0000 Subject: [PATCH 12/12] docs(build): describe prover distribution directly Signed-off-by: Johnny Greco --- architecture/build.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/architecture/build.md b/architecture/build.md index 3f9e8f8b3b..a85b228142 100644 --- a/architecture/build.md +++ b/architecture/build.md @@ -88,11 +88,10 @@ continue to opt in with `bundled-z3`. Release workflows build the standalone `openshell-prover` executable for Linux musl x86_64 and aarch64 and macOS Apple Silicon. The standard Debian, RPM, and -Homebrew installations include it, following the same package-managed pattern -as `openshell-gateway`. Releases also publish one standalone archive per target -plus a dedicated SHA-256 manifest. Before publication, target-native jobs -extract each archive, reject host Z3 or Nix store linkage, and run a real local -containment check. The standalone artifact therefore requires neither an +Homebrew installations include it. Releases also publish one standalone archive +per target plus a dedicated SHA-256 manifest. Before publication, target-native +jobs extract each archive, reject host Z3 or Nix store linkage, and run a real +local containment check. The standalone artifact therefore requires neither an OpenShell installation nor a separately installed Z3 runtime. ## Linux Runtime Environments