From 1409b7b11931a4053eaaa448bcca11a898cc87e7 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 2 Apr 2026 12:58:01 -0700 Subject: [PATCH 01/11] feat(prover): add native Rust policy prover with Z3 solver MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add openshell-prover crate implementing formal policy verification using Z3 SMT solving. Answers two questions about any sandbox policy: "Can data leave?" and "Can the agent write despite read-only intent?" Native Rust — no Python subprocess, no PYTHONPATH, no uv dependency. Z3 bundled via z3-sys for self-contained builds. Replaces the Python prototype from #703. Closes #699 Signed-off-by: Alexander Watson --- .gitignore | 1 + Cargo.lock | 515 +++++++++++++----- Cargo.toml | 3 + crates/openshell-cli/Cargo.toml | 1 + crates/openshell-cli/src/main.rs | 46 ++ crates/openshell-prover/Cargo.toml | 25 + .../registry/apis/github.yaml | 62 +++ .../registry/binaries/claude.yaml | 27 + .../registry/binaries/curl.yaml | 17 + .../registry/binaries/gh.yaml | 16 + .../registry/binaries/git.yaml | 25 + .../registry/binaries/nc.yaml | 15 + .../registry/binaries/node.yaml | 18 + .../registry/binaries/python3.yaml | 21 + .../registry/binaries/ssh.yaml | 15 + .../registry/binaries/wget.yaml | 14 + crates/openshell-prover/src/accepted_risks.rs | 171 ++++++ crates/openshell-prover/src/credentials.rs | 242 ++++++++ crates/openshell-prover/src/finding.rs | 67 +++ crates/openshell-prover/src/lib.rs | 228 ++++++++ crates/openshell-prover/src/model.rs | 393 +++++++++++++ crates/openshell-prover/src/policy.rs | 428 +++++++++++++++ crates/openshell-prover/src/queries.rs | 263 +++++++++ crates/openshell-prover/src/registry.rs | 316 +++++++++++ crates/openshell-prover/src/report.rs | 390 +++++++++++++ .../testdata/accepted-risks.yaml | 4 + .../testdata/credentials.yaml | 9 + .../testdata/empty-policy.yaml | 1 + crates/openshell-prover/testdata/policy.yaml | 47 ++ 29 files changed, 3240 insertions(+), 140 deletions(-) create mode 100644 crates/openshell-prover/Cargo.toml create mode 100644 crates/openshell-prover/registry/apis/github.yaml create mode 100644 crates/openshell-prover/registry/binaries/claude.yaml create mode 100644 crates/openshell-prover/registry/binaries/curl.yaml create mode 100644 crates/openshell-prover/registry/binaries/gh.yaml create mode 100644 crates/openshell-prover/registry/binaries/git.yaml create mode 100644 crates/openshell-prover/registry/binaries/nc.yaml create mode 100644 crates/openshell-prover/registry/binaries/node.yaml create mode 100644 crates/openshell-prover/registry/binaries/python3.yaml create mode 100644 crates/openshell-prover/registry/binaries/ssh.yaml create mode 100644 crates/openshell-prover/registry/binaries/wget.yaml create mode 100644 crates/openshell-prover/src/accepted_risks.rs create mode 100644 crates/openshell-prover/src/credentials.rs create mode 100644 crates/openshell-prover/src/finding.rs create mode 100644 crates/openshell-prover/src/lib.rs create mode 100644 crates/openshell-prover/src/model.rs create mode 100644 crates/openshell-prover/src/policy.rs create mode 100644 crates/openshell-prover/src/queries.rs create mode 100644 crates/openshell-prover/src/registry.rs create mode 100644 crates/openshell-prover/src/report.rs create mode 100644 crates/openshell-prover/testdata/accepted-risks.yaml create mode 100644 crates/openshell-prover/testdata/credentials.yaml create mode 100644 crates/openshell-prover/testdata/empty-policy.yaml create mode 100644 crates/openshell-prover/testdata/policy.yaml diff --git a/.gitignore b/.gitignore index a6e6eb3cc..d6b4fa356 100644 --- a/.gitignore +++ b/.gitignore @@ -201,3 +201,4 @@ architecture/plans .claude/worktrees/ rfc.md .worktrees +.z3-trace diff --git a/Cargo.lock b/Cargo.lock index c290e1074..035ce7449 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -35,7 +35,7 @@ checksum = "b169f7a6d4742236a0a00c541b845991d0ac43e546831af1249753ab4c3aa3a0" dependencies = [ "cfg-if", "cipher", - "cpufeatures", + "cpufeatures 0.2.17", ] [[package]] @@ -153,7 +153,7 @@ checksum = "3c3610892ee6e0cbce8ae2700349fcf8f98adb0dbfbee85aec3c9179d29cc072" dependencies = [ "base64ct", "blake2", - "cpufeatures", + "cpufeatures 0.2.17", "password-hash", ] @@ -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" @@ -584,9 +611,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.57" +version = "1.2.59" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a0dd1ca384932ff3641c8718a02769f1698e7563dc6974ffd03346116310423" +checksum = "b7a4d3ec6524d28a329fc53654bbadc9bdd7b0431f5d65f1a56ffb28a1ee5283" dependencies = [ "find-msvc-tools", "jobserver", @@ -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" @@ -614,7 +650,7 @@ checksum = "c3613f74bd2eac03dad61bd53dbe620703d4371614fe0bc3b9f04dd36fe4e818" dependencies = [ "cfg-if", "cipher", - "cpufeatures", + "cpufeatures 0.2.17", ] [[package]] @@ -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" @@ -695,9 +742,9 @@ checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9" [[package]] name = "cmake" -version = "0.1.57" +version = "0.1.58" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75443c44cd6b379beb8c5b45d85d0773baf31cce901fe7bb252f4eff3008ef7d" +checksum = "c0f78a02292a74a88ac736019ab962ece0bc380e3f977bf72e376c5d78ff0678" dependencies = [ "cc", ] @@ -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" @@ -797,6 +850,15 @@ dependencies = [ "libc", ] +[[package]] +name = "cpufeatures" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8b2a41393f66f16b0823bb79094d54ac5fbd34ab292ddafb9a0456ac9f87d201" +dependencies = [ + "libc", +] + [[package]] name = "crc" version = "3.4.0" @@ -869,7 +931,7 @@ checksum = "829d955a0bb380ef178a640b91779e3987da38c9aea133b20614cfed8cdea9c6" dependencies = [ "bitflags", "crossterm_winapi", - "mio 1.1.1", + "mio 1.2.0", "parking_lot", "rustix 0.38.44", "signal-hook", @@ -966,7 +1028,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "97fb8b7c4503de7d6ae7b42ab72a5a59857b4c937ec27a3d4539dba95b5ab2be" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.2.17", "curve25519-dalek-derive", "digest 0.10.7", "fiat-crypto", @@ -1045,6 +1107,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" @@ -1310,9 +1378,9 @@ dependencies = [ [[package]] name = "fastrand" -version = "2.3.0" +version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37909eebbb50d72f9059c3b6d82c0463f2ff062c9e95845c43a6c9c0355411be" +checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6" [[package]] name = "ff" @@ -1361,6 +1429,7 @@ checksum = "843fba2746e448b37e26a819579957415c8cef339bf08564fe8b7ddbd959573c" dependencies = [ "crc32fast", "miniz_oxide", + "zlib-rs", ] [[package]] @@ -1556,10 +1625,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 +1649,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" @@ -1613,7 +1690,7 @@ dependencies = [ "futures-core", "futures-sink", "http", - "indexmap 2.13.0", + "indexmap 2.14.0", "slab", "tokio", "tokio-util", @@ -1649,9 +1726,9 @@ dependencies = [ [[package]] name = "hashbrown" -version = "0.16.1" +version = "0.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" +checksum = "4f467dd6dccf739c208452f8014c75c18bb8301b050ad1cfb27153803edb0f51" [[package]] name = "hashlink" @@ -1797,18 +1874,18 @@ checksum = "df3b46402a9d5adb4c86a0cf463f42e19994e3ee891101b1841f30a545cb49a9" [[package]] name = "hybrid-array" -version = "0.4.8" +version = "0.4.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8655f91cd07f2b9d0c24137bd650fe69617773435ee5ec83022377777ce65ef1" +checksum = "3944cf8cf766b40e2a1a333ee5e9b563f854d5fa49d6a8ca2764e97c6eddb214" dependencies = [ "typenum", ] [[package]] name = "hyper" -version = "1.8.1" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ab2d4f250c3d7b1c9fcdff1cece94ea4e2dfbec68614f7b87cb205f24ca9d11" +checksum = "6299f016b246a94207e63da54dbe807655bf9e00044f73ded42c3ac5305fbcca" dependencies = [ "atomic-waker", "bytes", @@ -1821,7 +1898,6 @@ dependencies = [ "httpdate", "itoa", "pin-project-lite", - "pin-utils", "smallvec", "tokio", "want", @@ -1938,12 +2014,13 @@ dependencies = [ [[package]] name = "icu_collections" -version = "2.1.1" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c6b649701667bbe825c3b7e6388cb521c23d88644678e83c0c4d0a621a34b43" +checksum = "2984d1cd16c883d7935b9e07e44071dca8d917fd52ecc02c04d5fa0b5a3f191c" dependencies = [ "displaydoc", "potential_utf", + "utf8_iter", "yoke", "zerofrom", "zerovec", @@ -1951,9 +2028,9 @@ dependencies = [ [[package]] name = "icu_locale_core" -version = "2.1.1" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "edba7861004dd3714265b4db54a3c390e880ab658fec5f7db895fae2046b5bb6" +checksum = "92219b62b3e2b4d88ac5119f8904c10f8f61bf7e95b640d25ba3075e6cac2c29" dependencies = [ "displaydoc", "litemap", @@ -1964,9 +2041,9 @@ dependencies = [ [[package]] name = "icu_normalizer" -version = "2.1.1" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f6c8828b67bf8908d82127b2054ea1b4427ff0230ee9141c54251934ab1b599" +checksum = "c56e5ee99d6e3d33bd91c5d85458b6005a22140021cc324cea84dd0e72cff3b4" dependencies = [ "icu_collections", "icu_normalizer_data", @@ -1978,15 +2055,15 @@ dependencies = [ [[package]] name = "icu_normalizer_data" -version = "2.1.1" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7aedcccd01fc5fe81e6b489c15b247b8b0690feb23304303a9e560f37efc560a" +checksum = "da3be0ae77ea334f4da67c12f149704f19f81d1adf7c51cf482943e84a2bad38" [[package]] name = "icu_properties" -version = "2.1.2" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "020bfc02fe870ec3a66d93e677ccca0562506e5872c650f893269e08615d74ec" +checksum = "bee3b67d0ea5c2cca5003417989af8996f8604e34fb9ddf96208a033901e70de" dependencies = [ "icu_collections", "icu_locale_core", @@ -1998,15 +2075,15 @@ dependencies = [ [[package]] name = "icu_properties_data" -version = "2.1.2" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "616c294cf8d725c6afcd8f55abc17c56464ef6211f9ed59cccffe534129c77af" +checksum = "8e2bbb201e0c04f7b4b3e14382af113e17ba4f63e2c9d2ee626b720cbce54a14" [[package]] name = "icu_provider" -version = "2.1.1" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85962cf0ce02e1e0a629cc34e7ca3e373ce20dda4c4d7294bbd0bf1fdb59e614" +checksum = "139c4cf31c8b5f33d7e199446eff9c1e02decfc2f0eec2c8d71f65befa45b421" dependencies = [ "displaydoc", "icu_locale_core", @@ -2062,12 +2139,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.13.0" +version = "2.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7714e70437a7dc3ac8eb7e6f8df75fd8eb422675fc7678aff7364301092b1017" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" dependencies = [ "equivalent", - "hashbrown 0.16.1", + "hashbrown 0.17.0", "serde", "serde_core", ] @@ -2125,7 +2202,7 @@ dependencies = [ "rsa 0.10.0-rc.12", "sec1", "sha1 0.10.6", - "sha1 0.11.0-rc.5", + "sha1 0.11.0", "sha2 0.10.9", "signature 2.2.0", "signature 3.0.0-rc.6", @@ -2143,9 +2220,9 @@ checksum = "d98f6fed1fde3f8c21bc40a1abb88dd75e67924f9cffc3ef95607bad8017f8e2" [[package]] name = "iri-string" -version = "0.7.11" +version = "0.7.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d8e7418f59cc01c88316161279a7f665217ae316b388e58a0d10e29f54f1e5eb" +checksum = "25e659a4bb38e810ebc252e53b5814ff908a8c58c2a9ce2fae1bbec24cbf4e20" dependencies = [ "memchr", "serde", @@ -2217,10 +2294,12 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.91" +version = "0.3.94" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b49715b7073f385ba4bc528e5747d02e66cb39c6146efb66b781f131f0fb399c" +checksum = "2e04e2ef80ce82e13552136fabeef8a5ed1f985a96805761cbb9a2c34e7664d9" dependencies = [ + "cfg-if", + "futures-util", "once_cell", "wasm-bindgen", ] @@ -2396,11 +2475,17 @@ 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" +version = "0.2.184" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" +checksum = "48f5d2a454e16a5ea0f4ced81bd44e4cfc7bd3a507b61887c99fd3538b28e4af" [[package]] name = "libcrux-intrinsics" @@ -2486,14 +2571,14 @@ checksum = "b6d2cec3eae94f9f509c767b45932f1ada8350c4bdb85af2fcab4a3c14807981" [[package]] name = "libredox" -version = "0.1.15" +version = "0.1.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7ddbf48fd451246b1f8c2610bd3b4ac0cc6e149d89832867093ab69a17194f08" +checksum = "e02f3bb43d335493c96bf3fd3a321600bf6bd07ed34bc64118e9293bdffea46c" dependencies = [ "bitflags", "libc", "plain", - "redox_syscall 0.7.3", + "redox_syscall 0.7.4", ] [[package]] @@ -2531,9 +2616,9 @@ checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" [[package]] name = "litemap" -version = "0.8.1" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77" +checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0" [[package]] name = "lock_api" @@ -2565,6 +2650,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" @@ -2644,6 +2738,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" @@ -2668,9 +2768,9 @@ dependencies = [ [[package]] name = "mio" -version = "1.1.1" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a69bcab0ad47271a0234d9422b131806bf3968021e5dc9328caf2d4cd58557fc" +checksum = "50b7e5b27aa02a74bac8c3f23f448f8d87ff11f92d3aac1a6ed369ee08cc56c1" dependencies = [ "libc", "log", @@ -2705,6 +2805,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" @@ -2714,6 +2824,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" @@ -2742,6 +2866,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.1" @@ -2768,6 +2901,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" @@ -2862,6 +3006,7 @@ dependencies = [ "openshell-bootstrap", "openshell-core", "openshell-policy", + "openshell-prover", "openshell-providers", "openshell-tui", "owo-colors", @@ -2925,6 +3070,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" @@ -3336,7 +3496,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3672b37090dbd86368a4145bc067582552b29c27377cad4e0a306c97f9bd7772" dependencies = [ "fixedbitset", - "indexmap 2.13.0", + "indexmap 2.14.0", ] [[package]] @@ -3379,12 +3539,6 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" -[[package]] -name = "pin-utils" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b870d8c151b6f2fb93e84a13146138f05d02ed11c7e7c54f8826aaaf7c9f184" - [[package]] name = "pkcs1" version = "0.7.5" @@ -3403,7 +3557,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "986d2e952779af96ea048f160fd9194e1751b4faea78bcf3ceb456efe008088e" dependencies = [ "der 0.8.0", - "spki 0.8.0-rc.4", + "spki 0.8.0", ] [[package]] @@ -3440,7 +3594,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "12922b6296c06eb741b02d7b5161e3aaa22864af38dfa025a1a3ba3f68c84577" dependencies = [ "der 0.8.0", - "spki 0.8.0-rc.4", + "spki 0.8.0", ] [[package]] @@ -3461,7 +3615,7 @@ version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8159bd90725d2df49889a078b54f4f79e87f1f8a8444194cdca81d38f5393abf" dependencies = [ - "cpufeatures", + "cpufeatures 0.2.17", "opaque-debug", "universal-hash", ] @@ -3473,7 +3627,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9d1fe60d06143b2430aa532c94cfe9e29783047f06c0d7fd359a9a51b729fa25" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.2.17", "opaque-debug", "universal-hash", ] @@ -3486,9 +3640,9 @@ checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49" [[package]] name = "potential_utf" -version = "0.1.4" +version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b73949432f5e2a09657003c25bca5e19a0e9c84f8058ca374f49e0ebe605af77" +checksum = "0103b1cef7ec0cf76490e969665504990193874ea05c85ff9bab8b911d0a0564" dependencies = [ "zerovec", ] @@ -3499,6 +3653,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" @@ -3804,9 +3964,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.7.3" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ce70a74e890531977d37e532c34d45e9055d2409ed08ddba14529471ed0be16" +checksum = "f450ad9c3b1da563fb6948a8e0fb0fb9269711c9c73d9ea1de5058c79c8d643a" dependencies = [ "bitflags", ] @@ -3868,7 +4028,9 @@ checksum = "eddd3ca559203180a307f12d114c268abf583f59b03cb906fd0b3ff8646c1147" dependencies = [ "base64 0.22.1", "bytes", + "futures-channel", "futures-core", + "futures-util", "http", "http-body", "http-body-util", @@ -3955,9 +4117,9 @@ dependencies = [ "pkcs1 0.8.0-rc.4", "pkcs8 0.11.0-rc.11", "rand_core 0.10.0-rc-3", - "sha2 0.11.0-rc.5", + "sha2 0.11.0", "signature 3.0.0-rc.6", - "spki 0.8.0-rc.4", + "spki 0.8.0", "zeroize", ] @@ -4056,9 +4218,9 @@ checksum = "b50b8869d9fc858ce7266cce0194bd74df58b9d0e3f6df3a9fc8eb470d95c09d" [[package]] name = "rustc-hash" -version = "2.1.1" +version = "2.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "357703d41365b4b27c590e3ed91eabb1b663f07c4c084095e60cbed4362dff0d" +checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe" [[package]] name = "rustc_version" @@ -4281,9 +4443,9 @@ dependencies = [ [[package]] name = "semver" -version = "1.0.27" +version = "1.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d767eb0aabc880b29956c35734170f26ed551a859dbd361d140cdbeca61ab1e2" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" [[package]] name = "serde" @@ -4389,7 +4551,7 @@ version = "0.9.34+deprecated" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47" dependencies = [ - "indexmap 2.13.0", + "indexmap 2.14.0", "itoa", "ryu", "serde", @@ -4402,7 +4564,7 @@ version = "0.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "59e2dd588bf1597a252c3b920e0143eb99b0f76e4e082f4c92ce34fbc9e71ddd" dependencies = [ - "indexmap 2.13.0", + "indexmap 2.14.0", "itoa", "libyml", "memchr", @@ -4428,18 +4590,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e3bf829a2d51ab4a5ddf1352d8470c140cadc8301b2ae1789db023f01cedd6ba" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.2.17", "digest 0.10.7", ] [[package]] name = "sha1" -version = "0.11.0-rc.5" +version = "0.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b167252f3c126be0d8926639c4c4706950f01445900c4b3db0fd7e89fcb750a" +checksum = "aacc4cc499359472b4abe1bf11d0b12e688af9a805fa5e3016f9a386dc2d0214" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.3.0", "digest 0.11.2", ] @@ -4450,18 +4612,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.2.17", "digest 0.10.7", ] [[package]] name = "sha2" -version = "0.11.0-rc.5" +version = "0.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c5f3b1e2dc8aad28310d8410bd4d7e180eca65fca176c52ab00d364475d0024" +checksum = "446ba717509524cb3f22f17ecc096f10f4822d76ab5c0b9822c5f9c284e825f4" dependencies = [ "cfg-if", - "cpufeatures", + "cpufeatures 0.3.0", "digest 0.11.2", ] @@ -4510,7 +4672,7 @@ checksum = "b75a19a7a740b25bc7944bdee6172368f988763b744e3d4dfe753f6b4ece40cc" dependencies = [ "libc", "mio 0.8.11", - "mio 1.1.1", + "mio 1.2.0", "signal-hook", ] @@ -4546,9 +4708,9 @@ dependencies = [ [[package]] name = "simd-adler32" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e320a6c5ad31d271ad523dcf3ad13e2767ad8b1cb8f047f75a8aeaf8da139da2" +checksum = "703d5c7ef118737c72f1af64ad2f6f8c5e1921f818cdcb97b8fe6fc69bf66214" [[package]] name = "slab" @@ -4606,9 +4768,9 @@ dependencies = [ [[package]] name = "spki" -version = "0.8.0-rc.4" +version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8baeff88f34ed0691978ec34440140e1572b68c7dd4a495fd14a3dc1944daa80" +checksum = "1d9efca8738c78ee9484207732f728b1ef517bbb1833d6fc0879ca898a522f6f" dependencies = [ "base64ct", "der 0.8.0", @@ -4645,7 +4807,7 @@ dependencies = [ "futures-util", "hashbrown 0.15.5", "hashlink", - "indexmap 2.13.0", + "indexmap 2.14.0", "log", "memchr", "once_cell", @@ -5005,7 +5167,7 @@ dependencies = [ "cfg-if", "libc", "memchr", - "mio 1.1.1", + "mio 1.2.0", "terminal-trx", "windows-sys 0.61.2", "xterm-color", @@ -5099,6 +5261,7 @@ checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c" dependencies = [ "deranged", "itoa", + "js-sys", "num-conv", "powerfmt", "serde_core", @@ -5124,9 +5287,9 @@ dependencies = [ [[package]] name = "tinystr" -version = "0.8.2" +version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "42d3e9c45c09de15d06dd8acf5f4e0e399e85927b7f00711024eb7ae10fa4869" +checksum = "c8323304221c2a851516f22236c5722a72eaa19749016521d6dff0824447d96d" dependencies = [ "displaydoc", "zerovec", @@ -5170,13 +5333,13 @@ dependencies = [ [[package]] name = "tokio" -version = "1.50.0" +version = "1.51.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "27ad5e34374e03cfffefc301becb44e9dc3c17584f414349ebe29ed26661822d" +checksum = "f66bf9585cda4b724d3e78ab34b73fb2bbaba9011b9bfdf69dc836382ea13b8c" dependencies = [ "bytes", "libc", - "mio 1.1.1", + "mio 1.2.0", "parking_lot", "pin-project-lite", "signal-hook-registry", @@ -5187,9 +5350,9 @@ dependencies = [ [[package]] name = "tokio-macros" -version = "2.6.1" +version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5c55a2eff8b69ce66c84f85e1da1c233edc36ceb85a2058d11b0d6a3c7e7569c" +checksum = "385a6cb71ab9ab790c5fe8d67f1645e6c450a7ce006a33de03daa956cf70a496" dependencies = [ "proc-macro2", "quote", @@ -5521,6 +5684,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" @@ -5568,9 +5737,9 @@ checksum = "7df058c713841ad818f1dc5d3fd88063241cc61f49f5fbea4b951e8cf5a8d71d" [[package]] name = "unicode-segmentation" -version = "1.13.1" +version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da36089a805484bcccfffe0739803392c8298778a2d2f09febf76fac5ad9025b" +checksum = "9629274872b2bfaf8d66f5f15725007f635594914870f65218920345aa11aa8c" [[package]] name = "unicode-truncate" @@ -5661,9 +5830,9 @@ checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" [[package]] name = "uuid" -version = "1.22.0" +version = "1.23.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a68d3c8f01c0cfa54a75291d83601161799e4a89a39e0929f4b0354d88757a37" +checksum = "5ac8b6f42ead25368cf5b098aeb3dc8a1a2c05a3eee8a9a1a68c640edbfc79d9" dependencies = [ "getrandom 0.4.2", "js-sys", @@ -5729,9 +5898,9 @@ checksum = "b8dad83b4f25e74f184f64c43b150b91efe7647395b42289f38e50566d82855b" [[package]] name = "wasm-bindgen" -version = "0.2.114" +version = "0.2.117" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6532f9a5c1ece3798cb1c2cfdba640b9b3ba884f5db45973a6f442510a87d38e" +checksum = "0551fc1bb415591e3372d0bc4780db7e587d84e2a7e79da121051c5c4b89d0b0" dependencies = [ "cfg-if", "once_cell", @@ -5742,23 +5911,19 @@ dependencies = [ [[package]] name = "wasm-bindgen-futures" -version = "0.4.64" +version = "0.4.67" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e9c5522b3a28661442748e09d40924dfb9ca614b21c00d3fd135720e48b67db8" +checksum = "03623de6905b7206edd0a75f69f747f134b7f0a2323392d664448bf2d3c5d87e" dependencies = [ - "cfg-if", - "futures-util", "js-sys", - "once_cell", "wasm-bindgen", - "web-sys", ] [[package]] name = "wasm-bindgen-macro" -version = "0.2.114" +version = "0.2.117" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18a2d50fcf105fb33bb15f00e7a77b772945a2ee45dcf454961fd843e74c18e6" +checksum = "7fbdf9a35adf44786aecd5ff89b4563a90325f9da0923236f6104e603c7e86be" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -5766,9 +5931,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.114" +version = "0.2.117" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "03ce4caeaac547cdf713d280eda22a730824dd11e6b8c3ca9e42247b25c631e3" +checksum = "dca9693ef2bab6d4e6707234500350d8dad079eb508dca05530c85dc3a529ff2" dependencies = [ "bumpalo", "proc-macro2", @@ -5779,9 +5944,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.114" +version = "0.2.117" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75a326b8c223ee17883a4251907455a2431acc2791c98c26279376490c378c16" +checksum = "39129a682a6d2d841b6c429d0c51e5cb0ed1a03829d8b3d1e69a011e62cb3d3b" dependencies = [ "unicode-ident", ] @@ -5803,7 +5968,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" dependencies = [ "anyhow", - "indexmap 2.13.0", + "indexmap 2.14.0", "wasm-encoder", "wasmparser", ] @@ -5816,15 +5981,15 @@ checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" dependencies = [ "bitflags", "hashbrown 0.15.5", - "indexmap 2.13.0", + "indexmap 2.14.0", "semver", ] [[package]] name = "web-sys" -version = "0.3.91" +version = "0.3.94" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "854ba17bb104abfb26ba36da9729addc7ce7f06f5c0f90f3c391f8461cca21f9" +checksum = "cd70027e39b12f0849461e08ffc50b9cd7688d942c1c8e3c7b22273236b4dd0a" dependencies = [ "js-sys", "wasm-bindgen", @@ -6282,7 +6447,7 @@ checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" dependencies = [ "anyhow", "heck", - "indexmap 2.13.0", + "indexmap 2.14.0", "prettyplease", "syn 2.0.117", "wasm-metadata", @@ -6313,7 +6478,7 @@ checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" dependencies = [ "anyhow", "bitflags", - "indexmap 2.13.0", + "indexmap 2.14.0", "log", "serde", "serde_derive", @@ -6332,7 +6497,7 @@ checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" dependencies = [ "anyhow", "id-arena", - "indexmap 2.13.0", + "indexmap 2.14.0", "log", "semver", "serde", @@ -6344,9 +6509,9 @@ dependencies = [ [[package]] name = "writeable" -version = "0.6.2" +version = "0.6.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9edde0db4769d2dc68579893f2306b26c6ecfbe0ef499b013d731b7b9247e0b9" +checksum = "1ffae5123b2d3fc086436f8834ae3ab053a283cfac8fe0a0b8eaae044768a4c4" [[package]] name = "xattr" @@ -6375,9 +6540,9 @@ dependencies = [ [[package]] name = "yoke" -version = "0.8.1" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72d6e5c6afb84d73944e5cedb052c4680d5657337201555f9f2a16b7406d4954" +checksum = "abe8c5fda708d9ca3df187cae8bfb9ceda00dd96231bed36e445a1a48e66f9ca" dependencies = [ "stable_deref_trait", "yoke-derive", @@ -6386,9 +6551,9 @@ dependencies = [ [[package]] name = "yoke-derive" -version = "0.8.1" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b659052874eb698efe5b9e8cf382204678a0086ebf46982b79d6ca3182927e5d" +checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e" dependencies = [ "proc-macro2", "quote", @@ -6396,20 +6561,45 @@ 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.47" +version = "0.8.48" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "efbb2a062be311f2ba113ce66f697a4dc589f85e78a4aea276200804cea0ed87" +checksum = "eed437bf9d6692032087e337407a86f04cd8d6a16a37199ed57949d415bd68e9" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.8.47" +version = "0.8.48" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e8bc7269b54418e7aeeef514aa68f8690b8c0489a06b0136e5f57c4c5ccab89" +checksum = "70e3cd084b1788766f53af483dd21f93881ff30d7320490ec3ef7526d203bad4" dependencies = [ "proc-macro2", "quote", @@ -6418,18 +6608,18 @@ dependencies = [ [[package]] name = "zerofrom" -version = "0.1.6" +version = "0.1.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50cc42e0333e05660c3587f3bf9d0478688e15d870fab3346451ce7f8c9fbea5" +checksum = "69faa1f2a1ea75661980b013019ed6687ed0e83d069bc1114e2cc74c6c04c4df" dependencies = [ "zerofrom-derive", ] [[package]] name = "zerofrom-derive" -version = "0.1.6" +version = "0.1.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d71e5d6e06ab090c67b5e44993ec16b72dcbaabc526db883a360057678b48502" +checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1" dependencies = [ "proc-macro2", "quote", @@ -6459,9 +6649,9 @@ dependencies = [ [[package]] name = "zerotrie" -version = "0.2.3" +version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a59c17a5562d507e4b54960e8569ebee33bee890c70aa3fe7b97e85a9fd7851" +checksum = "0f9152d31db0792fa83f70fb2f83148effb5c1f5b8c7686c3459e361d9bc20bf" dependencies = [ "displaydoc", "yoke", @@ -6470,9 +6660,9 @@ dependencies = [ [[package]] name = "zerovec" -version = "0.11.5" +version = "0.11.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c28719294829477f525be0186d13efa9a3c602f7ec202ca9e353d310fb9a002" +checksum = "90f911cbc359ab6af17377d242225f4d75119aec87ea711a880987b18cd7b239" dependencies = [ "yoke", "zerofrom", @@ -6481,21 +6671,66 @@ dependencies = [ [[package]] name = "zerovec-derive" -version = "0.11.2" +version = "0.11.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eadce39539ca5cb3985590102671f2567e659fca9666581ad3411d59207951f3" +checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555" dependencies = [ "proc-macro2", "quote", "syn 2.0.117", ] +[[package]] +name = "zip" +version = "8.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dcab981e19633ebcf0b001ddd37dd802996098bc1864f90b7c5d970ce76c1d59" +dependencies = [ + "aes", + "bzip2", + "constant_time_eq", + "crc32fast", + "deflate64", + "flate2", + "getrandom 0.4.2", + "hmac", + "indexmap 2.14.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" diff --git a/Cargo.toml b/Cargo.toml index 08b699d47..a2b42f2f9 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 ef6d87791..a1c9a0b23 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 1d9305ff6..8d514831e 100644 --- a/crates/openshell-cli/src/main.rs +++ b/crates/openshell-cli/src/main.rs @@ -1478,6 +1478,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)] @@ -1898,6 +1922,27 @@ 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), }) => { @@ -1968,6 +2013,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 000000000..ee8905c57 --- /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 000000000..bfe5e404c --- /dev/null +++ b/crates/openshell-prover/registry/apis/github.yaml @@ -0,0 +1,62 @@ +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 000000000..b1e3c36f5 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/claude.yaml @@ -0,0 +1,27 @@ +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 000000000..ae87e4161 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/curl.yaml @@ -0,0 +1,17 @@ +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 000000000..84fd60bcb --- /dev/null +++ b/crates/openshell-prover/registry/binaries/gh.yaml @@ -0,0 +1,16 @@ +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 000000000..a6e3b732f --- /dev/null +++ b/crates/openshell-prover/registry/binaries/git.yaml @@ -0,0 +1,25 @@ +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 000000000..53a778d5c --- /dev/null +++ b/crates/openshell-prover/registry/binaries/nc.yaml @@ -0,0 +1,15 @@ +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 000000000..f6abaf6d8 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/node.yaml @@ -0,0 +1,18 @@ +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 000000000..f99214fe1 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/python3.yaml @@ -0,0 +1,21 @@ +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 000000000..8dccf3d30 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/ssh.yaml @@ -0,0 +1,15 @@ +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 000000000..6af6f4990 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/wget.yaml @@ -0,0 +1,14 @@ +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 000000000..0881db43c --- /dev/null +++ b/crates/openshell-prover/src/accepted_risks.rs @@ -0,0 +1,171 @@ +// 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_yaml::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 000000000..9dcf69acc --- /dev/null +++ b/crates/openshell-prover/src/credentials.rs @@ -0,0 +1,242 @@ +// 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_yaml::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_yaml::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 000000000..e42d95387 --- /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 000000000..89e684df4 --- /dev/null +++ b/crates/openshell-prover/src/lib.rs @@ -0,0 +1,228 @@ +// 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 000000000..9c5f574ee --- /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 000000000..969a4017b --- /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_yaml::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 000000000..77f571a11 --- /dev/null +++ b/crates/openshell-prover/src/queries.rs @@ -0,0 +1,263 @@ +// 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_allows_write".to_owned(), + format!("L7 allows write methods — {} can POST/PUT data", bpath), + ) + }; + + 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 | PolicyIntent::L4Only) { + 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 000000000..782d798b8 --- /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_yaml::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 000000000..bdc7d9d4f --- /dev/null +++ b/crates/openshell-prover/src/report.rs @@ -0,0 +1,390 @@ +// 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 000000000..cb2358190 --- /dev/null +++ b/crates/openshell-prover/testdata/accepted-risks.yaml @@ -0,0 +1,4 @@ +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 000000000..71039ee51 --- /dev/null +++ b/crates/openshell-prover/testdata/credentials.yaml @@ -0,0 +1,9 @@ +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 000000000..b82551848 --- /dev/null +++ b/crates/openshell-prover/testdata/empty-policy.yaml @@ -0,0 +1 @@ +version: 1 diff --git a/crates/openshell-prover/testdata/policy.yaml b/crates/openshell-prover/testdata/policy.yaml new file mode 100644 index 000000000..76aaaf691 --- /dev/null +++ b/crates/openshell-prover/testdata/policy.yaml @@ -0,0 +1,47 @@ +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* } From 7d269ba0df6db79644fc690d8d1838c29a26c554 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 2 Apr 2026 14:08:47 -0700 Subject: [PATCH 02/11] fix(prover): skip L7-write in exfil, write bypass only on read-only intent Port two fixes from the Python branch: - Exfil query skips endpoints where L7 is enforced and working - Write bypass only fires on explicit read-only intent, not L4-only Signed-off-by: Alexander Watson --- crates/openshell-prover/src/queries.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/crates/openshell-prover/src/queries.rs b/crates/openshell-prover/src/queries.rs index 77f571a11..90379b13f 100644 --- a/crates/openshell-prover/src/queries.rs +++ b/crates/openshell-prover/src/queries.rs @@ -49,10 +49,9 @@ pub fn check_data_exfiltration(model: &ReachabilityModel) -> Vec { ), ) } else { - ( - "l7_allows_write".to_owned(), - format!("L7 allows write methods — {} can POST/PUT data", bpath), - ) + // L7 is enforced and allows write — policy is + // working as intended. Not a finding. + continue; }; if !cap.exfil_mechanism.is_empty() { @@ -133,7 +132,7 @@ pub fn check_write_bypass(model: &ReachabilityModel) -> Vec { 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 | PolicyIntent::L4Only) { + if !matches!(intent, PolicyIntent::ReadOnly) { continue; } From 5891857e9418ae8fff9b93a1b917e0bb248d7942 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Fri, 3 Apr 2026 21:13:53 -0700 Subject: [PATCH 03/11] chore(prover): add missing SPDX license headers to registry and testdata YAML files --- crates/openshell-prover/registry/apis/github.yaml | 3 +++ crates/openshell-prover/registry/binaries/claude.yaml | 3 +++ crates/openshell-prover/registry/binaries/curl.yaml | 3 +++ crates/openshell-prover/registry/binaries/gh.yaml | 3 +++ crates/openshell-prover/registry/binaries/git.yaml | 3 +++ crates/openshell-prover/registry/binaries/nc.yaml | 3 +++ crates/openshell-prover/registry/binaries/node.yaml | 3 +++ crates/openshell-prover/registry/binaries/python3.yaml | 3 +++ crates/openshell-prover/registry/binaries/ssh.yaml | 3 +++ crates/openshell-prover/registry/binaries/wget.yaml | 3 +++ crates/openshell-prover/testdata/accepted-risks.yaml | 3 +++ crates/openshell-prover/testdata/credentials.yaml | 3 +++ crates/openshell-prover/testdata/empty-policy.yaml | 3 +++ crates/openshell-prover/testdata/policy.yaml | 3 +++ 14 files changed, 42 insertions(+) diff --git a/crates/openshell-prover/registry/apis/github.yaml b/crates/openshell-prover/registry/apis/github.yaml index bfe5e404c..78fa15c93 100644 --- a/crates/openshell-prover/registry/apis/github.yaml +++ b/crates/openshell-prover/registry/apis/github.yaml @@ -1,3 +1,6 @@ +# 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 diff --git a/crates/openshell-prover/registry/binaries/claude.yaml b/crates/openshell-prover/registry/binaries/claude.yaml index b1e3c36f5..e9d1b1d31 100644 --- a/crates/openshell-prover/registry/binaries/claude.yaml +++ b/crates/openshell-prover/registry/binaries/claude.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/curl.yaml b/crates/openshell-prover/registry/binaries/curl.yaml index ae87e4161..4cfadb8ac 100644 --- a/crates/openshell-prover/registry/binaries/curl.yaml +++ b/crates/openshell-prover/registry/binaries/curl.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/gh.yaml b/crates/openshell-prover/registry/binaries/gh.yaml index 84fd60bcb..8ad7cb392 100644 --- a/crates/openshell-prover/registry/binaries/gh.yaml +++ b/crates/openshell-prover/registry/binaries/gh.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/git.yaml b/crates/openshell-prover/registry/binaries/git.yaml index a6e3b732f..2c3480cbe 100644 --- a/crates/openshell-prover/registry/binaries/git.yaml +++ b/crates/openshell-prover/registry/binaries/git.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/nc.yaml b/crates/openshell-prover/registry/binaries/nc.yaml index 53a778d5c..8f98d7639 100644 --- a/crates/openshell-prover/registry/binaries/nc.yaml +++ b/crates/openshell-prover/registry/binaries/nc.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/node.yaml b/crates/openshell-prover/registry/binaries/node.yaml index f6abaf6d8..cfa83f2be 100644 --- a/crates/openshell-prover/registry/binaries/node.yaml +++ b/crates/openshell-prover/registry/binaries/node.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/python3.yaml b/crates/openshell-prover/registry/binaries/python3.yaml index f99214fe1..3cdf9cd3b 100644 --- a/crates/openshell-prover/registry/binaries/python3.yaml +++ b/crates/openshell-prover/registry/binaries/python3.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/ssh.yaml b/crates/openshell-prover/registry/binaries/ssh.yaml index 8dccf3d30..b53065d88 100644 --- a/crates/openshell-prover/registry/binaries/ssh.yaml +++ b/crates/openshell-prover/registry/binaries/ssh.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/registry/binaries/wget.yaml b/crates/openshell-prover/registry/binaries/wget.yaml index 6af6f4990..0741998b7 100644 --- a/crates/openshell-prover/registry/binaries/wget.yaml +++ b/crates/openshell-prover/registry/binaries/wget.yaml @@ -1,3 +1,6 @@ +# 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: diff --git a/crates/openshell-prover/testdata/accepted-risks.yaml b/crates/openshell-prover/testdata/accepted-risks.yaml index cb2358190..6af5c7146 100644 --- a/crates/openshell-prover/testdata/accepted-risks.yaml +++ b/crates/openshell-prover/testdata/accepted-risks.yaml @@ -1,3 +1,6 @@ +# 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." diff --git a/crates/openshell-prover/testdata/credentials.yaml b/crates/openshell-prover/testdata/credentials.yaml index 71039ee51..b186ccf9a 100644 --- a/crates/openshell-prover/testdata/credentials.yaml +++ b/crates/openshell-prover/testdata/credentials.yaml @@ -1,3 +1,6 @@ +# 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 diff --git a/crates/openshell-prover/testdata/empty-policy.yaml b/crates/openshell-prover/testdata/empty-policy.yaml index b82551848..458bab0e4 100644 --- a/crates/openshell-prover/testdata/empty-policy.yaml +++ b/crates/openshell-prover/testdata/empty-policy.yaml @@ -1 +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 index 76aaaf691..e98d95319 100644 --- a/crates/openshell-prover/testdata/policy.yaml +++ b/crates/openshell-prover/testdata/policy.yaml @@ -1,3 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + version: 1 filesystem_policy: From 843bb42987ba7078dc6bc906b96c2ba1f9f13fd0 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Fri, 3 Apr 2026 21:35:44 -0700 Subject: [PATCH 04/11] fix(prover): revert serde_yaml to serde_yml to match workspace dependency on main --- crates/openshell-prover/src/accepted_risks.rs | 2 +- crates/openshell-prover/src/credentials.rs | 4 ++-- crates/openshell-prover/src/policy.rs | 6 +++--- crates/openshell-prover/src/registry.rs | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/crates/openshell-prover/src/accepted_risks.rs b/crates/openshell-prover/src/accepted_risks.rs index 0881db43c..cc844f918 100644 --- a/crates/openshell-prover/src/accepted_risks.rs +++ b/crates/openshell-prover/src/accepted_risks.rs @@ -57,7 +57,7 @@ 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_yaml::from_str(&contents) + let raw: AcceptedRisksFile = serde_yml::from_str(&contents) .into_diagnostic() .wrap_err("parsing accepted risks YAML")?; diff --git a/crates/openshell-prover/src/credentials.rs b/crates/openshell-prover/src/credentials.rs index 9dcf69acc..18c7b6005 100644 --- a/crates/openshell-prover/src/credentials.rs +++ b/crates/openshell-prover/src/credentials.rs @@ -158,7 +158,7 @@ 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_yaml::from_str(&contents) + let raw: CredentialsFile = serde_yml::from_str(&contents) .into_diagnostic() .wrap_err("parsing credentials YAML")?; @@ -180,7 +180,7 @@ 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_yaml::from_str(&contents) + let raw: ApiRegistryDef = serde_yml::from_str(&contents) .into_diagnostic() .wrap_err_with(|| format!("parsing API registry {}", path.display()))?; diff --git a/crates/openshell-prover/src/policy.rs b/crates/openshell-prover/src/policy.rs index 969a4017b..01aa4a794 100644 --- a/crates/openshell-prover/src/policy.rs +++ b/crates/openshell-prover/src/policy.rs @@ -60,10 +60,10 @@ struct PolicyFile { // Ignored fields the prover does not need. #[serde(default)] #[allow(dead_code)] - landlock: Option, + landlock: Option, #[serde(default)] #[allow(dead_code)] - process: Option, + process: Option, } #[derive(Debug, Deserialize)] @@ -359,7 +359,7 @@ pub fn parse_policy(path: &Path) -> Result { /// Parse a policy YAML string into a [`PolicyModel`]. pub fn parse_policy_str(yaml: &str) -> Result { - let raw: PolicyFile = serde_yaml::from_str(yaml) + let raw: PolicyFile = serde_yml::from_str(yaml) .into_diagnostic() .wrap_err("parsing policy YAML")?; diff --git a/crates/openshell-prover/src/registry.rs b/crates/openshell-prover/src/registry.rs index 782d798b8..0ae5e5352 100644 --- a/crates/openshell-prover/src/registry.rs +++ b/crates/openshell-prover/src/registry.rs @@ -255,7 +255,7 @@ 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_yaml::from_str(&contents) + let raw: BinaryCapabilityDef = serde_yml::from_str(&contents) .into_diagnostic() .wrap_err_with(|| format!("parsing binary descriptor {}", path.display()))?; From 378a04b3fa83cf68d77125d16d481e0476e5ee9a Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Fri, 3 Apr 2026 21:38:20 -0700 Subject: [PATCH 05/11] fix(prover): apply cargo fmt formatting to prover and cli source files --- crates/openshell-cli/src/main.rs | 15 +++++++------- crates/openshell-prover/src/accepted_risks.rs | 5 +---- crates/openshell-prover/src/credentials.rs | 5 +---- crates/openshell-prover/src/lib.rs | 17 ++++++++-------- crates/openshell-prover/src/queries.rs | 20 ++++++------------- crates/openshell-prover/src/report.rs | 5 ++++- 6 files changed, 29 insertions(+), 38 deletions(-) diff --git a/crates/openshell-cli/src/main.rs b/crates/openshell-cli/src/main.rs index 8d514831e..ee2ad767b 100644 --- a/crates/openshell-cli/src/main.rs +++ b/crates/openshell-cli/src/main.rs @@ -1923,13 +1923,14 @@ async fn main() -> Result<()> { // Top-level policy (was `sandbox policy`) // ----------------------------------------------------------- Some(Commands::Policy { - command: Some(PolicyCommands::Prove { - policy, - credentials, - registry, - accepted_risks, - compact, - }), + command: + Some(PolicyCommands::Prove { + policy, + credentials, + registry, + accepted_risks, + compact, + }), }) => { // Prove runs locally — no gateway needed. let exit_code = openshell_prover::prove( diff --git a/crates/openshell-prover/src/accepted_risks.rs b/crates/openshell-prover/src/accepted_risks.rs index cc844f918..61aa025be 100644 --- a/crates/openshell-prover/src/accepted_risks.rs +++ b/crates/openshell-prover/src/accepted_risks.rs @@ -106,10 +106,7 @@ fn path_matches_risk(path: &FindingPath, risk: &AcceptedRisk) -> bool { /// 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 { +pub fn apply_accepted_risks(findings: Vec, accepted: &[AcceptedRisk]) -> Vec { if accepted.is_empty() { return findings; } diff --git a/crates/openshell-prover/src/credentials.rs b/crates/openshell-prover/src/credentials.rs index 18c7b6005..ca068bcad 100644 --- a/crates/openshell-prover/src/credentials.rs +++ b/crates/openshell-prover/src/credentials.rs @@ -213,10 +213,7 @@ fn load_api_registry(path: &Path) -> Result { /// 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 { +pub fn load_credential_set(credentials_path: &Path, registry_dir: &Path) -> Result { let creds = load_credentials(credentials_path)?; let mut api_registries = HashMap::new(); diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs index 89e684df4..6a9acaf16 100644 --- a/crates/openshell-prover/src/lib.rs +++ b/crates/openshell-prover/src/lib.rs @@ -50,7 +50,9 @@ pub fn prove( 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")) + std::borrow::Cow::Owned( + std::env::current_dir().unwrap_or_default().join("registry"), + ) } }); @@ -177,8 +179,7 @@ filesystem_policy: 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 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); @@ -198,9 +199,10 @@ filesystem_policy: // At least one critical or high finding. assert!( - findings - .iter() - .any(|f| matches!(f.risk, finding::RiskLevel::Critical | finding::RiskLevel::High)), + findings.iter().any(|f| matches!( + f.risk, + finding::RiskLevel::Critical | finding::RiskLevel::High + )), "expected at least one critical/high finding" ); } @@ -213,8 +215,7 @@ filesystem_policy: 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 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); diff --git a/crates/openshell-prover/src/queries.rs b/crates/openshell-prover/src/queries.rs index 90379b13f..ab301474e 100644 --- a/crates/openshell-prover/src/queries.rs +++ b/crates/openshell-prover/src/queries.rs @@ -99,14 +99,10 @@ pub fn check_data_exfiltration(model: &ReachabilityModel) -> Vec { .to_owned(), ); } - remediation.push( - "Restrict filesystem read access to only the paths the agent needs.".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 paths: Vec = exfil_paths.into_iter().map(FindingPath::Exfil).collect(); let n_paths = paths.len(); vec![Finding { @@ -142,8 +138,7 @@ pub fn check_write_bypass(model: &ReachabilityModel) -> Vec { // Check: binary bypasses L7 and can write if cap.bypasses_l7() && cap.can_write() { - let cred_actions = - collect_credential_actions(model, &ep.host, &cap); + let cred_actions = collect_credential_actions(model, &ep.host, &cap); if !cred_actions.is_empty() || model.credentials.credentials_for_host(&ep.host).is_empty() { @@ -161,8 +156,7 @@ pub fn check_write_bypass(model: &ReachabilityModel) -> Vec { // 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); + let cred_actions = collect_credential_actions(model, &ep.host, &cap); if !cred_actions.is_empty() { bypass_paths.push(WriteBypassPath { binary: b.path.clone(), @@ -193,9 +187,7 @@ pub fn check_write_bypass(model: &ReachabilityModel) -> Vec { 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." - ), + description: format!("{n} path(s) allow write operations despite read-only policy intent."), risk: RiskLevel::High, paths, remediation: vec![ diff --git a/crates/openshell-prover/src/report.rs b/crates/openshell-prover/src/report.rs index bdc7d9d4f..27207a6ae 100644 --- a/crates/openshell-prover/src/report.rs +++ b/crates/openshell-prover/src/report.rs @@ -283,7 +283,10 @@ pub fn render_report(findings: &[Finding], policy_path: &str, credentials_path: risk_label(finding.risk).dimmed(), finding.title.dimmed() ); - println!(" {}", format!("Reason: {}", finding.accepted_reason).dimmed()); + println!( + " {}", + format!("Reason: {}", finding.accepted_reason).dimmed() + ); println!(); } } From d9ee70d94c8a0b5bea78ca66c576a55dc8a72cc0 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Wed, 8 Apr 2026 10:10:01 -0700 Subject: [PATCH 06/11] ci: add clang and libclang-dev to CI image for z3-sys bindgen z3-sys requires libclang at build time for bindgen to generate FFI bindings. Without it, the Rust CI jobs fail on the prover crate. --- deploy/docker/Dockerfile.ci | 2 ++ 1 file changed, 2 insertions(+) diff --git a/deploy/docker/Dockerfile.ci b/deploy/docker/Dockerfile.ci index fe3241cb3..eab46c19b 100644 --- a/deploy/docker/Dockerfile.ci +++ b/deploy/docker/Dockerfile.ci @@ -23,6 +23,8 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ curl \ git \ build-essential \ + clang \ + libclang-dev \ pkg-config \ libssl-dev \ openssh-client \ From 7f0c65fa0bd73df4632cacc27fa876ba0015efd9 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 9 Apr 2026 14:26:48 -0700 Subject: [PATCH 07/11] fix(prover): use system libz3 instead of compiling from source MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add libz3-dev to the CI image and drop the z3 `bundled` feature from the workspace dependency. This eliminates the ~30 min z3 C++ build that ran on every CI cache miss. sccache only wraps rustc — it does not intercept the cmake C++ build that z3-sys runs when `bundled` is enabled. The cargo target cache helped on warm runs but evicts on toolchain bumps and fork PRs. With the system library pre-installed in the CI image, z3 link time is always zero. A `bundled-z3` opt-in feature is added to the prover crate for local development without system z3: cargo build -p openshell-prover --features bundled-z3 Regular local dev: brew install z3 (macOS) or apt install libz3-dev (Linux), then cargo build just works. Signed-off-by: Alexander Watson Made-with: Cursor --- Cargo.lock | 25 +++++++++++++++++++++---- Cargo.toml | 10 ++++++++-- crates/openshell-prover/Cargo.toml | 9 +++++---- deploy/docker/Dockerfile.ci | 1 + 4 files changed, 35 insertions(+), 10 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 035ce7449..e09c2583a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2127,6 +2127,25 @@ dependencies = [ "icu_properties", ] +[[package]] +name = "include_dir" +version = "0.7.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "923d117408f1e49d914f1a379a309cffe4f18c05cf4e3d12e613a15fc81bd0dd" +dependencies = [ + "include_dir_macros", +] + +[[package]] +name = "include_dir_macros" +version = "0.7.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7cab85a7ed0bd5f0e76d93846e0147172bed2e2d3f859bcc33a8d9699cad1a75" +dependencies = [ + "proc-macro2", + "quote", +] + [[package]] name = "indexmap" version = "1.9.3" @@ -3074,14 +3093,12 @@ dependencies = [ name = "openshell-prover" version = "0.0.0" dependencies = [ + "glob", + "include_dir", "miette", - "openshell-core", - "openshell-policy", "owo-colors", "serde", "serde_yml", - "thiserror 2.0.18", - "tracing", "z3", ] diff --git a/Cargo.toml b/Cargo.toml index a2b42f2f9..b51aee3c2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -75,6 +75,12 @@ tokio-tungstenite = { version = "0.26", features = ["rustls-tls-native-roots"] } # Clipboard (OSC 52) base64 = "0.22" +# Filesystem embedding +include_dir = "0.7" + +# Glob matching +glob = "0.3" + # Utilities futures = "0.3" bytes = "1" @@ -94,8 +100,8 @@ k8s-openapi = { version = "0.21.1", features = ["v1_26"] } # IDs uuid = { version = "1.10", features = ["v4"] } -# SMT solver -z3 = { version = "0.19", features = ["bundled"] } +# SMT solver (uses system libz3; enable z3/bundled via the prover's bundled-z3 feature for local dev without system z3) +z3 = "0.19" [workspace.lints.rust] unsafe_code = "warn" diff --git a/crates/openshell-prover/Cargo.toml b/crates/openshell-prover/Cargo.toml index ee8905c57..ee815f3a3 100644 --- a/crates/openshell-prover/Cargo.toml +++ b/crates/openshell-prover/Cargo.toml @@ -10,16 +10,17 @@ rust-version.workspace = true license.workspace = true repository.workspace = true +[features] +bundled-z3 = ["z3/bundled"] + [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 } +include_dir = { workspace = true } +glob = { workspace = true } [lints] workspace = true diff --git a/deploy/docker/Dockerfile.ci b/deploy/docker/Dockerfile.ci index eab46c19b..b09c93e11 100644 --- a/deploy/docker/Dockerfile.ci +++ b/deploy/docker/Dockerfile.ci @@ -25,6 +25,7 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ build-essential \ clang \ libclang-dev \ + libz3-dev \ pkg-config \ libssl-dev \ openssh-client \ From 4e7ecba17ee5b7749d2585254151dcff1ba32452 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 9 Apr 2026 14:26:57 -0700 Subject: [PATCH 08/11] fix(prover): use u16 for ports, align include_workdir default with runtime Port fields changed from u32 to u16 across all prover types (policy, model, finding, queries). Prevents the prover from silently accepting port values >65535 that the runtime rejects, which would produce misleading PASS results on invalid policies. Change include_workdir serde default from true to false to match the runtime (openshell-policy uses #[serde(default)] which gives false). The previous mismatch caused the prover to model a /sandbox path that does not exist at runtime, producing false analysis. Signed-off-by: Alexander Watson Made-with: Cursor --- crates/openshell-prover/src/finding.rs | 4 ++-- crates/openshell-prover/src/model.rs | 2 +- crates/openshell-prover/src/policy.rs | 18 +++++++----------- crates/openshell-prover/src/queries.rs | 2 +- 4 files changed, 11 insertions(+), 15 deletions(-) diff --git a/crates/openshell-prover/src/finding.rs b/crates/openshell-prover/src/finding.rs index e42d95387..ab4d4f47f 100644 --- a/crates/openshell-prover/src/finding.rs +++ b/crates/openshell-prover/src/finding.rs @@ -26,7 +26,7 @@ impl fmt::Display for RiskLevel { pub struct ExfilPath { pub binary: String, pub endpoint_host: String, - pub endpoint_port: u32, + pub endpoint_port: u16, pub mechanism: String, pub policy_name: String, /// One of `"l4_only"`, `"l7_allows_write"`, `"l7_bypassed"`. @@ -38,7 +38,7 @@ pub struct ExfilPath { pub struct WriteBypassPath { pub binary: String, pub endpoint_host: String, - pub endpoint_port: u32, + pub endpoint_port: u16, pub policy_name: String, pub policy_intent: String, /// One of `"l4_only"`, `"l7_bypass_protocol"`, `"credential_write_scope"`. diff --git a/crates/openshell-prover/src/model.rs b/crates/openshell-prover/src/model.rs index 9c5f574ee..b96e7fef2 100644 --- a/crates/openshell-prover/src/model.rs +++ b/crates/openshell-prover/src/model.rs @@ -17,7 +17,7 @@ use crate::registry::BinaryRegistry; pub struct EndpointId { pub policy_name: String, pub host: String, - pub port: u32, + pub port: u16, } impl EndpointId { diff --git a/crates/openshell-prover/src/policy.rs b/crates/openshell-prover/src/policy.rs index 01aa4a794..b116fd5b0 100644 --- a/crates/openshell-prover/src/policy.rs +++ b/crates/openshell-prover/src/policy.rs @@ -68,7 +68,7 @@ struct PolicyFile { #[derive(Debug, Deserialize)] struct FilesystemDef { - #[serde(default = "default_true")] + #[serde(default)] include_workdir: bool, #[serde(default)] read_only: Vec, @@ -76,10 +76,6 @@ struct FilesystemDef { read_write: Vec, } -fn default_true() -> bool { - true -} - #[derive(Debug, Deserialize)] struct NetworkPolicyRuleDef { #[serde(default)] @@ -95,9 +91,9 @@ struct EndpointDef { #[serde(default)] host: String, #[serde(default)] - port: u32, + port: u16, #[serde(default)] - ports: Vec, + ports: Vec, #[serde(default)] protocol: String, #[serde(default)] @@ -148,8 +144,8 @@ pub struct L7Rule { #[derive(Debug, Clone)] pub struct Endpoint { pub host: String, - pub port: u32, - pub ports: Vec, + pub port: u16, + pub ports: Vec, pub protocol: String, pub tls: String, pub enforcement: String, @@ -195,7 +191,7 @@ impl Endpoint { } /// The effective list of ports for this endpoint. - pub fn effective_ports(&self) -> Vec { + pub fn effective_ports(&self) -> Vec { if !self.ports.is_empty() { return self.ports.clone(); } @@ -263,7 +259,7 @@ pub struct FilesystemPolicy { impl Default for FilesystemPolicy { fn default() -> Self { Self { - include_workdir: true, + include_workdir: false, read_only: Vec::new(), read_write: Vec::new(), } diff --git a/crates/openshell-prover/src/queries.rs b/crates/openshell-prover/src/queries.rs index ab301474e..001255cea 100644 --- a/crates/openshell-prover/src/queries.rs +++ b/crates/openshell-prover/src/queries.rs @@ -217,7 +217,7 @@ pub fn run_all_queries(model: &ReachabilityModel) -> Vec { // --------------------------------------------------------------------------- /// Check whether an endpoint in the policy is L7-enforced. -fn is_endpoint_l7_enforced(policy: &crate::policy::PolicyModel, host: &str, port: u32) -> bool { +fn is_endpoint_l7_enforced(policy: &crate::policy::PolicyModel, host: &str, port: u16) -> bool { for rule in policy.network_policies.values() { for ep in &rule.endpoints { if ep.host == host && ep.effective_ports().contains(&port) { From bf217d11010521cce09f1c54e62b2f531e6830c7 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 9 Apr 2026 14:27:08 -0700 Subject: [PATCH 09/11] refactor(prover): embed registry at compile time, replace hand-rolled glob MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Embed binary and API capability registry YAML files into the binary at compile time using include_dir!. The previous approach used env!("CARGO_MANIFEST_DIR") which bakes in the build machine's source path — works in tests but breaks for installed binaries. The CWD fallback was equally fragile. The --registry CLI flag still works as a filesystem override for custom registries. Credentials remain filesystem-loaded (user-supplied data). Replace the hand-rolled glob matching (~60 lines) with the glob crate's Pattern::matches(), which is already a transitive dependency. Remove unused dependencies: openshell-policy, openshell-core, thiserror, tracing. The prover parses policy YAML directly into its own types and does not use the policy or core crate APIs. Signed-off-by: Alexander Watson Made-with: Cursor --- crates/openshell-prover/src/credentials.rs | 56 +++++++--- crates/openshell-prover/src/lib.rs | 67 +++++------ crates/openshell-prover/src/registry.rs | 123 +++++++-------------- 3 files changed, 111 insertions(+), 135 deletions(-) diff --git a/crates/openshell-prover/src/credentials.rs b/crates/openshell-prover/src/credentials.rs index ca068bcad..dffbc2e8b 100644 --- a/crates/openshell-prover/src/credentials.rs +++ b/crates/openshell-prover/src/credentials.rs @@ -175,14 +175,10 @@ pub fn load_credentials(path: &Path) -> Result> { .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) +fn parse_api_registry(contents: &str, source: &str) -> Result { + let raw: ApiRegistryDef = serde_yml::from_str(contents) .into_diagnostic() - .wrap_err_with(|| format!("parsing API registry {}", path.display()))?; + .wrap_err_with(|| format!("parsing API registry {source}"))?; let scope_capabilities = raw .scope_capabilities @@ -210,12 +206,24 @@ fn load_api_registry(path: &Path) -> Result { }) } -/// 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)?; +fn load_embedded_api_registries() -> Result> { + let registry = crate::registry::embedded_registry(); + let mut api_registries = HashMap::new(); + if let Some(dir) = registry.get_dir("apis") { + for file in dir.files() { + if file.path().extension().is_some_and(|ext| ext == "yaml") { + let contents = file.contents_utf8().ok_or_else(|| { + miette::miette!("non-UTF8 API registry file: {}", file.path().display()) + })?; + let api = parse_api_registry(contents, &file.path().display().to_string())?; + api_registries.insert(api.api.clone(), api); + } + } + } + Ok(api_registries) +} +fn load_api_registries_from_dir(registry_dir: &Path) -> Result> { let mut api_registries = HashMap::new(); let apis_dir = registry_dir.join("apis"); if apis_dir.is_dir() { @@ -226,12 +234,34 @@ pub fn load_credential_set(credentials_path: &Path, registry_dir: &Path) -> Resu let entry = entry.into_diagnostic()?; let path = entry.path(); if path.extension().is_some_and(|ext| ext == "yaml") { - let api = load_api_registry(&path)?; + let contents = std::fs::read_to_string(&path) + .into_diagnostic() + .wrap_err_with(|| format!("reading {}", path.display()))?; + let api = parse_api_registry(&contents, &path.display().to_string())?; api_registries.insert(api.api.clone(), api); } } } + Ok(api_registries) +} +/// Load credentials with API registries from the embedded registry. +pub fn load_credential_set_embedded(credentials_path: &Path) -> Result { + let creds = load_credentials(credentials_path)?; + let api_registries = load_embedded_api_registries()?; + Ok(CredentialSet { + credentials: creds, + api_registries, + }) +} + +/// Load credentials with API registries from a filesystem directory override. +pub fn load_credential_set_from_dir( + credentials_path: &Path, + registry_dir: &Path, +) -> Result { + let creds = load_credentials(credentials_path)?; + let api_registries = load_api_registries_from_dir(registry_dir)?; Ok(CredentialSet { credentials: creds, api_registries, diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs index 6a9acaf16..10a4d3535 100644 --- a/crates/openshell-prover/src/lib.rs +++ b/crates/openshell-prover/src/lib.rs @@ -21,11 +21,9 @@ 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. @@ -33,6 +31,9 @@ use report::{render_compact, render_report}; /// - `0` — pass (no critical/high findings, or all accepted) /// - `1` — fail (critical or high findings present) /// - `2` — input error +/// +/// Binary and API capability registries are embedded at compile time. +/// Pass `registry_dir` to override with a custom filesystem registry. pub fn prove( policy_path: &str, credentials_path: &str, @@ -40,39 +41,30 @@ pub fn prove( 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)?; + let (credential_set, binary_registry) = match registry_dir { + Some(dir) => { + let dir = Path::new(dir); + ( + credentials::load_credential_set_from_dir(Path::new(credentials_path), dir)?, + registry::load_binary_registry_from_dir(dir)?, + ) + } + None => ( + credentials::load_credential_set_embedded(Path::new(credentials_path))?, + registry::load_embedded_binary_registry()?, + ), + }; - // 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 { @@ -95,10 +87,6 @@ mod tests { 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() { @@ -118,14 +106,12 @@ mod tests { 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. + // 3. Workdir NOT included by default (matches runtime behavior). #[test] fn test_include_workdir_default() { let yaml = r#" @@ -136,7 +122,7 @@ filesystem_policy: "#; let model = policy::parse_policy_str(yaml).expect("parse"); let readable = model.filesystem_policy.readable_paths(); - assert!(readable.contains(&"/sandbox".to_owned())); + assert!(!readable.contains(&"/sandbox".to_owned())); } // 4. Workdir excluded when include_workdir: false. @@ -171,21 +157,20 @@ filesystem_policy: assert_eq!(sandbox_count, 1); } - // 6. End-to-end: git push bypass findings detected. + // 6. End-to-end: git push bypass findings detected (uses embedded registry). #[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 cred_set = + credentials::load_credential_set_embedded(&creds_path).expect("load creds"); + let bin_reg = registry::load_embedded_binary_registry().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!( @@ -196,8 +181,6 @@ filesystem_policy: query_types.contains("write_bypass"), "expected write_bypass finding" ); - - // At least one critical or high finding. assert!( findings.iter().any(|f| matches!( f.risk, @@ -212,11 +195,11 @@ filesystem_policy: 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 cred_set = + credentials::load_credential_set_embedded(&creds_path).expect("load creds"); + let bin_reg = registry::load_embedded_binary_registry().expect("load registry"); let z3_model = model::build_model(pol, cred_set, bin_reg); let findings = queries::run_all_queries(&z3_model); diff --git a/crates/openshell-prover/src/registry.rs b/crates/openshell-prover/src/registry.rs index 0ae5e5352..c51caef05 100644 --- a/crates/openshell-prover/src/registry.rs +++ b/crates/openshell-prover/src/registry.rs @@ -3,13 +3,18 @@ //! Binary capability registry — loads YAML descriptors that describe what each //! binary can do (protocols, exfiltration, HTTP construction, etc.). +//! +//! The built-in registry is embedded at compile time via `include_dir!`. +//! A filesystem override can be provided at runtime for custom registries. use std::collections::HashMap; -use std::path::Path; +use include_dir::{include_dir, Dir}; use miette::{IntoDiagnostic, Result, WrapErr}; use serde::Deserialize; +static EMBEDDED_REGISTRY: Dir<'_> = include_dir!("$CARGO_MANIFEST_DIR/registry"); + // --------------------------------------------------------------------------- // Serde types // --------------------------------------------------------------------------- @@ -164,13 +169,15 @@ impl BinaryRegistry { 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(); + if reg_path.contains('*') { + if let Ok(pattern) = glob::Pattern::new(reg_path) { + if pattern.matches(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(), @@ -183,81 +190,14 @@ impl BinaryRegistry { } } -/// 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) +fn parse_binary_capability(contents: &str, source: &str) -> Result { + let raw: BinaryCapabilityDef = serde_yml::from_str(contents) .into_diagnostic() - .wrap_err_with(|| format!("parsing binary descriptor {}", path.display()))?; + .wrap_err_with(|| format!("parsing binary descriptor {source}"))?; let protocols = raw .protocols @@ -293,10 +233,25 @@ fn load_binary_capability(path: &Path) -> Result { }) } -/// Load all binary capability descriptors from a registry directory. -/// -/// Expects `{registry_dir}/binaries/*.yaml`. -pub fn load_binary_registry(registry_dir: &Path) -> Result { +/// Load binary registry from the compile-time embedded registry data. +pub fn load_embedded_binary_registry() -> Result { + let mut binaries = HashMap::new(); + if let Some(dir) = EMBEDDED_REGISTRY.get_dir("binaries") { + for file in dir.files() { + if file.path().extension().is_some_and(|ext| ext == "yaml") { + let contents = file.contents_utf8().ok_or_else(|| { + miette::miette!("non-UTF8 registry file: {}", file.path().display()) + })?; + let cap = parse_binary_capability(contents, &file.path().display().to_string())?; + binaries.insert(cap.path.clone(), cap); + } + } + } + Ok(BinaryRegistry { binaries }) +} + +/// Load binary registry from a filesystem directory override. +pub fn load_binary_registry_from_dir(registry_dir: &std::path::Path) -> Result { let mut binaries = HashMap::new(); let binaries_dir = registry_dir.join("binaries"); if binaries_dir.is_dir() { @@ -307,10 +262,18 @@ pub fn load_binary_registry(registry_dir: &Path) -> Result { let entry = entry.into_diagnostic()?; let path = entry.path(); if path.extension().is_some_and(|ext| ext == "yaml") { - let cap = load_binary_capability(&path)?; + let contents = std::fs::read_to_string(&path) + .into_diagnostic() + .wrap_err_with(|| format!("reading {}", path.display()))?; + let cap = parse_binary_capability(&contents, &path.display().to_string())?; binaries.insert(cap.path.clone(), cap); } } } Ok(BinaryRegistry { binaries }) } + +/// Accessor for the embedded registry (used by credentials module for API descriptors). +pub fn embedded_registry() -> &'static Dir<'static> { + &EMBEDDED_REGISTRY +} From 1b1a99e919a042c49c46adc92b63226266f77a57 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 9 Apr 2026 14:27:57 -0700 Subject: [PATCH 10/11] docs: add Z3 system library to prerequisites The prover crate now links against system libz3 instead of compiling from source. Document the install steps for macOS, Ubuntu, and Fedora, and note the bundled-z3 feature flag as a fallback. Signed-off-by: Alexander Watson Made-with: Cursor --- CONTRIBUTING.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 7adb3cc4e..52e67d00b 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -119,6 +119,28 @@ Project requirements: - Rust 1.88+ - Python 3.12+ - Docker (running) +- Z3 solver library (for the policy prover crate) + +### Z3 installation + +The `openshell-prover` crate links against the system Z3 library via pkg-config. + +```bash +# macOS +brew install z3 + +# Ubuntu / Debian +sudo apt install libz3-dev + +# Fedora +sudo dnf install z3-devel +``` + +If you prefer not to install Z3 system-wide, you can compile it from source as a one-time step: + +```bash +cargo build -p openshell-prover --features bundled-z3 +``` ## Getting Started From 72428551a9e56ed3179e2f58b7e691109c935906 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Thu, 9 Apr 2026 14:46:06 -0700 Subject: [PATCH 11/11] fix(prover): apply cargo fmt formatting Made-with: Cursor --- crates/openshell-prover/src/lib.rs | 6 ++---- crates/openshell-prover/src/registry.rs | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs index 10a4d3535..feff7d1d5 100644 --- a/crates/openshell-prover/src/lib.rs +++ b/crates/openshell-prover/src/lib.rs @@ -164,8 +164,7 @@ filesystem_policy: let creds_path = testdata_dir().join("credentials.yaml"); let pol = policy::parse_policy(&policy_path).expect("parse policy"); - let cred_set = - credentials::load_credential_set_embedded(&creds_path).expect("load creds"); + let cred_set = credentials::load_credential_set_embedded(&creds_path).expect("load creds"); let bin_reg = registry::load_embedded_binary_registry().expect("load registry"); let z3_model = model::build_model(pol, cred_set, bin_reg); @@ -197,8 +196,7 @@ filesystem_policy: let creds_path = testdata_dir().join("credentials.yaml"); let pol = policy::parse_policy(&policy_path).expect("parse policy"); - let cred_set = - credentials::load_credential_set_embedded(&creds_path).expect("load creds"); + let cred_set = credentials::load_credential_set_embedded(&creds_path).expect("load creds"); let bin_reg = registry::load_embedded_binary_registry().expect("load registry"); let z3_model = model::build_model(pol, cred_set, bin_reg); diff --git a/crates/openshell-prover/src/registry.rs b/crates/openshell-prover/src/registry.rs index c51caef05..3acd52f82 100644 --- a/crates/openshell-prover/src/registry.rs +++ b/crates/openshell-prover/src/registry.rs @@ -9,7 +9,7 @@ use std::collections::HashMap; -use include_dir::{include_dir, Dir}; +use include_dir::{Dir, include_dir}; use miette::{IntoDiagnostic, Result, WrapErr}; use serde::Deserialize;