diff --git a/.gitignore b/.gitignore index 32610f71..8d68bf14 100644 --- a/.gitignore +++ b/.gitignore @@ -197,3 +197,4 @@ architecture/plans .claude/settings.local.json.claude/worktrees/ .claude/worktrees/ rfc.md +.z3-trace diff --git a/Cargo.lock b/Cargo.lock index 852d97a0..e7be83f9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -431,6 +431,24 @@ dependencies = [ "sha2 0.10.9", ] +[[package]] +name = "bindgen" +version = "0.72.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "993776b509cfb49c750f11b8f07a46fa23e0a1386ffc01fb1e7d343efc387895" +dependencies = [ + "bitflags", + "cexpr", + "clang-sys", + "itertools 0.13.0", + "proc-macro2", + "quote", + "regex", + "rustc-hash", + "shlex", + "syn 2.0.117", +] + [[package]] name = "bitflags" version = "2.11.0" @@ -558,6 +576,15 @@ version = "1.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e748733b7cbc798e1434b6ac524f0c1ff2ab456fe201501e6497c8417a4fc33" +[[package]] +name = "bzip2" +version = "0.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3a53fac24f34a81bc9954b5d6cfce0c21e18ec6959f44f56e8e90e4bb7c346c" +dependencies = [ + "libbz2-rs-sys", +] + [[package]] name = "cassowary" version = "0.3.0" @@ -594,6 +621,15 @@ dependencies = [ "shlex", ] +[[package]] +name = "cexpr" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" +dependencies = [ + "nom", +] + [[package]] name = "cfg-if" version = "1.0.4" @@ -641,6 +677,17 @@ dependencies = [ "inout", ] +[[package]] +name = "clang-sys" +version = "1.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b023947811758c97c59bf9d1c188fd619ad4718dcaa767947df1cadb14f39f4" +dependencies = [ + "glob", + "libc", + "libloading", +] + [[package]] name = "clap" version = "4.6.0" @@ -761,6 +808,12 @@ version = "0.10.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a6ef517f0926dd24a1582492c791b6a4818a4d94e789a334894aa15b0d12f55c" +[[package]] +name = "constant_time_eq" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d52eff69cd5e647efe296129160853a42795992097e8af39800e1060caeea9b" + [[package]] name = "core-foundation" version = "0.10.1" @@ -1045,6 +1098,12 @@ version = "0.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "092966b41edc516079bdf31ec78a2e0588d1d0c08f78b91d8307215928642b2b" +[[package]] +name = "deflate64" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac6b926516df9c60bfa16e107b21086399f8285a44ca9711344b9e553c5146e2" + [[package]] name = "delegate" version = "0.13.5" @@ -1361,6 +1420,7 @@ checksum = "843fba2746e448b37e26a819579957415c8cef339bf08564fe8b7ddbd959573c" dependencies = [ "crc32fast", "miniz_oxide", + "zlib-rs", ] [[package]] @@ -1556,10 +1616,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555" dependencies = [ "cfg-if", + "js-sys", "libc", "r-efi 6.0.0", "wasip2", "wasip3", + "wasm-bindgen", ] [[package]] @@ -1578,6 +1640,12 @@ version = "0.32.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e629b9b98ef3dd8afe6ca2bd0f89306cec16d43d907889945bc5d6687f2f13c7" +[[package]] +name = "glob" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280" + [[package]] name = "globset" version = "0.4.18" @@ -2396,6 +2464,12 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" +[[package]] +name = "libbz2-rs-sys" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2c4a545a15244c7d945065b5d392b2d2d7f21526fba56ce51467b06ed445e8f7" + [[package]] name = "libc" version = "0.2.183" @@ -2468,6 +2542,16 @@ dependencies = [ "rand 0.9.2", ] +[[package]] +name = "libloading" +version = "0.8.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55" +dependencies = [ + "cfg-if", + "windows-link", +] + [[package]] name = "libm" version = "0.2.16" @@ -2555,6 +2639,15 @@ version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "112b39cec0b298b6c1999fee3e31427f74f676e4cb9879ed1a121b43661a4154" +[[package]] +name = "lzma-rust2" +version = "0.16.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47bb1e988e6fb779cf720ad431242d3f03167c1b3f2b1aae7f1a94b2495b36ae" +dependencies = [ + "sha2 0.10.9", +] + [[package]] name = "matchers" version = "0.2.0" @@ -2634,6 +2727,12 @@ version = "0.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6877bb514081ee2a7ff5ef9de3281f14a4dd4bceac4c09388074a6b5df8a139a" +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + [[package]] name = "miniz_oxide" version = "0.8.9" @@ -2695,6 +2794,16 @@ dependencies = [ "libc", ] +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + [[package]] name = "nu-ansi-term" version = "0.50.3" @@ -2704,6 +2813,20 @@ dependencies = [ "windows-sys 0.61.2", ] +[[package]] +name = "num" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23" +dependencies = [ + "num-bigint", + "num-complex", + "num-integer", + "num-iter", + "num-rational", + "num-traits", +] + [[package]] name = "num-bigint" version = "0.4.6" @@ -2732,6 +2855,15 @@ dependencies = [ "zeroize", ] +[[package]] +name = "num-complex" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495" +dependencies = [ + "num-traits", +] + [[package]] name = "num-conv" version = "0.2.0" @@ -2758,6 +2890,17 @@ dependencies = [ "num-traits", ] +[[package]] +name = "num-rational" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824" +dependencies = [ + "num-bigint", + "num-integer", + "num-traits", +] + [[package]] name = "num-traits" version = "0.2.19" @@ -2852,6 +2995,7 @@ dependencies = [ "openshell-bootstrap", "openshell-core", "openshell-policy", + "openshell-prover", "openshell-providers", "openshell-tui", "owo-colors", @@ -2915,6 +3059,21 @@ dependencies = [ "serde_yml", ] +[[package]] +name = "openshell-prover" +version = "0.0.0" +dependencies = [ + "miette", + "openshell-core", + "openshell-policy", + "owo-colors", + "serde", + "serde_yml", + "thiserror 2.0.18", + "tracing", + "z3", +] + [[package]] name = "openshell-providers" version = "0.0.0" @@ -3461,6 +3620,12 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" +[[package]] +name = "ppmd-rust" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "efca4c95a19a79d1c98f791f10aebd5c1363b473244630bb7dbde1dc98455a24" + [[package]] name = "ppv-lite86" version = "0.2.21" @@ -3830,7 +3995,9 @@ checksum = "eddd3ca559203180a307f12d114c268abf583f59b03cb906fd0b3ff8646c1147" dependencies = [ "base64 0.22.1", "bytes", + "futures-channel", "futures-core", + "futures-util", "http", "http-body", "http-body-util", @@ -5061,6 +5228,7 @@ checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c" dependencies = [ "deranged", "itoa", + "js-sys", "num-conv", "powerfmt", "serde_core", @@ -5483,6 +5651,12 @@ dependencies = [ "utf-8", ] +[[package]] +name = "typed-path" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e28f89b80c87b8fb0cf04ab448d5dd0dd0ade2f8891bae878de66a75a28600e" + [[package]] name = "typenum" version = "1.19.0" @@ -6358,6 +6532,31 @@ dependencies = [ "synstructure", ] +[[package]] +name = "z3" +version = "0.19.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "107cca65ed27d28b11f7c492298a51383333fd48ba6ebe49a432aba96162f678" +dependencies = [ + "log", + "num", + "z3-sys", +] + +[[package]] +name = "z3-sys" +version = "0.10.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c82b97329d02d87da6802ed9fda083f1b255d822ab13d5b1fb961196b58a69a1" +dependencies = [ + "bindgen", + "cmake", + "pkg-config", + "reqwest", + "serde_json", + "zip", +] + [[package]] name = "zerocopy" version = "0.8.42" @@ -6452,8 +6651,81 @@ dependencies = [ "syn 2.0.117", ] +[[package]] +name = "zip" +version = "8.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2726508a48f38dceb22b35ecbbd2430efe34ff05c62bd3285f965d7911b33464" +dependencies = [ + "aes", + "bzip2", + "constant_time_eq", + "crc32fast", + "deflate64", + "flate2", + "getrandom 0.4.2", + "hmac", + "indexmap 2.13.0", + "lzma-rust2", + "memchr", + "pbkdf2", + "ppmd-rust", + "sha1 0.10.6", + "time", + "typed-path", + "zeroize", + "zopfli", + "zstd", +] + +[[package]] +name = "zlib-rs" +version = "0.6.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3be3d40e40a133f9c916ee3f9f4fa2d9d63435b5fbe1bfc6d9dae0aa0ada1513" + [[package]] name = "zmij" version = "1.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" + +[[package]] +name = "zopfli" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f05cd8797d63865425ff89b5c4a48804f35ba0ce8d125800027ad6017d2b5249" +dependencies = [ + "bumpalo", + "crc32fast", + "log", + "simd-adler32", +] + +[[package]] +name = "zstd" +version = "0.13.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91ee311a569c327171651566e07972200e76fcfe2242a4fa446149a3881c08a" +dependencies = [ + "zstd-safe", +] + +[[package]] +name = "zstd-safe" +version = "7.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f49c4d5f0abb602a93fb8736af2a4f4dd9512e36f7f570d66e65ff867ed3b9d" +dependencies = [ + "zstd-sys", +] + +[[package]] +name = "zstd-sys" +version = "2.0.16+zstd.1.5.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "91e19ebc2adc8f83e43039e79776e3fda8ca919132d68a1fed6a5faca2683748" +dependencies = [ + "cc", + "pkg-config", +] diff --git a/Cargo.toml b/Cargo.toml index 08b699d4..a2b42f2f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -94,6 +94,9 @@ k8s-openapi = { version = "0.21.1", features = ["v1_26"] } # IDs uuid = { version = "1.10", features = ["v4"] } +# SMT solver +z3 = { version = "0.19", features = ["bundled"] } + [workspace.lints.rust] unsafe_code = "warn" rust_2018_idioms = { level = "warn", priority = -1 } diff --git a/crates/openshell-cli/Cargo.toml b/crates/openshell-cli/Cargo.toml index ef6d8779..a1c9a0b2 100644 --- a/crates/openshell-cli/Cargo.toml +++ b/crates/openshell-cli/Cargo.toml @@ -19,6 +19,7 @@ openshell-bootstrap = { path = "../openshell-bootstrap" } openshell-core = { path = "../openshell-core" } openshell-policy = { path = "../openshell-policy" } openshell-providers = { path = "../openshell-providers" } +openshell-prover = { path = "../openshell-prover" } openshell-tui = { path = "../openshell-tui" } serde = { workspace = true } serde_json = { workspace = true } diff --git a/crates/openshell-cli/src/main.rs b/crates/openshell-cli/src/main.rs index c8147645..1ae91956 100644 --- a/crates/openshell-cli/src/main.rs +++ b/crates/openshell-cli/src/main.rs @@ -1432,6 +1432,30 @@ enum PolicyCommands { #[arg(long)] yes: bool, }, + + /// Prove properties of a sandbox policy — or find counterexamples. + #[command(help_template = LEAF_HELP_TEMPLATE, next_help_heading = "FLAGS")] + Prove { + /// Path to OpenShell sandbox policy YAML. + #[arg(long, value_hint = ValueHint::FilePath)] + policy: String, + + /// Path to credential descriptor YAML. + #[arg(long, value_hint = ValueHint::FilePath)] + credentials: String, + + /// Path to capability registry directory (default: bundled). + #[arg(long, value_hint = ValueHint::DirPath)] + registry: Option, + + /// Path to accepted risks YAML. + #[arg(long, value_hint = ValueHint::FilePath)] + accepted_risks: Option, + + /// One-line-per-finding output (for demos and CI). + #[arg(long)] + compact: bool, + }, } #[derive(Subcommand, Debug)] @@ -1852,6 +1876,28 @@ async fn main() -> Result<()> { // ----------------------------------------------------------- // Top-level policy (was `sandbox policy`) // ----------------------------------------------------------- + Some(Commands::Policy { + command: + Some(PolicyCommands::Prove { + policy, + credentials, + registry, + accepted_risks, + compact, + }), + }) => { + // Prove runs locally — no gateway needed. + let exit_code = openshell_prover::prove( + &policy, + &credentials, + registry.as_deref(), + accepted_risks.as_deref(), + compact, + )?; + if exit_code != 0 { + std::process::exit(exit_code); + } + } Some(Commands::Policy { command: Some(policy_cmd), }) => { @@ -1922,6 +1968,7 @@ async fn main() -> Result<()> { } run::gateway_setting_delete(&ctx.endpoint, "policy", yes, &tls).await?; } + PolicyCommands::Prove { .. } => unreachable!(), } } diff --git a/crates/openshell-prover/Cargo.toml b/crates/openshell-prover/Cargo.toml new file mode 100644 index 00000000..ee8905c5 --- /dev/null +++ b/crates/openshell-prover/Cargo.toml @@ -0,0 +1,25 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +[package] +name = "openshell-prover" +description = "Formal policy verification for OpenShell sandboxes" +version.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true +repository.workspace = true + +[dependencies] +openshell-core = { path = "../openshell-core" } +openshell-policy = { path = "../openshell-policy" } +z3 = { workspace = true } +serde = { workspace = true } +serde_yml = { workspace = true } +miette = { workspace = true } +thiserror = { workspace = true } +tracing = { workspace = true } +owo-colors = { workspace = true } + +[lints] +workspace = true diff --git a/crates/openshell-prover/registry/apis/github.yaml b/crates/openshell-prover/registry/apis/github.yaml new file mode 100644 index 00000000..78fa15c9 --- /dev/null +++ b/crates/openshell-prover/registry/apis/github.yaml @@ -0,0 +1,65 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +api: github +host: api.github.com +port: 443 +credential_type: github-pat + +scope_capabilities: + repo: + - { method: GET, path: "/repos/**", action: read_repo } + - { method: GET, path: "/user/repos", action: list_repos } + - { method: POST, path: "/repos/*/issues", action: create_issue } + - { method: POST, path: "/repos/*/issues/*/comments", action: comment_issue } + - { method: POST, path: "/repos/*/pulls", action: create_pr } + - { method: PUT, path: "/repos/*/contents/**", action: write_file } + - { method: DELETE, path: "/repos/*/contents/**", action: delete_file } + - { method: DELETE, path: "/repos/*/*", action: delete_repo } + - { method: POST, path: "/repos/*/git/**", action: write_git_data } + - { method: POST, path: "/repos/*/forks", action: fork_repo } + - { method: PATCH, path: "/repos/*/*", action: update_repo } + - { method: POST, path: "/repos/*/releases", action: create_release } + - { method: POST, path: "/repos/*/dispatches", action: trigger_workflow } + "read:org": + - { method: GET, path: "/orgs/**", action: read_org } + - { method: GET, path: "/user/orgs", action: list_orgs } + "write:org": + - { method: GET, path: "/orgs/**", action: read_org } + - { method: POST, path: "/orgs/*/repos", action: create_org_repo } + - { method: PUT, path: "/orgs/*/memberships/**", action: manage_members } + gist: + - { method: GET, path: "/gists/**", action: read_gists } + - { method: POST, path: "/gists", action: create_gist } + - { method: PATCH, path: "/gists/*", action: update_gist } + - { method: DELETE, path: "/gists/*", action: delete_gist } + "admin:repo_hook": + - { method: GET, path: "/repos/*/hooks/**", action: read_hooks } + - { method: POST, path: "/repos/*/hooks", action: create_hook } + - { method: DELETE, path: "/repos/*/hooks/*", action: delete_hook } + +action_risk: + read_repo: low + list_repos: low + create_issue: medium + comment_issue: medium + create_pr: medium + write_file: high + delete_file: high + delete_repo: critical + write_git_data: high + fork_repo: medium + update_repo: high + create_release: high + trigger_workflow: critical + read_org: low + list_orgs: low + create_org_repo: high + manage_members: critical + read_gists: low + create_gist: medium + update_gist: medium + delete_gist: medium + read_hooks: low + create_hook: critical + delete_hook: high diff --git a/crates/openshell-prover/registry/binaries/claude.yaml b/crates/openshell-prover/registry/binaries/claude.yaml new file mode 100644 index 00000000..e9d1b1d3 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/claude.yaml @@ -0,0 +1,30 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/local/bin/claude +description: "Claude Code CLI — AI coding agent" +protocols: + - name: anthropic-api + transport: https + description: "Anthropic API calls for inference" + bypasses_l7: false + actions: + - { name: inference, type: write, description: "Send prompts and receive completions" } + - name: http-via-tools + transport: https + description: "Claude can make HTTP requests via tool use (Bash, WebFetch)" + bypasses_l7: false + actions: + - { name: get, type: read } + - { name: post, type: write } + - { name: put, type: write } +spawns: + - /usr/local/bin/node + - /usr/local/bin/python3.13 + - /usr/bin/git + - /usr/bin/curl + - /usr/bin/ssh + - /usr/bin/nc +can_exfiltrate: true +exfil_mechanism: "Can read files and send contents via tool use, API calls, or spawned subprocesses" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/curl.yaml b/crates/openshell-prover/registry/binaries/curl.yaml new file mode 100644 index 00000000..4cfadb8a --- /dev/null +++ b/crates/openshell-prover/registry/binaries/curl.yaml @@ -0,0 +1,20 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/curl +description: "Command-line HTTP client" +protocols: + - name: http + transport: https + description: "HTTP/HTTPS requests — can construct arbitrary method, path, headers, body" + bypasses_l7: false + actions: + - { name: get, type: read, description: "HTTP GET request" } + - { name: post, type: write, description: "HTTP POST with arbitrary body" } + - { name: put, type: write, description: "HTTP PUT with arbitrary body" } + - { name: delete, type: destructive, description: "HTTP DELETE request" } + - { name: upload, type: write, description: "File upload via multipart POST" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "POST/PUT file contents to any reachable endpoint, or encode in URL query parameters" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/gh.yaml b/crates/openshell-prover/registry/binaries/gh.yaml new file mode 100644 index 00000000..8ad7cb39 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/gh.yaml @@ -0,0 +1,19 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/gh +description: "GitHub CLI — REST API client for GitHub" +protocols: + - name: github-rest + transport: https + description: "GitHub REST API via gh cli — uses standard HTTP, subject to L7 inspection" + bypasses_l7: false + actions: + - { name: api_read, type: read, description: "GET requests to GitHub API" } + - { name: api_write, type: write, description: "POST/PUT/PATCH requests (create issues, PRs, etc.)" } + - { name: api_delete, type: destructive, description: "DELETE requests (delete repos, branches, etc.)" } +spawns: + - /usr/bin/git +can_exfiltrate: true +exfil_mechanism: "Create gists, issues, or PRs with file contents" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/git.yaml b/crates/openshell-prover/registry/binaries/git.yaml new file mode 100644 index 00000000..2c3480cb --- /dev/null +++ b/crates/openshell-prover/registry/binaries/git.yaml @@ -0,0 +1,28 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/git +description: "Distributed version control system" +protocols: + - name: git-smart-http + transport: https + description: "Git smart HTTP protocol over HTTPS CONNECT tunnel — not REST, bypasses L7 HTTP inspection" + bypasses_l7: true + actions: + - { name: clone, type: read, description: "Clone/fetch repository" } + - { name: push, type: write, description: "Push commits to remote" } + - { name: force_push, type: destructive, description: "Force push, rewriting remote history" } + - name: git-ssh + transport: ssh + description: "Git over SSH" + bypasses_l7: true + actions: + - { name: clone, type: read } + - { name: push, type: write } + - { name: force_push, type: destructive } +spawns: + - /usr/lib/git-core/git-remote-https + - /usr/bin/ssh +can_exfiltrate: true +exfil_mechanism: "Commit data to repo and push, or encode in branch/tag names" +can_construct_http: false diff --git a/crates/openshell-prover/registry/binaries/nc.yaml b/crates/openshell-prover/registry/binaries/nc.yaml new file mode 100644 index 00000000..8f98d763 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/nc.yaml @@ -0,0 +1,18 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/nc +description: "Netcat — arbitrary TCP/UDP connections" +protocols: + - name: raw-tcp + transport: tcp + description: "Raw TCP connection — can send/receive arbitrary data" + bypasses_l7: true + actions: + - { name: connect, type: read, description: "Establish TCP connection" } + - { name: send, type: write, description: "Send arbitrary data over TCP" } + - { name: listen, type: read, description: "Listen for incoming connections" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "Stream arbitrary data over raw TCP connection" +can_construct_http: false diff --git a/crates/openshell-prover/registry/binaries/node.yaml b/crates/openshell-prover/registry/binaries/node.yaml new file mode 100644 index 00000000..cfa83f2b --- /dev/null +++ b/crates/openshell-prover/registry/binaries/node.yaml @@ -0,0 +1,21 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/local/bin/node +description: "Node.js runtime — general-purpose JavaScript runtime" +protocols: + - name: http-programmatic + transport: https + description: "Node can construct arbitrary HTTP requests via fetch, axios, http module" + bypasses_l7: false + actions: + - { name: get, type: read } + - { name: post, type: write } + - { name: put, type: write } + - { name: delete, type: destructive } +spawns: + - /usr/bin/curl + - /usr/bin/git +can_exfiltrate: true +exfil_mechanism: "Construct arbitrary HTTP requests, spawn subprocesses" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/python3.yaml b/crates/openshell-prover/registry/binaries/python3.yaml new file mode 100644 index 00000000..3cdf9cd3 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/python3.yaml @@ -0,0 +1,24 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/local/bin/python3.13 +description: "Python interpreter — general-purpose runtime" +protocols: + - name: http-programmatic + transport: https + description: "Python can construct arbitrary HTTP requests via urllib, httpx, requests" + bypasses_l7: false + actions: + - { name: get, type: read } + - { name: post, type: write } + - { name: put, type: write } + - { name: delete, type: destructive } +spawns: + - /usr/bin/curl + - /usr/bin/git + - /usr/bin/ssh + - /usr/bin/nc + - /usr/bin/wget +can_exfiltrate: true +exfil_mechanism: "Construct arbitrary HTTP requests, write to files, spawn subprocesses" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/ssh.yaml b/crates/openshell-prover/registry/binaries/ssh.yaml new file mode 100644 index 00000000..b53065d8 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/ssh.yaml @@ -0,0 +1,18 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/ssh +description: "OpenSSH client" +protocols: + - name: ssh + transport: ssh + description: "SSH protocol — encrypted tunnel, can forward ports and transfer files" + bypasses_l7: true + actions: + - { name: connect, type: read, description: "SSH shell connection" } + - { name: tunnel, type: write, description: "Port forwarding / tunnel" } + - { name: scp, type: write, description: "File transfer via SCP" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "SCP files or pipe data through SSH tunnel" +can_construct_http: false diff --git a/crates/openshell-prover/registry/binaries/wget.yaml b/crates/openshell-prover/registry/binaries/wget.yaml new file mode 100644 index 00000000..0741998b --- /dev/null +++ b/crates/openshell-prover/registry/binaries/wget.yaml @@ -0,0 +1,17 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/wget +description: "Non-interactive network downloader" +protocols: + - name: http + transport: https + description: "HTTP/HTTPS downloads — can also POST with --post-data" + bypasses_l7: false + actions: + - { name: download, type: read } + - { name: post, type: write, description: "POST via --post-data or --post-file" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "POST file contents via --post-file to any reachable endpoint" +can_construct_http: true diff --git a/crates/openshell-prover/src/accepted_risks.rs b/crates/openshell-prover/src/accepted_risks.rs new file mode 100644 index 00000000..61aa025b --- /dev/null +++ b/crates/openshell-prover/src/accepted_risks.rs @@ -0,0 +1,168 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Load and match accepted risk annotations against findings. + +use std::path::Path; + +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +use crate::finding::{Finding, FindingPath}; + +// --------------------------------------------------------------------------- +// Serde types +// --------------------------------------------------------------------------- + +#[derive(Debug, Deserialize)] +struct AcceptedRisksFile { + #[serde(default)] + accepted_risks: Vec, +} + +#[derive(Debug, Deserialize)] +struct AcceptedRiskDef { + #[serde(default)] + query: String, + #[serde(default)] + reason: String, + #[serde(default)] + accepted_by: String, + #[serde(default)] + binary: String, + #[serde(default)] + endpoint: String, +} + +// --------------------------------------------------------------------------- +// Public types +// --------------------------------------------------------------------------- + +/// An explicitly accepted risk annotation. +#[derive(Debug, Clone)] +pub struct AcceptedRisk { + pub query: String, + pub reason: String, + pub accepted_by: String, + pub binary: String, + pub endpoint: String, +} + +// --------------------------------------------------------------------------- +// Loading +// --------------------------------------------------------------------------- + +/// Load accepted risks from a YAML file. +pub fn load_accepted_risks(path: &Path) -> Result> { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading accepted risks {}", path.display()))?; + let raw: AcceptedRisksFile = serde_yml::from_str(&contents) + .into_diagnostic() + .wrap_err("parsing accepted risks YAML")?; + + Ok(raw + .accepted_risks + .into_iter() + .map(|r| AcceptedRisk { + query: r.query, + reason: r.reason, + accepted_by: r.accepted_by, + binary: r.binary, + endpoint: r.endpoint, + }) + .collect()) +} + +// --------------------------------------------------------------------------- +// Matching +// --------------------------------------------------------------------------- + +/// Check if a single finding path matches an accepted risk. +fn path_matches_risk(path: &FindingPath, risk: &AcceptedRisk) -> bool { + if !risk.binary.is_empty() { + let path_binary = match path { + FindingPath::Exfil(p) => &p.binary, + FindingPath::WriteBypass(p) => &p.binary, + }; + if path_binary != &risk.binary { + return false; + } + } + if !risk.endpoint.is_empty() { + let endpoint_host = match path { + FindingPath::Exfil(p) => &p.endpoint_host, + FindingPath::WriteBypass(p) => &p.endpoint_host, + }; + if endpoint_host != &risk.endpoint { + return false; + } + } + true +} + +/// Mark findings as accepted where they match accepted risk annotations. +/// +/// A finding is accepted if **all** of its paths match at least one accepted +/// risk entry for that query. If only some paths match, the finding stays +/// active with the unmatched paths. +pub fn apply_accepted_risks(findings: Vec, accepted: &[AcceptedRisk]) -> Vec { + if accepted.is_empty() { + return findings; + } + + let mut result = Vec::new(); + for finding in findings { + let matching_risks: Vec<&AcceptedRisk> = accepted + .iter() + .filter(|r| r.query == finding.query) + .collect(); + + if matching_risks.is_empty() { + result.push(finding); + continue; + } + + if finding.paths.is_empty() { + // Pathless finding — accept if query matches. + result.push(Finding { + accepted: true, + accepted_reason: matching_risks[0].reason.clone(), + ..finding + }); + continue; + } + + let mut unmatched_paths = Vec::new(); + let mut matched_reason = String::new(); + for path in &finding.paths { + let mut path_accepted = false; + for risk in &matching_risks { + if path_matches_risk(path, risk) { + path_accepted = true; + matched_reason.clone_from(&risk.reason); + break; + } + } + if !path_accepted { + unmatched_paths.push(path.clone()); + } + } + + if unmatched_paths.is_empty() { + result.push(Finding { + accepted: true, + accepted_reason: matched_reason, + ..finding + }); + } else if unmatched_paths.len() < finding.paths.len() { + result.push(Finding { + paths: unmatched_paths, + ..finding + }); + } else { + result.push(finding); + } + } + result +} diff --git a/crates/openshell-prover/src/credentials.rs b/crates/openshell-prover/src/credentials.rs new file mode 100644 index 00000000..ca068bca --- /dev/null +++ b/crates/openshell-prover/src/credentials.rs @@ -0,0 +1,239 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Credential descriptors and API capability registries. + +use std::collections::HashMap; +use std::path::Path; + +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +// --------------------------------------------------------------------------- +// Serde types +// --------------------------------------------------------------------------- + +#[derive(Debug, Deserialize)] +struct CredentialsFile { + #[serde(default)] + credentials: Vec, +} + +#[derive(Debug, Deserialize)] +struct CredentialDef { + #[serde(default)] + name: String, + #[serde(default, rename = "type")] + cred_type: String, + #[serde(default)] + scopes: Vec, + #[serde(default)] + injected_via: String, + #[serde(default)] + target_hosts: Vec, +} + +#[derive(Debug, Deserialize)] +struct ApiRegistryDef { + #[serde(default)] + api: String, + #[serde(default)] + host: String, + #[serde(default)] + port: u32, + #[serde(default)] + credential_type: String, + #[serde(default)] + scope_capabilities: HashMap>, + #[serde(default)] + action_risk: HashMap, +} + +#[derive(Debug, Deserialize)] +struct ApiActionDef { + #[serde(default)] + method: String, + #[serde(default)] + path: String, + #[serde(default)] + action: String, +} + +// --------------------------------------------------------------------------- +// Public types +// --------------------------------------------------------------------------- + +/// A credential injected into the sandbox. +#[derive(Debug, Clone)] +pub struct Credential { + pub name: String, + pub cred_type: String, + pub scopes: Vec, + pub injected_via: String, + pub target_hosts: Vec, +} + +/// A single API action (HTTP method + path + semantic name). +#[derive(Debug, Clone)] +pub struct ApiAction { + pub method: String, + pub path: String, + pub action: String, +} + +/// Capability registry for an API (e.g., GitHub REST API). +#[derive(Debug, Clone)] +pub struct ApiCapability { + pub api: String, + pub host: String, + pub port: u32, + pub credential_type: String, + pub scope_capabilities: HashMap>, + pub action_risk: HashMap, +} + +impl ApiCapability { + /// All actions enabled by the given scopes. + pub fn actions_for_scopes(&self, scopes: &[String]) -> Vec<&ApiAction> { + let mut result = Vec::new(); + for scope in scopes { + if let Some(actions) = self.scope_capabilities.get(scope) { + result.extend(actions.iter()); + } + } + result + } + + /// Write actions (POST, PUT, PATCH, DELETE) enabled by the given scopes. + pub fn write_actions_for_scopes(&self, scopes: &[String]) -> Vec<&ApiAction> { + self.actions_for_scopes(scopes) + .into_iter() + .filter(|a| { + let m = a.method.to_uppercase(); + m == "POST" || m == "PUT" || m == "PATCH" || m == "DELETE" + }) + .collect() + } + + /// Destructive actions (high or critical risk) enabled by the given scopes. + pub fn destructive_actions_for_scopes(&self, scopes: &[String]) -> Vec<&ApiAction> { + self.actions_for_scopes(scopes) + .into_iter() + .filter(|a| { + let risk = self.action_risk.get(&a.action).map(String::as_str); + matches!(risk, Some("high" | "critical")) + }) + .collect() + } +} + +/// Combined set of credentials and API registries. +#[derive(Debug, Clone, Default)] +pub struct CredentialSet { + pub credentials: Vec, + pub api_registries: HashMap, +} + +impl CredentialSet { + /// Credentials that target a given host. + pub fn credentials_for_host(&self, host: &str) -> Vec<&Credential> { + self.credentials + .iter() + .filter(|c| c.target_hosts.iter().any(|h| h == host)) + .collect() + } + + /// API capability registry for a given host. + pub fn api_for_host(&self, host: &str) -> Option<&ApiCapability> { + self.api_registries.values().find(|api| api.host == host) + } +} + +// --------------------------------------------------------------------------- +// Loading +// --------------------------------------------------------------------------- + +/// Load credential descriptors from a YAML file. +pub fn load_credentials(path: &Path) -> Result> { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading credentials file {}", path.display()))?; + let raw: CredentialsFile = serde_yml::from_str(&contents) + .into_diagnostic() + .wrap_err("parsing credentials YAML")?; + + Ok(raw + .credentials + .into_iter() + .map(|c| Credential { + name: c.name, + cred_type: c.cred_type, + scopes: c.scopes, + injected_via: c.injected_via, + target_hosts: c.target_hosts, + }) + .collect()) +} + +/// Load an API capability registry from a YAML file. +fn load_api_registry(path: &Path) -> Result { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading API registry {}", path.display()))?; + let raw: ApiRegistryDef = serde_yml::from_str(&contents) + .into_diagnostic() + .wrap_err_with(|| format!("parsing API registry {}", path.display()))?; + + let scope_capabilities = raw + .scope_capabilities + .into_iter() + .map(|(scope, actions)| { + let actions = actions + .into_iter() + .map(|a| ApiAction { + method: a.method, + path: a.path, + action: a.action, + }) + .collect(); + (scope, actions) + }) + .collect(); + + Ok(ApiCapability { + api: raw.api, + host: raw.host, + port: raw.port, + credential_type: raw.credential_type, + scope_capabilities, + action_risk: raw.action_risk, + }) +} + +/// Load credentials and all API registries from the registry directory. +/// +/// Expects `{registry_dir}/apis/*.yaml`. +pub fn load_credential_set(credentials_path: &Path, registry_dir: &Path) -> Result { + let creds = load_credentials(credentials_path)?; + + let mut api_registries = HashMap::new(); + let apis_dir = registry_dir.join("apis"); + if apis_dir.is_dir() { + let entries = std::fs::read_dir(&apis_dir) + .into_diagnostic() + .wrap_err_with(|| format!("reading directory {}", apis_dir.display()))?; + for entry in entries { + let entry = entry.into_diagnostic()?; + let path = entry.path(); + if path.extension().is_some_and(|ext| ext == "yaml") { + let api = load_api_registry(&path)?; + api_registries.insert(api.api.clone(), api); + } + } + } + + Ok(CredentialSet { + credentials: creds, + api_registries, + }) +} diff --git a/crates/openshell-prover/src/finding.rs b/crates/openshell-prover/src/finding.rs new file mode 100644 index 00000000..e42d9538 --- /dev/null +++ b/crates/openshell-prover/src/finding.rs @@ -0,0 +1,67 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Finding types emitted by verification queries. + +use std::fmt; + +/// Severity level for a finding. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum RiskLevel { + High, + Critical, +} + +impl fmt::Display for RiskLevel { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::High => write!(f, "HIGH"), + Self::Critical => write!(f, "CRITICAL"), + } + } +} + +/// A concrete path through which data can be exfiltrated. +#[derive(Debug, Clone)] +pub struct ExfilPath { + pub binary: String, + pub endpoint_host: String, + pub endpoint_port: u32, + pub mechanism: String, + pub policy_name: String, + /// One of `"l4_only"`, `"l7_allows_write"`, `"l7_bypassed"`. + pub l7_status: String, +} + +/// A path that allows writing despite read-only intent. +#[derive(Debug, Clone)] +pub struct WriteBypassPath { + pub binary: String, + pub endpoint_host: String, + pub endpoint_port: u32, + pub policy_name: String, + pub policy_intent: String, + /// One of `"l4_only"`, `"l7_bypass_protocol"`, `"credential_write_scope"`. + pub bypass_reason: String, + pub credential_actions: Vec, +} + +/// Concrete evidence attached to a [`Finding`]. +#[derive(Debug, Clone)] +pub enum FindingPath { + Exfil(ExfilPath), + WriteBypass(WriteBypassPath), +} + +/// A single verification finding. +#[derive(Debug, Clone)] +pub struct Finding { + pub query: String, + pub title: String, + pub description: String, + pub risk: RiskLevel, + pub paths: Vec, + pub remediation: Vec, + pub accepted: bool, + pub accepted_reason: String, +} diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs new file mode 100644 index 00000000..6a9acaf1 --- /dev/null +++ b/crates/openshell-prover/src/lib.rs @@ -0,0 +1,229 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Formal policy verification for OpenShell sandboxes. +//! +//! Encodes sandbox policies, binary capabilities, and credential scopes as Z3 +//! SMT constraints, then checks reachability queries to detect data exfiltration +//! paths and write-bypass violations. + +pub mod accepted_risks; +pub mod credentials; +pub mod finding; +pub mod model; +pub mod policy; +pub mod queries; +pub mod registry; +pub mod report; + +use std::path::Path; + +use miette::Result; + +use accepted_risks::{apply_accepted_risks, load_accepted_risks}; +use credentials::load_credential_set; +use model::build_model; +use policy::parse_policy; +use queries::run_all_queries; +use registry::load_binary_registry; +use report::{render_compact, render_report}; + +/// Run the prover end-to-end and return an exit code. +/// +/// - `0` — pass (no critical/high findings, or all accepted) +/// - `1` — fail (critical or high findings present) +/// - `2` — input error +pub fn prove( + policy_path: &str, + credentials_path: &str, + registry_dir: Option<&str>, + accepted_risks_path: Option<&str>, + compact: bool, +) -> Result { + // Determine registry directory. + let registry = registry_dir + .map(Path::new) + .map(std::borrow::Cow::Borrowed) + .unwrap_or_else(|| { + // Default: look for registry/ next to the prover crate, then CWD. + let crate_registry = Path::new(env!("CARGO_MANIFEST_DIR")).join("registry"); + if crate_registry.is_dir() { + std::borrow::Cow::Owned(crate_registry) + } else { + std::borrow::Cow::Owned( + std::env::current_dir().unwrap_or_default().join("registry"), + ) + } + }); + + let policy = parse_policy(Path::new(policy_path))?; + + let credential_set = load_credential_set(Path::new(credentials_path), ®istry)?; + + let binary_registry = load_binary_registry(®istry)?; + + // Build Z3 model and run queries. + let z3_model = build_model(policy, credential_set, binary_registry); + let mut findings = run_all_queries(&z3_model); + + // Apply accepted risks. + if let Some(ar_path) = accepted_risks_path { + let accepted = load_accepted_risks(Path::new(ar_path))?; + findings = apply_accepted_risks(findings, &accepted); + } + + // Render. + let exit_code = if compact { + render_compact(&findings, policy_path, credentials_path) + } else { + render_report(&findings, policy_path, credentials_path) + }; + + Ok(exit_code) +} + +// =========================================================================== +// Tests +// =========================================================================== + +#[cfg(test)] +mod tests { + use super::*; + use std::path::PathBuf; + + fn testdata_dir() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("testdata") + } + + fn registry_dir() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("registry") + } + + // 1. Parse testdata/policy.yaml, verify structure. + #[test] + fn test_parse_policy() { + let path = testdata_dir().join("policy.yaml"); + let model = policy::parse_policy(&path).expect("failed to parse policy"); + assert_eq!(model.version, 1); + assert!(model.network_policies.contains_key("github_api")); + let rule = &model.network_policies["github_api"]; + assert_eq!(rule.name, "github-api"); + assert_eq!(rule.endpoints.len(), 2); + assert!(rule.binaries.len() >= 4); + } + + // 2. Verify readable_paths. + #[test] + fn test_filesystem_policy() { + let path = testdata_dir().join("policy.yaml"); + let model = policy::parse_policy(&path).expect("failed to parse policy"); + let readable = model.filesystem_policy.readable_paths(); + // read_only has 7 entries, read_write has 3 (/sandbox, /tmp, /dev/null). + // include_workdir=true but /sandbox is already in read_write, so no dup. + assert!(readable.contains(&"/usr".to_owned())); + assert!(readable.contains(&"/sandbox".to_owned())); + assert!(readable.contains(&"/tmp".to_owned())); + } + + // 3. Workdir included by default. + #[test] + fn test_include_workdir_default() { + let yaml = r#" +version: 1 +filesystem_policy: + read_only: + - /usr +"#; + let model = policy::parse_policy_str(yaml).expect("parse"); + let readable = model.filesystem_policy.readable_paths(); + assert!(readable.contains(&"/sandbox".to_owned())); + } + + // 4. Workdir excluded when include_workdir: false. + #[test] + fn test_include_workdir_false() { + let yaml = r#" +version: 1 +filesystem_policy: + include_workdir: false + read_only: + - /usr +"#; + let model = policy::parse_policy_str(yaml).expect("parse"); + let readable = model.filesystem_policy.readable_paths(); + assert!(!readable.contains(&"/sandbox".to_owned())); + } + + // 5. No duplicate when workdir already in read_write. + #[test] + fn test_include_workdir_no_duplicate() { + let yaml = r#" +version: 1 +filesystem_policy: + include_workdir: true + read_write: + - /sandbox + - /tmp +"#; + let model = policy::parse_policy_str(yaml).expect("parse"); + let readable = model.filesystem_policy.readable_paths(); + let sandbox_count = readable.iter().filter(|p| *p == "/sandbox").count(); + assert_eq!(sandbox_count, 1); + } + + // 6. End-to-end: git push bypass findings detected. + #[test] + fn test_git_push_bypass_findings() { + let policy_path = testdata_dir().join("policy.yaml"); + let creds_path = testdata_dir().join("credentials.yaml"); + let reg_dir = registry_dir(); + + let pol = policy::parse_policy(&policy_path).expect("parse policy"); + let cred_set = credentials::load_credential_set(&creds_path, ®_dir).expect("load creds"); + let bin_reg = registry::load_binary_registry(®_dir).expect("load registry"); + + let z3_model = model::build_model(pol, cred_set, bin_reg); + let findings = queries::run_all_queries(&z3_model); + + // Should have findings from both query types. + let query_types: std::collections::HashSet<&str> = + findings.iter().map(|f| f.query.as_str()).collect(); + assert!( + query_types.contains("data_exfiltration"), + "expected data_exfiltration finding" + ); + assert!( + query_types.contains("write_bypass"), + "expected write_bypass finding" + ); + + // At least one critical or high finding. + assert!( + findings.iter().any(|f| matches!( + f.risk, + finding::RiskLevel::Critical | finding::RiskLevel::High + )), + "expected at least one critical/high finding" + ); + } + + // 7. Empty policy produces no findings. + #[test] + fn test_empty_policy_no_findings() { + let policy_path = testdata_dir().join("empty-policy.yaml"); + let creds_path = testdata_dir().join("credentials.yaml"); + let reg_dir = registry_dir(); + + let pol = policy::parse_policy(&policy_path).expect("parse policy"); + let cred_set = credentials::load_credential_set(&creds_path, ®_dir).expect("load creds"); + let bin_reg = registry::load_binary_registry(®_dir).expect("load registry"); + + let z3_model = model::build_model(pol, cred_set, bin_reg); + let findings = queries::run_all_queries(&z3_model); + + assert!( + findings.is_empty(), + "deny-all policy should produce no findings, got: {findings:?}" + ); + } +} diff --git a/crates/openshell-prover/src/model.rs b/crates/openshell-prover/src/model.rs new file mode 100644 index 00000000..9c5f574e --- /dev/null +++ b/crates/openshell-prover/src/model.rs @@ -0,0 +1,393 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Z3 constraint model encoding policy, credentials, and binary capabilities. + +use std::collections::{HashMap, HashSet}; + +use z3::ast::Bool; +use z3::{Context, SatResult, Solver}; + +use crate::credentials::CredentialSet; +use crate::policy::{PolicyModel, WRITE_METHODS}; +use crate::registry::BinaryRegistry; + +/// Unique identifier for a network endpoint in the model. +#[derive(Debug, Clone, Hash, PartialEq, Eq)] +pub struct EndpointId { + pub policy_name: String, + pub host: String, + pub port: u32, +} + +impl EndpointId { + /// Stable string key used for Z3 variable naming. + pub fn key(&self) -> String { + format!("{}:{}:{}", self.policy_name, self.host, self.port) + } +} + +/// Z3-backed reachability model for an OpenShell sandbox policy. +pub struct ReachabilityModel { + pub policy: PolicyModel, + pub credentials: CredentialSet, + pub binary_registry: BinaryRegistry, + + // Indexed facts + pub endpoints: Vec, + pub binary_paths: Vec, + + // Z3 solver + solver: Solver, + + // Boolean variable maps + policy_allows: HashMap, + l7_enforced: HashMap, + l7_allows_write: HashMap, + binary_bypasses_l7: HashMap, + binary_can_write: HashMap, + binary_can_exfil: HashMap, + binary_can_construct_http: HashMap, + credential_has_write: HashMap, + #[allow(dead_code)] + credential_has_destructive: HashMap, + #[allow(dead_code)] + filesystem_readable: HashMap, +} + +impl ReachabilityModel { + /// Build a new reachability model from the given inputs. + pub fn new( + policy: PolicyModel, + credentials: CredentialSet, + binary_registry: BinaryRegistry, + ) -> Self { + let solver = Solver::new(); + let mut model = Self { + policy, + credentials, + binary_registry, + endpoints: Vec::new(), + binary_paths: Vec::new(), + solver, + policy_allows: HashMap::new(), + l7_enforced: HashMap::new(), + l7_allows_write: HashMap::new(), + binary_bypasses_l7: HashMap::new(), + binary_can_write: HashMap::new(), + binary_can_exfil: HashMap::new(), + binary_can_construct_http: HashMap::new(), + credential_has_write: HashMap::new(), + credential_has_destructive: HashMap::new(), + filesystem_readable: HashMap::new(), + }; + model.build(); + model + } + + fn build(&mut self) { + self.index_endpoints(); + self.index_binaries(); + self.encode_policy_allows(); + self.encode_l7_enforcement(); + self.encode_binary_capabilities(); + self.encode_credentials(); + self.encode_filesystem(); + } + + fn index_endpoints(&mut self) { + for (policy_name, rule) in &self.policy.network_policies { + for ep in &rule.endpoints { + for port in ep.effective_ports() { + self.endpoints.push(EndpointId { + policy_name: policy_name.clone(), + host: ep.host.clone(), + port, + }); + } + } + } + } + + fn index_binaries(&mut self) { + let mut seen = HashSet::new(); + for rule in self.policy.network_policies.values() { + for b in &rule.binaries { + if seen.insert(b.path.clone()) { + self.binary_paths.push(b.path.clone()); + } + } + } + } + + fn encode_policy_allows(&mut self) { + for (policy_name, rule) in &self.policy.network_policies { + for ep in &rule.endpoints { + for port in ep.effective_ports() { + let eid = EndpointId { + policy_name: policy_name.clone(), + host: ep.host.clone(), + port, + }; + for b in &rule.binaries { + let key = format!("{}:{}", b.path, eid.key()); + let var = Bool::new_const(format!("policy_allows_{key}")); + self.solver.assert(&var); + self.policy_allows.insert(key, var); + } + } + } + } + } + + fn encode_l7_enforcement(&mut self) { + for (policy_name, rule) in &self.policy.network_policies { + for ep in &rule.endpoints { + for port in ep.effective_ports() { + let eid = EndpointId { + policy_name: policy_name.clone(), + host: ep.host.clone(), + port, + }; + let ek = eid.key(); + + // L7 enforced? + let l7_var = Bool::new_const(format!("l7_enforced_{ek}")); + if ep.is_l7_enforced() { + self.solver.assert(&l7_var); + } else { + self.solver.assert(&!l7_var.clone()); + } + self.l7_enforced.insert(ek.clone(), l7_var); + + // L7 allows write? + let allowed = ep.allowed_methods(); + let write_set: HashSet<&str> = WRITE_METHODS.iter().copied().collect(); + let has_write = if allowed.is_empty() { + true // L4-only: all methods pass + } else { + allowed.iter().any(|m| write_set.contains(m.as_str())) + }; + + let l7w_var = Bool::new_const(format!("l7_allows_write_{ek}")); + if ep.is_l7_enforced() { + if has_write { + self.solver.assert(&l7w_var); + } else { + self.solver.assert(&!l7w_var.clone()); + } + } else { + // L4-only: all methods pass through + self.solver.assert(&l7w_var); + } + self.l7_allows_write.insert(ek, l7w_var); + } + } + } + } + + fn encode_binary_capabilities(&mut self) { + for bpath in &self.binary_paths.clone() { + let cap = self.binary_registry.get_or_unknown(bpath); + + let bypass_var = Bool::new_const(format!("binary_bypasses_l7_{bpath}")); + if cap.bypasses_l7() { + self.solver.assert(&bypass_var); + } else { + self.solver.assert(&!bypass_var.clone()); + } + self.binary_bypasses_l7.insert(bpath.clone(), bypass_var); + + let write_var = Bool::new_const(format!("binary_can_write_{bpath}")); + if cap.can_write() { + self.solver.assert(&write_var); + } else { + self.solver.assert(&!write_var.clone()); + } + self.binary_can_write.insert(bpath.clone(), write_var); + + let exfil_var = Bool::new_const(format!("binary_can_exfil_{bpath}")); + if cap.can_exfiltrate { + self.solver.assert(&exfil_var); + } else { + self.solver.assert(&!exfil_var.clone()); + } + self.binary_can_exfil.insert(bpath.clone(), exfil_var); + + let http_var = Bool::new_const(format!("binary_can_construct_http_{bpath}")); + if cap.can_construct_http { + self.solver.assert(&http_var); + } else { + self.solver.assert(&!http_var.clone()); + } + self.binary_can_construct_http + .insert(bpath.clone(), http_var); + } + } + + fn encode_credentials(&mut self) { + let hosts: HashSet = self.endpoints.iter().map(|e| e.host.clone()).collect(); + + for host in &hosts { + let creds = self.credentials.credentials_for_host(host); + let api = self.credentials.api_for_host(host); + + let mut has_write = false; + let mut has_destructive = false; + + for cred in &creds { + if let Some(api) = api { + if !api.write_actions_for_scopes(&cred.scopes).is_empty() { + has_write = true; + } + if !api.destructive_actions_for_scopes(&cred.scopes).is_empty() { + has_destructive = true; + } + } else if !cred.scopes.is_empty() { + has_write = true; + } + } + + let cw_var = Bool::new_const(format!("credential_has_write_{host}")); + if has_write { + self.solver.assert(&cw_var); + } else { + self.solver.assert(&!cw_var.clone()); + } + self.credential_has_write.insert(host.clone(), cw_var); + + let cd_var = Bool::new_const(format!("credential_has_destructive_{host}")); + if has_destructive { + self.solver.assert(&cd_var); + } else { + self.solver.assert(&!cd_var.clone()); + } + self.credential_has_destructive.insert(host.clone(), cd_var); + } + } + + fn encode_filesystem(&mut self) { + for path in self.policy.filesystem_policy.readable_paths() { + let var = Bool::new_const(format!("fs_readable_{path}")); + self.solver.assert(&var); + self.filesystem_readable.insert(path, var); + } + } + + // --- Query helpers --- + + fn false_val() -> Bool { + Bool::from_bool(false) + } + + /// Build a Z3 expression for whether a binary can write to an endpoint. + pub fn can_write_to_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool { + let ek = eid.key(); + let access_key = format!("{bpath}:{ek}"); + + let has_access = match self.policy_allows.get(&access_key) { + Some(v) => v.clone(), + None => return Self::false_val(), + }; + + let bypass = self + .binary_bypasses_l7 + .get(bpath) + .cloned() + .unwrap_or_else(Self::false_val); + let l7_enforced = self + .l7_enforced + .get(&ek) + .cloned() + .unwrap_or_else(Self::false_val); + let l7_write = self + .l7_allows_write + .get(&ek) + .cloned() + .unwrap_or_else(Self::false_val); + let binary_write = self + .binary_can_write + .get(bpath) + .cloned() + .unwrap_or_else(Self::false_val); + let cred_write = self + .credential_has_write + .get(&eid.host) + .cloned() + .unwrap_or_else(Self::false_val); + + Bool::and(&[ + has_access, + binary_write, + Bool::or(&[!l7_enforced, l7_write, bypass]), + cred_write, + ]) + } + + /// Build a Z3 expression for whether data can be exfiltrated via this path. + pub fn can_exfil_via_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool { + let ek = eid.key(); + let access_key = format!("{bpath}:{ek}"); + + let has_access = match self.policy_allows.get(&access_key) { + Some(v) => v.clone(), + None => return Self::false_val(), + }; + + let exfil = self + .binary_can_exfil + .get(bpath) + .cloned() + .unwrap_or_else(Self::false_val); + let bypass = self + .binary_bypasses_l7 + .get(bpath) + .cloned() + .unwrap_or_else(Self::false_val); + let l7_enforced = self + .l7_enforced + .get(&ek) + .cloned() + .unwrap_or_else(Self::false_val); + let l7_write = self + .l7_allows_write + .get(&ek) + .cloned() + .unwrap_or_else(Self::false_val); + let http = self + .binary_can_construct_http + .get(bpath) + .cloned() + .unwrap_or_else(Self::false_val); + + Bool::and(&[ + has_access, + exfil, + Bool::or(&[ + Bool::and(&[!l7_enforced.clone(), http.clone()]), + Bool::and(&[l7_write, http]), + bypass, + ]), + ]) + } + + /// Check satisfiability of an expression against the base constraints. + pub fn check_sat(&self, expr: &Bool) -> SatResult { + self.solver.push(); + self.solver.assert(expr); + let result = self.solver.check(); + self.solver.pop(1); + result + } +} + +/// Build a reachability model from the given inputs. +pub fn build_model( + policy: PolicyModel, + credentials: CredentialSet, + binary_registry: BinaryRegistry, +) -> ReachabilityModel { + // Ensure the thread-local Z3 context is initialized + let _ctx = Context::thread_local(); + ReachabilityModel::new(policy, credentials, binary_registry) +} diff --git a/crates/openshell-prover/src/policy.rs b/crates/openshell-prover/src/policy.rs new file mode 100644 index 00000000..01aa4a79 --- /dev/null +++ b/crates/openshell-prover/src/policy.rs @@ -0,0 +1,428 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Policy YAML parsing into prover-specific types. +//! +//! We parse the policy YAML directly (rather than going through the proto +//! types) because the prover needs fields like `access`, `protocol`, and +//! individual L7 rules that the proto representation strips. + +use std::collections::{BTreeMap, HashSet}; +use std::path::Path; + +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +// --------------------------------------------------------------------------- +// Policy intent +// --------------------------------------------------------------------------- + +/// The inferred access intent for an endpoint. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum PolicyIntent { + L4Only, + ReadOnly, + ReadWrite, + Full, + Custom, +} + +impl std::fmt::Display for PolicyIntent { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Self::L4Only => write!(f, "l4_only"), + Self::ReadOnly => write!(f, "read_only"), + Self::ReadWrite => write!(f, "read_write"), + Self::Full => write!(f, "full"), + Self::Custom => write!(f, "custom"), + } + } +} + +/// HTTP methods considered to be write operations. +pub const WRITE_METHODS: &[&str] = &["POST", "PUT", "PATCH", "DELETE"]; + +/// All standard HTTP methods. +const ALL_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH", "DELETE"]; + +// --------------------------------------------------------------------------- +// Serde types — mirrors the YAML schema +// --------------------------------------------------------------------------- + +#[derive(Debug, Deserialize)] +struct PolicyFile { + #[allow(dead_code)] + version: Option, + #[serde(default)] + filesystem_policy: Option, + #[serde(default)] + network_policies: Option>, + // Ignored fields the prover does not need. + #[serde(default)] + #[allow(dead_code)] + landlock: Option, + #[serde(default)] + #[allow(dead_code)] + process: Option, +} + +#[derive(Debug, Deserialize)] +struct FilesystemDef { + #[serde(default = "default_true")] + include_workdir: bool, + #[serde(default)] + read_only: Vec, + #[serde(default)] + read_write: Vec, +} + +fn default_true() -> bool { + true +} + +#[derive(Debug, Deserialize)] +struct NetworkPolicyRuleDef { + #[serde(default)] + name: Option, + #[serde(default)] + endpoints: Vec, + #[serde(default)] + binaries: Vec, +} + +#[derive(Debug, Deserialize)] +struct EndpointDef { + #[serde(default)] + host: String, + #[serde(default)] + port: u32, + #[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)] + allowed_ips: Vec, +} + +#[derive(Debug, Deserialize)] +struct L7RuleDef { + allow: L7AllowDef, +} + +#[derive(Debug, Deserialize)] +struct L7AllowDef { + #[serde(default)] + method: String, + #[serde(default)] + path: String, + #[serde(default)] + command: String, +} + +#[derive(Debug, Deserialize)] +struct BinaryDef { + path: String, +} + +// --------------------------------------------------------------------------- +// Public model types +// --------------------------------------------------------------------------- + +/// A single L7 rule (method + path) on an endpoint. +#[derive(Debug, Clone)] +pub struct L7Rule { + pub method: String, + pub path: String, + pub command: String, +} + +/// A network endpoint in the policy. +#[derive(Debug, Clone)] +pub struct Endpoint { + pub host: String, + pub port: u32, + pub ports: Vec, + pub protocol: String, + pub tls: String, + pub enforcement: String, + pub access: String, + pub rules: Vec, + pub allowed_ips: Vec, +} + +impl Endpoint { + /// Whether this endpoint has L7 (protocol-level) enforcement. + pub fn is_l7_enforced(&self) -> bool { + !self.protocol.is_empty() + } + + /// The inferred access intent. + pub fn intent(&self) -> PolicyIntent { + if self.protocol.is_empty() { + return PolicyIntent::L4Only; + } + match self.access.as_str() { + "read-only" => PolicyIntent::ReadOnly, + "read-write" => PolicyIntent::ReadWrite, + "full" => PolicyIntent::Full, + _ => { + if self.rules.is_empty() { + return PolicyIntent::Custom; + } + let methods: HashSet = + self.rules.iter().map(|r| r.method.to_uppercase()).collect(); + let read_only: HashSet = ["GET", "HEAD", "OPTIONS"] + .iter() + .map(|s| (*s).to_owned()) + .collect(); + if methods.is_subset(&read_only) { + PolicyIntent::ReadOnly + } else if !methods.contains("DELETE") { + PolicyIntent::ReadWrite + } else { + PolicyIntent::Full + } + } + } + } + + /// The effective list of ports for this endpoint. + pub fn effective_ports(&self) -> Vec { + if !self.ports.is_empty() { + return self.ports.clone(); + } + if self.port > 0 { + return vec![self.port]; + } + vec![] + } + + /// The set of HTTP methods this endpoint allows. Empty means all (L4-only). + pub fn allowed_methods(&self) -> HashSet { + if self.protocol.is_empty() { + return HashSet::new(); // L4-only: all traffic passes + } + match self.access.as_str() { + "read-only" => ["GET", "HEAD", "OPTIONS"] + .iter() + .map(|s| (*s).to_owned()) + .collect(), + "read-write" => ["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH"] + .iter() + .map(|s| (*s).to_owned()) + .collect(), + "full" => ALL_METHODS.iter().map(|s| (*s).to_owned()).collect(), + _ => { + if !self.rules.is_empty() { + let mut methods = HashSet::new(); + for r in &self.rules { + let m = r.method.to_uppercase(); + if m == "*" { + return ALL_METHODS.iter().map(|s| (*s).to_owned()).collect(); + } + methods.insert(m); + } + return methods; + } + HashSet::new() + } + } + } +} + +/// A binary path entry in a network policy rule. +#[derive(Debug, Clone)] +pub struct Binary { + pub path: String, +} + +/// A named network policy rule containing endpoints and binaries. +#[derive(Debug, Clone)] +pub struct NetworkPolicyRule { + pub name: String, + pub endpoints: Vec, + pub binaries: Vec, +} + +/// Filesystem access policy. +#[derive(Debug, Clone)] +pub struct FilesystemPolicy { + pub include_workdir: bool, + pub read_only: Vec, + pub read_write: Vec, +} + +impl Default for FilesystemPolicy { + fn default() -> Self { + Self { + include_workdir: true, + read_only: Vec::new(), + read_write: Vec::new(), + } + } +} + +impl FilesystemPolicy { + /// All readable paths (union of `read_only` and `read_write`), with workdir + /// added when `include_workdir` is true and not already present. + pub fn readable_paths(&self) -> Vec { + let mut paths: Vec = self + .read_only + .iter() + .chain(self.read_write.iter()) + .cloned() + .collect(); + if self.include_workdir && !paths.iter().any(|p| p == "/sandbox") { + paths.push("/sandbox".to_owned()); + } + paths + } +} + +/// The top-level policy model used by the prover. +#[derive(Debug, Clone)] +pub struct PolicyModel { + pub version: u32, + pub filesystem_policy: FilesystemPolicy, + pub network_policies: BTreeMap, +} + +impl Default for PolicyModel { + fn default() -> Self { + Self { + version: 1, + filesystem_policy: FilesystemPolicy::default(), + network_policies: BTreeMap::new(), + } + } +} + +impl PolicyModel { + /// All (policy_name, endpoint) pairs. + pub fn all_endpoints(&self) -> Vec<(&str, &Endpoint)> { + let mut result = Vec::new(); + for (name, rule) in &self.network_policies { + for ep in &rule.endpoints { + result.push((name.as_str(), ep)); + } + } + result + } + + /// Deduplicated list of all binary paths across all policies. + pub fn all_binaries(&self) -> Vec<&Binary> { + let mut seen = HashSet::new(); + let mut result = Vec::new(); + for rule in self.network_policies.values() { + for b in &rule.binaries { + if seen.insert(&b.path) { + result.push(b); + } + } + } + result + } + + /// All (binary, policy_name, endpoint) triples. + pub fn binary_endpoint_pairs(&self) -> Vec<(&Binary, &str, &Endpoint)> { + let mut result = Vec::new(); + for (name, rule) in &self.network_policies { + for b in &rule.binaries { + for ep in &rule.endpoints { + result.push((b, name.as_str(), ep)); + } + } + } + result + } +} + +// --------------------------------------------------------------------------- +// Parsing +// --------------------------------------------------------------------------- + +/// Parse an OpenShell policy YAML file into a [`PolicyModel`]. +pub fn parse_policy(path: &Path) -> Result { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading policy file {}", path.display()))?; + parse_policy_str(&contents) +} + +/// Parse a policy YAML string into a [`PolicyModel`]. +pub fn parse_policy_str(yaml: &str) -> Result { + let raw: PolicyFile = serde_yml::from_str(yaml) + .into_diagnostic() + .wrap_err("parsing policy YAML")?; + + let fs = match raw.filesystem_policy { + Some(fs_def) => FilesystemPolicy { + include_workdir: fs_def.include_workdir, + read_only: fs_def.read_only, + read_write: fs_def.read_write, + }, + None => FilesystemPolicy::default(), + }; + + let mut network_policies = BTreeMap::new(); + if let Some(np) = raw.network_policies { + for (key, rule_raw) in np { + let endpoints = rule_raw + .endpoints + .into_iter() + .map(|ep_raw| { + let rules = ep_raw + .rules + .into_iter() + .map(|r| L7Rule { + method: r.allow.method, + path: r.allow.path, + command: r.allow.command, + }) + .collect(); + Endpoint { + host: ep_raw.host, + port: ep_raw.port, + ports: ep_raw.ports, + protocol: ep_raw.protocol, + tls: ep_raw.tls, + enforcement: ep_raw.enforcement, + access: ep_raw.access, + rules, + allowed_ips: ep_raw.allowed_ips, + } + }) + .collect(); + + let binaries = rule_raw + .binaries + .into_iter() + .map(|b| Binary { path: b.path }) + .collect(); + + let name = rule_raw.name.unwrap_or_else(|| key.clone()); + network_policies.insert( + key, + NetworkPolicyRule { + name, + endpoints, + binaries, + }, + ); + } + } + + Ok(PolicyModel { + version: raw.version.unwrap_or(1), + filesystem_policy: fs, + network_policies, + }) +} diff --git a/crates/openshell-prover/src/queries.rs b/crates/openshell-prover/src/queries.rs new file mode 100644 index 00000000..ab301474 --- /dev/null +++ b/crates/openshell-prover/src/queries.rs @@ -0,0 +1,254 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Verification queries: `check_data_exfiltration` and `check_write_bypass`. + +use z3::SatResult; + +use crate::finding::{ExfilPath, Finding, FindingPath, RiskLevel, WriteBypassPath}; +use crate::model::ReachabilityModel; +use crate::policy::PolicyIntent; + +/// Check for data exfiltration paths from readable filesystem to writable +/// egress channels. +pub fn check_data_exfiltration(model: &ReachabilityModel) -> Vec { + if model.policy.filesystem_policy.readable_paths().is_empty() { + return Vec::new(); + } + + let mut exfil_paths: Vec = Vec::new(); + + for bpath in &model.binary_paths { + let cap = model.binary_registry.get_or_unknown(bpath); + if !cap.can_exfiltrate { + continue; + } + + for eid in &model.endpoints { + let expr = model.can_exfil_via_endpoint(bpath, eid); + + if model.check_sat(&expr) == SatResult::Sat { + // Determine L7 status and mechanism + let ep_is_l7 = is_endpoint_l7_enforced(&model.policy, &eid.host, eid.port); + let bypass = cap.bypasses_l7(); + + let (l7_status, mut mechanism) = if bypass { + ( + "l7_bypassed".to_owned(), + format!( + "{} — uses non-HTTP protocol, bypasses L7 inspection", + cap.description + ), + ) + } else if !ep_is_l7 { + ( + "l4_only".to_owned(), + format!( + "L4-only endpoint — no HTTP inspection, {} can send arbitrary data", + bpath + ), + ) + } else { + // L7 is enforced and allows write — policy is + // working as intended. Not a finding. + continue; + }; + + if !cap.exfil_mechanism.is_empty() { + mechanism = format!("{}. Exfil via: {}", mechanism, cap.exfil_mechanism); + } + + exfil_paths.push(ExfilPath { + binary: bpath.clone(), + endpoint_host: eid.host.clone(), + endpoint_port: eid.port, + mechanism, + policy_name: eid.policy_name.clone(), + l7_status, + }); + } + } + } + + if exfil_paths.is_empty() { + return Vec::new(); + } + + let readable = model.policy.filesystem_policy.readable_paths(); + let has_l4_only = exfil_paths.iter().any(|p| p.l7_status == "l4_only"); + let has_bypass = exfil_paths.iter().any(|p| p.l7_status == "l7_bypassed"); + let risk = if has_l4_only || has_bypass { + RiskLevel::Critical + } else { + RiskLevel::High + }; + + let mut remediation = Vec::new(); + if has_l4_only { + remediation.push( + "Add `protocol: rest` with specific L7 rules to L4-only endpoints \ + to enable HTTP inspection and restrict to safe methods/paths." + .to_owned(), + ); + } + if has_bypass { + remediation.push( + "Binaries using non-HTTP protocols (git, ssh, nc) bypass L7 inspection. \ + Remove these binaries from the policy if write access is not intended, \ + or restrict credential scopes to read-only." + .to_owned(), + ); + } + remediation + .push("Restrict filesystem read access to only the paths the agent needs.".to_owned()); + + let paths: Vec = exfil_paths.into_iter().map(FindingPath::Exfil).collect(); + + let n_paths = paths.len(); + vec![Finding { + query: "data_exfiltration".to_owned(), + title: "Data Exfiltration Paths Detected".to_owned(), + description: format!( + "{n_paths} exfiltration path(s) found from {} readable filesystem path(s) to external endpoints.", + readable.len() + ), + risk, + paths, + remediation, + accepted: false, + accepted_reason: String::new(), + }] +} + +/// Check for write capabilities that bypass read-only policy intent. +pub fn check_write_bypass(model: &ReachabilityModel) -> Vec { + let mut bypass_paths: Vec = Vec::new(); + + for (policy_name, rule) in &model.policy.network_policies { + for ep in &rule.endpoints { + // Only check endpoints where the intent is read-only or L4-only + let intent = ep.intent(); + if !matches!(intent, PolicyIntent::ReadOnly) { + continue; + } + + for port in ep.effective_ports() { + for b in &rule.binaries { + let cap = model.binary_registry.get_or_unknown(&b.path); + + // Check: binary bypasses L7 and can write + if cap.bypasses_l7() && cap.can_write() { + let cred_actions = collect_credential_actions(model, &ep.host, &cap); + if !cred_actions.is_empty() + || model.credentials.credentials_for_host(&ep.host).is_empty() + { + bypass_paths.push(WriteBypassPath { + binary: b.path.clone(), + endpoint_host: ep.host.clone(), + endpoint_port: port, + policy_name: policy_name.clone(), + policy_intent: intent.to_string(), + bypass_reason: "l7_bypass_protocol".to_owned(), + credential_actions: cred_actions, + }); + } + } + + // Check: L4-only endpoint + binary can construct HTTP + credential has write + if !ep.is_l7_enforced() && cap.can_construct_http { + let cred_actions = collect_credential_actions(model, &ep.host, &cap); + if !cred_actions.is_empty() { + bypass_paths.push(WriteBypassPath { + binary: b.path.clone(), + endpoint_host: ep.host.clone(), + endpoint_port: port, + policy_name: policy_name.clone(), + policy_intent: intent.to_string(), + bypass_reason: "l4_only".to_owned(), + credential_actions: cred_actions, + }); + } + } + } + } + } + } + + if bypass_paths.is_empty() { + return Vec::new(); + } + + let n = bypass_paths.len(); + let paths: Vec = bypass_paths + .into_iter() + .map(FindingPath::WriteBypass) + .collect(); + + vec![Finding { + query: "write_bypass".to_owned(), + title: "Write Bypass Detected — Read-Only Intent Violated".to_owned(), + description: format!("{n} path(s) allow write operations despite read-only policy intent."), + risk: RiskLevel::High, + paths, + remediation: vec![ + "For L4-only endpoints: add `protocol: rest` with `access: read-only` \ + to enable HTTP method filtering." + .to_owned(), + "For L7-bypassing binaries (git, ssh, nc): remove them from the policy's \ + binary list if write access is not intended." + .to_owned(), + "Restrict credential scopes to read-only where possible.".to_owned(), + ], + accepted: false, + accepted_reason: String::new(), + }] +} + +/// Run both verification queries. +pub fn run_all_queries(model: &ReachabilityModel) -> Vec { + let mut findings = Vec::new(); + findings.extend(check_data_exfiltration(model)); + findings.extend(check_write_bypass(model)); + findings +} + +// --------------------------------------------------------------------------- +// Helpers +// --------------------------------------------------------------------------- + +/// Check whether an endpoint in the policy is L7-enforced. +fn is_endpoint_l7_enforced(policy: &crate::policy::PolicyModel, host: &str, port: u32) -> bool { + for rule in policy.network_policies.values() { + for ep in &rule.endpoints { + if ep.host == host && ep.effective_ports().contains(&port) { + return ep.is_l7_enforced(); + } + } + } + false +} + +/// Collect human-readable credential action descriptions for a host. +fn collect_credential_actions( + model: &ReachabilityModel, + host: &str, + _cap: &crate::registry::BinaryCapability, +) -> Vec { + let creds = model.credentials.credentials_for_host(host); + let api = model.credentials.api_for_host(host); + let mut actions = Vec::new(); + + for cred in &creds { + if let Some(api) = api { + for wa in api.write_actions_for_scopes(&cred.scopes) { + actions.push(format!("{} {} ({})", wa.method, wa.path, wa.action)); + } + } else { + actions.push(format!( + "credential '{}' has scopes: {:?}", + cred.name, cred.scopes + )); + } + } + actions +} diff --git a/crates/openshell-prover/src/registry.rs b/crates/openshell-prover/src/registry.rs new file mode 100644 index 00000000..0ae5e535 --- /dev/null +++ b/crates/openshell-prover/src/registry.rs @@ -0,0 +1,316 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Binary capability registry — loads YAML descriptors that describe what each +//! binary can do (protocols, exfiltration, HTTP construction, etc.). + +use std::collections::HashMap; +use std::path::Path; + +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +// --------------------------------------------------------------------------- +// Serde types +// --------------------------------------------------------------------------- + +#[derive(Debug, Deserialize)] +struct BinaryCapabilityDef { + binary: String, + #[serde(default)] + description: String, + #[serde(default)] + protocols: Vec, + #[serde(default)] + spawns: Vec, + #[serde(default)] + can_exfiltrate: bool, + #[serde(default)] + exfil_mechanism: String, + #[serde(default)] + can_construct_http: bool, +} + +#[derive(Debug, Deserialize)] +struct BinaryProtocolDef { + #[serde(default)] + name: String, + #[serde(default)] + transport: String, + #[serde(default)] + description: String, + #[serde(default)] + bypasses_l7: bool, + #[serde(default)] + actions: Vec, +} + +#[derive(Debug, Deserialize)] +struct BinaryActionDef { + #[serde(default)] + name: String, + #[serde(default, rename = "type")] + action_type: String, + #[serde(default)] + description: String, +} + +// --------------------------------------------------------------------------- +// Public types +// --------------------------------------------------------------------------- + +/// Type of action a binary can perform. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ActionType { + Read, + Write, + Destructive, +} + +impl ActionType { + fn from_str(s: &str) -> Self { + match s { + "write" => Self::Write, + "destructive" => Self::Destructive, + _ => Self::Read, + } + } +} + +/// A single action a binary protocol supports. +#[derive(Debug, Clone)] +pub struct BinaryAction { + pub name: String, + pub action_type: ActionType, + pub description: String, +} + +/// A protocol supported by a binary. +#[derive(Debug, Clone)] +pub struct BinaryProtocol { + pub name: String, + pub transport: String, + pub description: String, + pub bypasses_l7: bool, + pub actions: Vec, +} + +impl BinaryProtocol { + /// Whether any action in this protocol is a write or destructive action. + pub fn can_write(&self) -> bool { + self.actions + .iter() + .any(|a| matches!(a.action_type, ActionType::Write | ActionType::Destructive)) + } +} + +/// Capability descriptor for a single binary. +#[derive(Debug, Clone)] +pub struct BinaryCapability { + pub path: String, + pub description: String, + pub protocols: Vec, + pub spawns: Vec, + pub can_exfiltrate: bool, + pub exfil_mechanism: String, + pub can_construct_http: bool, +} + +impl BinaryCapability { + /// Whether any protocol bypasses L7 inspection. + pub fn bypasses_l7(&self) -> bool { + self.protocols.iter().any(|p| p.bypasses_l7) + } + + /// Whether the binary can perform write actions. + pub fn can_write(&self) -> bool { + self.protocols.iter().any(|p| p.can_write()) || self.can_construct_http + } + + /// Short mechanisms by which this binary can write. + pub fn write_mechanisms(&self) -> Vec { + let mut mechanisms = Vec::new(); + for p in &self.protocols { + if p.can_write() { + for a in &p.actions { + if matches!(a.action_type, ActionType::Write | ActionType::Destructive) { + mechanisms.push(format!("{}: {}", p.name, a.name)); + } + } + } + } + if self.can_construct_http { + mechanisms.push("arbitrary HTTP request construction".to_owned()); + } + mechanisms + } +} + +/// Registry of binary capability descriptors. +#[derive(Debug, Clone, Default)] +pub struct BinaryRegistry { + binaries: HashMap, +} + +impl BinaryRegistry { + /// Look up a binary by exact path. + pub fn get(&self, path: &str) -> Option<&BinaryCapability> { + self.binaries.get(path) + } + + /// Look up a binary, falling back to glob matching, then to a conservative + /// unknown descriptor. + pub fn get_or_unknown(&self, path: &str) -> BinaryCapability { + if let Some(cap) = self.binaries.get(path) { + return cap.clone(); + } + // Check glob patterns (e.g., registry has /usr/bin/python* matching /usr/bin/python3.13) + for (reg_path, cap) in &self.binaries { + if reg_path.contains('*') && glob_match(reg_path, path) { + return cap.clone(); + } + } + // Conservative default: unknown binary assumed capable of everything. + BinaryCapability { + path: path.to_owned(), + description: "Unknown binary — not in registry".to_owned(), + protocols: Vec::new(), + spawns: Vec::new(), + can_exfiltrate: true, + exfil_mechanism: String::new(), + can_construct_http: true, + } + } +} + +/// Simple glob matching supporting `*` (single segment) and `**` (multiple +/// segments). +fn glob_match(pattern: &str, path: &str) -> bool { + // Split both on `/` and match segment by segment. + let pat_parts: Vec<&str> = pattern.split('/').collect(); + let path_parts: Vec<&str> = path.split('/').collect(); + glob_match_segments(&pat_parts, &path_parts) +} + +fn glob_match_segments(pat: &[&str], path: &[&str]) -> bool { + if pat.is_empty() { + return path.is_empty(); + } + if pat[0] == "**" { + // ** matches zero or more segments. + for i in 0..=path.len() { + if glob_match_segments(&pat[1..], &path[i..]) { + return true; + } + } + return false; + } + if path.is_empty() { + return false; + } + if segment_match(pat[0], path[0]) { + return glob_match_segments(&pat[1..], &path[1..]); + } + false +} + +fn segment_match(pattern: &str, segment: &str) -> bool { + if pattern == "*" { + return true; + } + if !pattern.contains('*') { + return pattern == segment; + } + // Simple wildcard within a segment: split on '*' and check prefix/suffix. + let parts: Vec<&str> = pattern.split('*').collect(); + if parts.len() == 2 { + return segment.starts_with(parts[0]) && segment.ends_with(parts[1]); + } + // Fallback: fnmatch-like. For simplicity, just check contains for each part. + let mut remaining = segment; + for (i, part) in parts.iter().enumerate() { + if part.is_empty() { + continue; + } + if i == 0 { + if !remaining.starts_with(part) { + return false; + } + remaining = &remaining[part.len()..]; + } else if let Some(pos) = remaining.find(part) { + remaining = &remaining[pos + part.len()..]; + } else { + return false; + } + } + true +} + +// --------------------------------------------------------------------------- +// Loading +// --------------------------------------------------------------------------- + +/// Load a single binary capability descriptor from a YAML file. +fn load_binary_capability(path: &Path) -> Result { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading binary descriptor {}", path.display()))?; + let raw: BinaryCapabilityDef = serde_yml::from_str(&contents) + .into_diagnostic() + .wrap_err_with(|| format!("parsing binary descriptor {}", path.display()))?; + + let protocols = raw + .protocols + .into_iter() + .map(|p| { + let actions = p + .actions + .into_iter() + .map(|a| BinaryAction { + name: a.name, + action_type: ActionType::from_str(&a.action_type), + description: a.description, + }) + .collect(); + BinaryProtocol { + name: p.name, + transport: p.transport, + description: p.description, + bypasses_l7: p.bypasses_l7, + actions, + } + }) + .collect(); + + Ok(BinaryCapability { + path: raw.binary, + description: raw.description, + protocols, + spawns: raw.spawns, + can_exfiltrate: raw.can_exfiltrate, + exfil_mechanism: raw.exfil_mechanism, + can_construct_http: raw.can_construct_http, + }) +} + +/// Load all binary capability descriptors from a registry directory. +/// +/// Expects `{registry_dir}/binaries/*.yaml`. +pub fn load_binary_registry(registry_dir: &Path) -> Result { + let mut binaries = HashMap::new(); + let binaries_dir = registry_dir.join("binaries"); + if binaries_dir.is_dir() { + let entries = std::fs::read_dir(&binaries_dir) + .into_diagnostic() + .wrap_err_with(|| format!("reading directory {}", binaries_dir.display()))?; + for entry in entries { + let entry = entry.into_diagnostic()?; + let path = entry.path(); + if path.extension().is_some_and(|ext| ext == "yaml") { + let cap = load_binary_capability(&path)?; + binaries.insert(cap.path.clone(), cap); + } + } + } + Ok(BinaryRegistry { binaries }) +} diff --git a/crates/openshell-prover/src/report.rs b/crates/openshell-prover/src/report.rs new file mode 100644 index 00000000..27207a6a --- /dev/null +++ b/crates/openshell-prover/src/report.rs @@ -0,0 +1,393 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Terminal report rendering (full and compact). + +use std::collections::{HashMap, HashSet}; +use std::path::Path; + +use owo_colors::OwoColorize; + +use crate::finding::{Finding, FindingPath, RiskLevel}; + +// --------------------------------------------------------------------------- +// Compact titles (short labels for each query type) +// --------------------------------------------------------------------------- + +fn compact_title(query: &str) -> &str { + match query { + "data_exfiltration" => "Data exfiltration possible", + "write_bypass" => "Write bypass \u{2014} read-only intent violated", + _ => "Unknown finding", + } +} + +// --------------------------------------------------------------------------- +// Compact detail line +// --------------------------------------------------------------------------- + +fn compact_detail(finding: &Finding) -> String { + match finding.query.as_str() { + "data_exfiltration" => { + let mut by_status: HashMap<&str, HashSet> = HashMap::new(); + for path in &finding.paths { + if let FindingPath::Exfil(p) = path { + by_status + .entry(&p.l7_status) + .or_default() + .insert(format!("{}:{}", p.endpoint_host, p.endpoint_port)); + } + } + let mut parts = Vec::new(); + if let Some(eps) = by_status.get("l4_only") { + let mut sorted: Vec<&String> = eps.iter().collect(); + sorted.sort(); + parts.push(format!( + "L4-only: {}", + sorted + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", ") + )); + } + if let Some(eps) = by_status.get("l7_bypassed") { + let mut sorted: Vec<&String> = eps.iter().collect(); + sorted.sort(); + parts.push(format!( + "wire protocol bypass: {}", + sorted + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", ") + )); + } + if let Some(eps) = by_status.get("l7_allows_write") { + let mut sorted: Vec<&String> = eps.iter().collect(); + sorted.sort(); + parts.push(format!( + "L7 write: {}", + sorted + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", ") + )); + } + parts.join("; ") + } + "write_bypass" => { + let mut reasons = HashSet::new(); + let mut endpoints = HashSet::new(); + for path in &finding.paths { + if let FindingPath::WriteBypass(p) = path { + reasons.insert(p.bypass_reason.as_str()); + endpoints.insert(format!("{}:{}", p.endpoint_host, p.endpoint_port)); + } + } + let mut sorted_eps: Vec<&String> = endpoints.iter().collect(); + sorted_eps.sort(); + let ep_list = sorted_eps + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", "); + if reasons.contains("l4_only") && reasons.contains("l7_bypass_protocol") { + format!("L4-only + wire protocol: {ep_list}") + } else if reasons.contains("l4_only") { + format!("L4-only (no inspection): {ep_list}") + } else if reasons.contains("l7_bypass_protocol") { + format!("wire protocol bypasses L7: {ep_list}") + } else { + String::new() + } + } + _ => String::new(), + } +} + +// --------------------------------------------------------------------------- +// Risk formatting +// --------------------------------------------------------------------------- + +fn risk_label(risk: RiskLevel) -> String { + match risk { + RiskLevel::Critical => "CRITICAL".to_owned(), + RiskLevel::High => "HIGH".to_owned(), + } +} + +fn print_risk_label(risk: RiskLevel) { + match risk { + RiskLevel::Critical => print!("{}", "CRITICAL".bold().red()), + RiskLevel::High => print!("{}", " HIGH".red()), + } +} + +// --------------------------------------------------------------------------- +// Compact output +// --------------------------------------------------------------------------- + +/// Render compact output (one-line-per-finding for demos and CI). +/// Returns exit code: 0 = pass, 1 = critical/high found. +pub fn render_compact(findings: &[Finding], _policy_path: &str, _credentials_path: &str) -> i32 { + let active: Vec<&Finding> = findings.iter().filter(|f| !f.accepted).collect(); + let accepted: Vec<&Finding> = findings.iter().filter(|f| f.accepted).collect(); + + for finding in &active { + print!(" "); + print_risk_label(finding.risk); + println!(" {}", compact_title(&finding.query)); + let detail = compact_detail(finding); + if !detail.is_empty() { + println!(" {detail}"); + } + println!(); + } + + for finding in &accepted { + println!( + " {} {}", + "ACCEPTED".dimmed(), + compact_title(&finding.query).dimmed() + ); + } + if !accepted.is_empty() { + println!(); + } + + // Verdict + let mut counts: HashMap = HashMap::new(); + for f in &active { + *counts.entry(f.risk).or_default() += 1; + } + let has_critical = counts.contains_key(&RiskLevel::Critical); + let has_high = counts.contains_key(&RiskLevel::High); + let accepted_note = if accepted.is_empty() { + String::new() + } else { + format!(", {} accepted", accepted.len()) + }; + + if has_critical || has_high { + let n = counts.get(&RiskLevel::Critical).unwrap_or(&0) + + counts.get(&RiskLevel::High).unwrap_or(&0); + println!( + " {} {n} critical/high gaps{accepted_note}", + " FAIL ".white().bold().on_red() + ); + 1 + } else if !active.is_empty() { + println!( + " {} advisories only{accepted_note}", + " PASS ".black().bold().on_yellow() + ); + 0 + } else { + println!( + " {} all findings accepted{accepted_note}", + " PASS ".white().bold().on_green() + ); + 0 + } +} + +// --------------------------------------------------------------------------- +// Full terminal report +// --------------------------------------------------------------------------- + +/// Render a full terminal report with finding panels. +/// Returns exit code: 0 = pass, 1 = critical/high found. +pub fn render_report(findings: &[Finding], policy_path: &str, credentials_path: &str) -> i32 { + let policy_name = Path::new(policy_path) + .file_name() + .map_or("policy.yaml", |n| n.to_str().unwrap_or("policy.yaml")); + let creds_name = Path::new(credentials_path) + .file_name() + .map_or("credentials.yaml", |n| { + n.to_str().unwrap_or("credentials.yaml") + }); + + println!(); + println!( + "{}", + "\u{250c}\u{2500}\u{2500} OpenShell Policy Prover \u{2500}\u{2500}\u{2510}".blue() + ); + println!(" Policy: {policy_name}"); + println!(" Credentials: {creds_name}"); + println!(); + + let active: Vec<&Finding> = findings.iter().filter(|f| !f.accepted).collect(); + let accepted: Vec<&Finding> = findings.iter().filter(|f| f.accepted).collect(); + + // Summary + let mut counts: HashMap = HashMap::new(); + for f in &active { + *counts.entry(f.risk).or_default() += 1; + } + + println!("{}", "Finding Summary".bold().underline()); + for level in [RiskLevel::Critical, RiskLevel::High] { + if let Some(&count) = counts.get(&level) { + match level { + RiskLevel::Critical => { + println!(" {:>10} {count}", "CRITICAL".bold().red()); + } + RiskLevel::High => println!(" {:>10} {count}", "HIGH".red()), + } + } + } + if !accepted.is_empty() { + println!(" {:>10} {}", "ACCEPTED".dimmed(), accepted.len()); + } + println!(); + + if active.is_empty() && accepted.is_empty() { + println!("{}", "No findings. Policy posture is clean.".green().bold()); + return 0; + } + + // Per-finding details + for (i, finding) in active.iter().enumerate() { + let label = risk_label(finding.risk); + let border = match finding.risk { + RiskLevel::Critical => format!("{}", format!("[{label}]").bold().red()), + RiskLevel::High => format!("{}", format!("[{label}]").red()), + }; + + println!("--- Finding #{} {border} ---", i + 1); + println!(" {}", finding.title.bold()); + println!(" {}", finding.description); + println!(); + + // Render paths + render_paths(&finding.paths); + + // Remediation + if !finding.remediation.is_empty() { + println!(" {}", "Remediation:".bold()); + for r in &finding.remediation { + println!(" - {r}"); + } + println!(); + } + } + + // Accepted findings + if !accepted.is_empty() { + println!("{}", "--- Accepted Risks ---".dimmed()); + for finding in &accepted { + println!( + " {} {}", + risk_label(finding.risk).dimmed(), + finding.title.dimmed() + ); + println!( + " {}", + format!("Reason: {}", finding.accepted_reason).dimmed() + ); + println!(); + } + } + + // Verdict + let has_critical = counts.contains_key(&RiskLevel::Critical); + let has_high = counts.contains_key(&RiskLevel::High); + let accepted_note = if accepted.is_empty() { + String::new() + } else { + format!(" ({} accepted)", accepted.len()) + }; + + if has_critical { + println!( + "{}{accepted_note}", + "FAIL \u{2014} Critical gaps found.".bold().red() + ); + 1 + } else if has_high { + println!( + "{}{accepted_note}", + "FAIL \u{2014} High-risk gaps found.".bold().red() + ); + 1 + } else if !active.is_empty() { + println!( + "{}{accepted_note}", + "PASS \u{2014} Advisories only.".bold().yellow() + ); + 0 + } else { + println!( + "{}{accepted_note}", + "PASS \u{2014} All findings accepted.".bold().green() + ); + 0 + } +} + +fn render_paths(paths: &[FindingPath]) { + if paths.is_empty() { + return; + } + + match &paths[0] { + FindingPath::Exfil(_) => render_exfil_paths(paths), + FindingPath::WriteBypass(_) => render_write_bypass_paths(paths), + } +} + +fn render_exfil_paths(paths: &[FindingPath]) { + println!( + " {:<30} {:<25} {:<15} {}", + "Binary".bold(), + "Endpoint".bold(), + "L7 Status".bold(), + "Mechanism".bold(), + ); + for path in paths { + if let FindingPath::Exfil(p) = path { + let l7_display = match p.l7_status.as_str() { + "l4_only" => format!("{}", "L4-only".red()), + "l7_bypassed" => format!("{}", "bypassed".red()), + "l7_allows_write" => format!("{}", "L7 write".yellow()), + _ => p.l7_status.clone(), + }; + let ep = format!("{}:{}", p.endpoint_host, p.endpoint_port); + // Truncate mechanism for display + let mech = if p.mechanism.len() > 50 { + format!("{}...", &p.mechanism[..47]) + } else { + p.mechanism.clone() + }; + println!(" {:<30} {:<25} {:<15} {}", p.binary, ep, l7_display, mech); + } + } + println!(); +} + +fn render_write_bypass_paths(paths: &[FindingPath]) { + println!( + " {:<30} {:<25} {:<15} {}", + "Binary".bold(), + "Endpoint".bold(), + "Bypass".bold(), + "Intent".bold(), + ); + for path in paths { + if let FindingPath::WriteBypass(p) = path { + let ep = format!("{}:{}", p.endpoint_host, p.endpoint_port); + let bypass_display = match p.bypass_reason.as_str() { + "l4_only" => format!("{}", "L4-only".red()), + "l7_bypass_protocol" => format!("{}", "wire proto".red()), + _ => p.bypass_reason.clone(), + }; + println!( + " {:<30} {:<25} {:<15} {}", + p.binary, ep, bypass_display, p.policy_intent + ); + } + } + println!(); +} diff --git a/crates/openshell-prover/testdata/accepted-risks.yaml b/crates/openshell-prover/testdata/accepted-risks.yaml new file mode 100644 index 00000000..6af5c714 --- /dev/null +++ b/crates/openshell-prover/testdata/accepted-risks.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +accepted_risks: + - query: inference_relay + reason: "Demo environment — inference.local not configured." + accepted_by: demo diff --git a/crates/openshell-prover/testdata/credentials.yaml b/crates/openshell-prover/testdata/credentials.yaml new file mode 100644 index 00000000..b186ccf9 --- /dev/null +++ b/crates/openshell-prover/testdata/credentials.yaml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +credentials: + - name: github-pat + type: github-pat + scopes: + - repo + injected_via: GITHUB_TOKEN + target_hosts: + - api.github.com + - github.com diff --git a/crates/openshell-prover/testdata/empty-policy.yaml b/crates/openshell-prover/testdata/empty-policy.yaml new file mode 100644 index 00000000..458bab0e --- /dev/null +++ b/crates/openshell-prover/testdata/empty-policy.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/testdata/policy.yaml b/crates/openshell-prover/testdata/policy.yaml new file mode 100644 index 00000000..e98d9531 --- /dev/null +++ b/crates/openshell-prover/testdata/policy.yaml @@ -0,0 +1,50 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 + +filesystem_policy: + include_workdir: true + read_only: + - /usr + - /lib + - /proc + - /dev/urandom + - /app + - /etc + - /var/log + read_write: + - /sandbox + - /tmp + - /dev/null + +landlock: + compatibility: best_effort + +process: + run_as_user: sandbox + run_as_group: sandbox + +# Intent: read-only GitHub access for the agent. +# The REST API has L7 enforcement — only GET allowed. +# github.com is included for git clone — "it just needs connectivity." +network_policies: + github_api: + name: github-api + endpoints: + # REST API — L7 enforced, read-only + - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: read-only + # github.com — for git clone. + # No protocol field — L4 only. + - host: github.com + port: 443 + binaries: + - { path: /usr/local/bin/claude } + - { path: /usr/bin/git } + - { path: /usr/bin/curl } + - { path: /usr/bin/gh } + - { path: /sandbox/.uv/python/**/python3* }