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/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/package-release-binaries.yml b/.github/workflows/package-release-binaries.yml index f1900f3c35..4b7007e4c2 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,109 @@ 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 + + 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 + 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..1ca128a1d4 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 @@ -244,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 }} @@ -264,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 }} @@ -326,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 @@ -340,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 @@ -410,6 +424,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: @@ -459,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/ @@ -607,11 +636,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..70a8152aa2 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] @@ -294,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 }} @@ -315,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 }} @@ -420,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 @@ -434,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 @@ -506,6 +523,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 +675,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/.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/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..a85b228142 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`. +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. 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 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..75b7ff86df 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -335,7 +335,25 @@ 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 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, model limitations, 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..55f8a54dc1 --- /dev/null +++ b/crates/openshell-prover-cli/src/main.rs @@ -0,0 +1,570 @@ +// 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>, +} + +#[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_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}" + ); + 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(), + } +} + +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}"))?; + } + 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..f973f2698b --- /dev/null +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -0,0 +1,470 @@ +// 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_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()); +} + +#[test] +fn exceeding_policy_returns_counterexample_and_one() { + let output = check_json("candidate-exceeds.yaml", "maximum-no-write.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 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 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!( + "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 directory = std::env::temp_dir().join(format!( + "openshell-prover-cancellation-{}", + std::process::id() + )); + 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(), + ) + .to_string(), + ) + .unwrap(); + + let mut child = Command::new(env!("CARGO_BIN_EXE_openshell-prover")) + .args([ + "check", + candidate.to_str().expect("UTF-8 temporary path"), + "--maximum", + maximum.to_str().expect("UTF-8 temporary path"), + "--output", + "json", + "--timeout", + "10s", + ]) + .stdout(Stdio::piped()) + .spawn() + .expect("start cancellable prover"); + // 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"); + 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)] +#[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 new file mode 100644 index 0000000000..308d88f1ba --- /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 + read_write: + - /tmp 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/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/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-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-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-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..4944c21a7f 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -8,6 +8,22 @@ attached credential set + a binary capability registry as a Z3 SMT model, then runs reachability queries to detect credentialed-reach and capability changes a reviewer should be aware of. +The crate also exposes an independent containment API for checking whether a +fully composed candidate policy stays within an operator-supplied maximum. The +`openshell-prover-cli` package wraps that API for local files. Containment and +the legacy proposal-risk queries answer different questions; gateway callers +continue to use the proposal-risk API until the managed-policy migration. + +The containment model accepts ASCII literals in network binary selectors, +endpoint host and path selectors, and REST allow and deny method and path +selectors. It returns `unsupported_policy_shape` when either policy uses a +non-ASCII literal in one of those fields. This boundary does not apply to +filesystem paths or unrelated policy text. Embedded NUL bytes in network +selector fields are also unsupported. ASCII wildcards are modeled over the +runtime match language and can therefore match non-ASCII runtime values. A +solver string that cannot be decoded and validated exactly produces +`invalid_witness` rather than counterexample evidence. + Used by the gateway to gate auto-approval of agent-authored policy proposals: any finding blocks auto-approval, an empty delta lets the chunk pass through (when the reviewer opts in via the @@ -47,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). @@ -107,10 +123,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..16d52a32ed --- /dev/null +++ b/crates/openshell-prover/src/containment.rs @@ -0,0 +1,2910 @@ +// 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::{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, Deserialize, PartialEq)] +struct FilesystemPolicy { + #[serde(default)] + include_workdir: bool, + #[serde(default)] + read_only: Vec, + #[serde(default)] + read_write: Vec, + #[serde(flatten)] + 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")] + _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, + UnresolvedFilesystemPath, + 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::UnresolvedFilesystemPath => "unresolved_filesystem_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], +} + +static DOMAINS: &[CheckDomain] = &[ + CheckDomain::Filesystem, + CheckDomain::NetworkL4, + CheckDomain::NetworkRest, +]; +fn check_scope() -> &'static CheckScope { + static SCOPE: CheckScope = CheckScope { + model_version: "maximum-boundary-v1", + policy_version: 1, + domains: DOMAINS, + }; + &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); + } + 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] { + 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, + } + 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) { + return unsupported( + ReasonCode::UnresolvedBinaryPath, + "network deny containment depends on image-specific exact binary symlink resolution" + .to_owned(), + ); + } + filesystem_result.unwrap_or(CheckResult::Within(WithinEvidence)) +} + +fn solve_network_mode( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, + binary_identity_required: bool, + started: Instant, + 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" + } 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); + 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)) { + 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)) + .filter(|counterexample| { + counterexample_satisfies_predicate(maximum, candidate, counterexample) + }) + .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 }) +} + +/// 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 { + 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)); + } + // 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])); + 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_string_exact(model, &action.layer)?; + let binary = if binary_identity_required { + let binary = model_string_exact(model, &action.binary)?; + if !is_canonical_runtime_binary_path(&binary) { + return None; + } + Some(binary) + } else { + None + }; + let ancestor_binary = if binary_identity_required { + let binary = model_string_exact(model, &action.ancestor_binary)?; + if !is_canonical_runtime_binary_path(&binary) { + return None; + } + Some(binary) + } else { + None + }; + let host = model_string_exact(model, &action.host)?; + 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_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; + } + (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, + }) +} + +/// 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()?; + // 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) +} + +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) +} + +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() + || matches!(byte, b'-' | b'_') + }) + && label.as_bytes().first().is_some_and(|byte| *byte != b'-') + && label.as_bytes().last().is_some_and(|byte| *byte != b'-') + }) +} + +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 has_ambiguous_candidate_binary_path( + maximum: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> 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, + &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) + }) + }) + }) + }) + }) +} + +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_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 + .iter() + .any(|other| endpoint_authority_equal(endpoint, other)) + }) && right.iter().all(|endpoint| { + left.iter() + .any(|other| endpoint_authority_equal(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 check_filesystem( + 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()); + + 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) +} + +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 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) + || !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 let Some(reason) = unsupported_network_literal(&endpoint.host) { + return unsupported(format!("{context} endpoint host {reason}")); + } + 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() + || (endpoint.port != 0 && !endpoint.ports.is_empty()) + { + return unsupported(format!("{context} has no unambiguous host and port")); + } + 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")); + } + 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 let Some(reason) = unsupported_network_literal(&rule.allow.method) { + return unsupported(format!("{context} REST allow method {reason}")); + } + 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 let Some(reason) = unsupported_network_literal(&rule.method) { + return unsupported(format!("{context} REST deny method {reason}")); + } + 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")); + } + } + } + } + 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 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, +) -> 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; + } + 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 { + 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(); + } + if separator == "/" { + return path_glob_regex(pattern); + } + let mut parts = Vec::new(); + let mut chars = pattern.chars().peekable(); + while let Some(character) = chars.next() { + if character == '*' && chars.peek() == Some(&'*') { + chars.next(); + 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 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 { + // 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(), + ]) +} + +#[cfg(test)] +mod tests { + use super::*; + 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, /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( + &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( + "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 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_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), + "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( + "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") + || (binary == "/usr/bin/python3" && ancestor == "/usr/bin/curl") + ) + ), + "{result:?}" + ); + } + + #[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", + ); + 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", + ); + assert!(!network_is_structurally_contained( + &maximum, &candidate, true + )); + } + + #[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\nfilesystem_policy: {}\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", + ); + let result = check_within_maximum(&maximum, &candidate, options()); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason_code() == ReasonCode::UnresolvedBinaryPath + ), + "{result:?}" + ); + } + + #[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 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( + "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, /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(_) + )); + 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"), + ("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 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, expected, "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) + ); + } + } + + #[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", + "/a/é/b", + "/a/汉/b", + "/a/e\u{301}/b", + "/a/😀/b", + ] { + 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}" + ); + } + } + } + + #[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:?}" + ); + } + } + } + + #[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/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..3eef1cbbfb --- /dev/null +++ b/crates/openshell-prover/tests/runtime_parity.rs @@ -0,0 +1,464 @@ +// 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, Counterexample, 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 { + 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": require_binary_identity }), + ); + + 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 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| { + 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 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#" +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/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/policy-prover.mdx b/docs/reference/policy-prover.mdx new file mode 100644 index 0000000000..3cdf4c3b9b --- /dev/null +++ b/docs/reference/policy-prover.mdx @@ -0,0 +1,208 @@ +--- +# 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 + +The standard OpenShell installer includes `openshell-prover`: + +```shell +curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh +openshell-prover --version +``` + +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 +a separate Z3 installation. + +## Check a Policy Boundary + +Create `maximum.yaml` with this maximum policy: + +```yaml +version: 1 +filesystem_policy: + read_only: + - /usr + - /etc + read_write: + - /tmp +``` + +Create `candidate.yaml` with this contained candidate: + +```yaml +version: 1 +filesystem_policy: + read_only: + - /usr + read_write: + - /tmp +``` + +Run the check: + +```shell +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 +openshell-prover check candidate.yaml \ + --maximum maximum.yaml \ + --output json +``` + +The JSON object includes the result, exit code, input paths, prover version, +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. + +| 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`: + +```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. + +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. 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 +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. +- 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. +- 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 +evidence. 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