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/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 diff --git a/Cargo.lock b/Cargo.lock index c290e1074..e09c2583a 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", @@ -2050,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" @@ -2062,12 +2158,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 +2221,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 +2239,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 +2313,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 +2494,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 +2590,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 +2635,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 +2669,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 +2757,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 +2787,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 +2824,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 +2843,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 +2885,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 +2920,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 +3025,7 @@ dependencies = [ "openshell-bootstrap", "openshell-core", "openshell-policy", + "openshell-prover", "openshell-providers", "openshell-tui", "owo-colors", @@ -2925,6 +3089,19 @@ dependencies = [ "serde_yml", ] +[[package]] +name = "openshell-prover" +version = "0.0.0" +dependencies = [ + "glob", + "include_dir", + "miette", + "owo-colors", + "serde", + "serde_yml", + "z3", +] + [[package]] name = "openshell-providers" version = "0.0.0" @@ -3336,7 +3513,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 +3556,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 +3574,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 +3611,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 +3632,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 +3644,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 +3657,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 +3670,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 +3981,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 +4045,9 @@ checksum = "eddd3ca559203180a307f12d114c268abf583f59b03cb906fd0b3ff8646c1147" dependencies = [ "base64 0.22.1", "bytes", + "futures-channel", "futures-core", + "futures-util", "http", "http-body", "http-body-util", @@ -3955,9 +4134,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 +4235,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 +4460,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 +4568,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 +4581,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 +4607,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 +4629,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 +4689,7 @@ checksum = "b75a19a7a740b25bc7944bdee6172368f988763b744e3d4dfe753f6b4ece40cc" dependencies = [ "libc", "mio 0.8.11", - "mio 1.1.1", + "mio 1.2.0", "signal-hook", ] @@ -4546,9 +4725,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 +4785,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 +4824,7 @@ dependencies = [ "futures-util", "hashbrown 0.15.5", "hashlink", - "indexmap 2.13.0", + "indexmap 2.14.0", "log", "memchr", "once_cell", @@ -5005,7 +5184,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 +5278,7 @@ checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c" dependencies = [ "deranged", "itoa", + "js-sys", "num-conv", "powerfmt", "serde_core", @@ -5124,9 +5304,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 +5350,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 +5367,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 +5701,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 +5754,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 +5847,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 +5915,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 +5928,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 +5948,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 +5961,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 +5985,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 +5998,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 +6464,7 @@ checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" dependencies = [ "anyhow", "heck", - "indexmap 2.13.0", + "indexmap 2.14.0", "prettyplease", "syn 2.0.117", "wasm-metadata", @@ -6313,7 +6495,7 @@ checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" dependencies = [ "anyhow", "bitflags", - "indexmap 2.13.0", + "indexmap 2.14.0", "log", "serde", "serde_derive", @@ -6332,7 +6514,7 @@ checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" dependencies = [ "anyhow", "id-arena", - "indexmap 2.13.0", + "indexmap 2.14.0", "log", "semver", "serde", @@ -6344,9 +6526,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 +6557,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 +6568,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 +6578,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 +6625,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 +6666,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 +6677,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 +6688,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..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,6 +100,9 @@ k8s-openapi = { version = "0.21.1", features = ["v1_26"] } # IDs uuid = { version = "1.10", features = ["v4"] } +# 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" 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..ee2ad767b 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,28 @@ async fn main() -> Result<()> { // ----------------------------------------------------------- // Top-level policy (was `sandbox policy`) // ----------------------------------------------------------- + Some(Commands::Policy { + command: + Some(PolicyCommands::Prove { + policy, + credentials, + registry, + accepted_risks, + compact, + }), + }) => { + // Prove runs locally — no gateway needed. + let exit_code = openshell_prover::prove( + &policy, + &credentials, + registry.as_deref(), + accepted_risks.as_deref(), + compact, + )?; + if exit_code != 0 { + std::process::exit(exit_code); + } + } Some(Commands::Policy { command: Some(policy_cmd), }) => { @@ -1968,6 +2014,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..ee815f3a3 --- /dev/null +++ b/crates/openshell-prover/Cargo.toml @@ -0,0 +1,26 @@ +# 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 + +[features] +bundled-z3 = ["z3/bundled"] + +[dependencies] +z3 = { workspace = true } +serde = { workspace = true } +serde_yml = { workspace = true } +miette = { workspace = true } +owo-colors = { workspace = true } +include_dir = { workspace = true } +glob = { 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..78fa15c93 --- /dev/null +++ b/crates/openshell-prover/registry/apis/github.yaml @@ -0,0 +1,65 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +api: github +host: api.github.com +port: 443 +credential_type: github-pat + +scope_capabilities: + repo: + - { method: GET, path: "/repos/**", action: read_repo } + - { method: GET, path: "/user/repos", action: list_repos } + - { method: POST, path: "/repos/*/issues", action: create_issue } + - { method: POST, path: "/repos/*/issues/*/comments", action: comment_issue } + - { method: POST, path: "/repos/*/pulls", action: create_pr } + - { method: PUT, path: "/repos/*/contents/**", action: write_file } + - { method: DELETE, path: "/repos/*/contents/**", action: delete_file } + - { method: DELETE, path: "/repos/*/*", action: delete_repo } + - { method: POST, path: "/repos/*/git/**", action: write_git_data } + - { method: POST, path: "/repos/*/forks", action: fork_repo } + - { method: PATCH, path: "/repos/*/*", action: update_repo } + - { method: POST, path: "/repos/*/releases", action: create_release } + - { method: POST, path: "/repos/*/dispatches", action: trigger_workflow } + "read:org": + - { method: GET, path: "/orgs/**", action: read_org } + - { method: GET, path: "/user/orgs", action: list_orgs } + "write:org": + - { method: GET, path: "/orgs/**", action: read_org } + - { method: POST, path: "/orgs/*/repos", action: create_org_repo } + - { method: PUT, path: "/orgs/*/memberships/**", action: manage_members } + gist: + - { method: GET, path: "/gists/**", action: read_gists } + - { method: POST, path: "/gists", action: create_gist } + - { method: PATCH, path: "/gists/*", action: update_gist } + - { method: DELETE, path: "/gists/*", action: delete_gist } + "admin:repo_hook": + - { method: GET, path: "/repos/*/hooks/**", action: read_hooks } + - { method: POST, path: "/repos/*/hooks", action: create_hook } + - { method: DELETE, path: "/repos/*/hooks/*", action: delete_hook } + +action_risk: + read_repo: low + list_repos: low + create_issue: medium + comment_issue: medium + create_pr: medium + write_file: high + delete_file: high + delete_repo: critical + write_git_data: high + fork_repo: medium + update_repo: high + create_release: high + trigger_workflow: critical + read_org: low + list_orgs: low + create_org_repo: high + manage_members: critical + read_gists: low + create_gist: medium + update_gist: medium + delete_gist: medium + read_hooks: low + create_hook: critical + delete_hook: high diff --git a/crates/openshell-prover/registry/binaries/claude.yaml b/crates/openshell-prover/registry/binaries/claude.yaml new file mode 100644 index 000000000..e9d1b1d31 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/claude.yaml @@ -0,0 +1,30 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/local/bin/claude +description: "Claude Code CLI — AI coding agent" +protocols: + - name: anthropic-api + transport: https + description: "Anthropic API calls for inference" + bypasses_l7: false + actions: + - { name: inference, type: write, description: "Send prompts and receive completions" } + - name: http-via-tools + transport: https + description: "Claude can make HTTP requests via tool use (Bash, WebFetch)" + bypasses_l7: false + actions: + - { name: get, type: read } + - { name: post, type: write } + - { name: put, type: write } +spawns: + - /usr/local/bin/node + - /usr/local/bin/python3.13 + - /usr/bin/git + - /usr/bin/curl + - /usr/bin/ssh + - /usr/bin/nc +can_exfiltrate: true +exfil_mechanism: "Can read files and send contents via tool use, API calls, or spawned subprocesses" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/curl.yaml b/crates/openshell-prover/registry/binaries/curl.yaml new file mode 100644 index 000000000..4cfadb8ac --- /dev/null +++ b/crates/openshell-prover/registry/binaries/curl.yaml @@ -0,0 +1,20 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/curl +description: "Command-line HTTP client" +protocols: + - name: http + transport: https + description: "HTTP/HTTPS requests — can construct arbitrary method, path, headers, body" + bypasses_l7: false + actions: + - { name: get, type: read, description: "HTTP GET request" } + - { name: post, type: write, description: "HTTP POST with arbitrary body" } + - { name: put, type: write, description: "HTTP PUT with arbitrary body" } + - { name: delete, type: destructive, description: "HTTP DELETE request" } + - { name: upload, type: write, description: "File upload via multipart POST" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "POST/PUT file contents to any reachable endpoint, or encode in URL query parameters" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/gh.yaml b/crates/openshell-prover/registry/binaries/gh.yaml new file mode 100644 index 000000000..8ad7cb392 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/gh.yaml @@ -0,0 +1,19 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/gh +description: "GitHub CLI — REST API client for GitHub" +protocols: + - name: github-rest + transport: https + description: "GitHub REST API via gh cli — uses standard HTTP, subject to L7 inspection" + bypasses_l7: false + actions: + - { name: api_read, type: read, description: "GET requests to GitHub API" } + - { name: api_write, type: write, description: "POST/PUT/PATCH requests (create issues, PRs, etc.)" } + - { name: api_delete, type: destructive, description: "DELETE requests (delete repos, branches, etc.)" } +spawns: + - /usr/bin/git +can_exfiltrate: true +exfil_mechanism: "Create gists, issues, or PRs with file contents" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/git.yaml b/crates/openshell-prover/registry/binaries/git.yaml new file mode 100644 index 000000000..2c3480cbe --- /dev/null +++ b/crates/openshell-prover/registry/binaries/git.yaml @@ -0,0 +1,28 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/git +description: "Distributed version control system" +protocols: + - name: git-smart-http + transport: https + description: "Git smart HTTP protocol over HTTPS CONNECT tunnel — not REST, bypasses L7 HTTP inspection" + bypasses_l7: true + actions: + - { name: clone, type: read, description: "Clone/fetch repository" } + - { name: push, type: write, description: "Push commits to remote" } + - { name: force_push, type: destructive, description: "Force push, rewriting remote history" } + - name: git-ssh + transport: ssh + description: "Git over SSH" + bypasses_l7: true + actions: + - { name: clone, type: read } + - { name: push, type: write } + - { name: force_push, type: destructive } +spawns: + - /usr/lib/git-core/git-remote-https + - /usr/bin/ssh +can_exfiltrate: true +exfil_mechanism: "Commit data to repo and push, or encode in branch/tag names" +can_construct_http: false diff --git a/crates/openshell-prover/registry/binaries/nc.yaml b/crates/openshell-prover/registry/binaries/nc.yaml new file mode 100644 index 000000000..8f98d7639 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/nc.yaml @@ -0,0 +1,18 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/nc +description: "Netcat — arbitrary TCP/UDP connections" +protocols: + - name: raw-tcp + transport: tcp + description: "Raw TCP connection — can send/receive arbitrary data" + bypasses_l7: true + actions: + - { name: connect, type: read, description: "Establish TCP connection" } + - { name: send, type: write, description: "Send arbitrary data over TCP" } + - { name: listen, type: read, description: "Listen for incoming connections" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "Stream arbitrary data over raw TCP connection" +can_construct_http: false diff --git a/crates/openshell-prover/registry/binaries/node.yaml b/crates/openshell-prover/registry/binaries/node.yaml new file mode 100644 index 000000000..cfa83f2be --- /dev/null +++ b/crates/openshell-prover/registry/binaries/node.yaml @@ -0,0 +1,21 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/local/bin/node +description: "Node.js runtime — general-purpose JavaScript runtime" +protocols: + - name: http-programmatic + transport: https + description: "Node can construct arbitrary HTTP requests via fetch, axios, http module" + bypasses_l7: false + actions: + - { name: get, type: read } + - { name: post, type: write } + - { name: put, type: write } + - { name: delete, type: destructive } +spawns: + - /usr/bin/curl + - /usr/bin/git +can_exfiltrate: true +exfil_mechanism: "Construct arbitrary HTTP requests, spawn subprocesses" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/python3.yaml b/crates/openshell-prover/registry/binaries/python3.yaml new file mode 100644 index 000000000..3cdf9cd3b --- /dev/null +++ b/crates/openshell-prover/registry/binaries/python3.yaml @@ -0,0 +1,24 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/local/bin/python3.13 +description: "Python interpreter — general-purpose runtime" +protocols: + - name: http-programmatic + transport: https + description: "Python can construct arbitrary HTTP requests via urllib, httpx, requests" + bypasses_l7: false + actions: + - { name: get, type: read } + - { name: post, type: write } + - { name: put, type: write } + - { name: delete, type: destructive } +spawns: + - /usr/bin/curl + - /usr/bin/git + - /usr/bin/ssh + - /usr/bin/nc + - /usr/bin/wget +can_exfiltrate: true +exfil_mechanism: "Construct arbitrary HTTP requests, write to files, spawn subprocesses" +can_construct_http: true diff --git a/crates/openshell-prover/registry/binaries/ssh.yaml b/crates/openshell-prover/registry/binaries/ssh.yaml new file mode 100644 index 000000000..b53065d88 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/ssh.yaml @@ -0,0 +1,18 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/ssh +description: "OpenSSH client" +protocols: + - name: ssh + transport: ssh + description: "SSH protocol — encrypted tunnel, can forward ports and transfer files" + bypasses_l7: true + actions: + - { name: connect, type: read, description: "SSH shell connection" } + - { name: tunnel, type: write, description: "Port forwarding / tunnel" } + - { name: scp, type: write, description: "File transfer via SCP" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "SCP files or pipe data through SSH tunnel" +can_construct_http: false diff --git a/crates/openshell-prover/registry/binaries/wget.yaml b/crates/openshell-prover/registry/binaries/wget.yaml new file mode 100644 index 000000000..0741998b7 --- /dev/null +++ b/crates/openshell-prover/registry/binaries/wget.yaml @@ -0,0 +1,17 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +binary: /usr/bin/wget +description: "Non-interactive network downloader" +protocols: + - name: http + transport: https + description: "HTTP/HTTPS downloads — can also POST with --post-data" + bypasses_l7: false + actions: + - { name: download, type: read } + - { name: post, type: write, description: "POST via --post-data or --post-file" } +spawns: [] +can_exfiltrate: true +exfil_mechanism: "POST file contents via --post-file to any reachable endpoint" +can_construct_http: true diff --git a/crates/openshell-prover/src/accepted_risks.rs b/crates/openshell-prover/src/accepted_risks.rs new file mode 100644 index 000000000..61aa025be --- /dev/null +++ b/crates/openshell-prover/src/accepted_risks.rs @@ -0,0 +1,168 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Load and match accepted risk annotations against findings. + +use std::path::Path; + +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +use crate::finding::{Finding, FindingPath}; + +// --------------------------------------------------------------------------- +// Serde types +// --------------------------------------------------------------------------- + +#[derive(Debug, Deserialize)] +struct AcceptedRisksFile { + #[serde(default)] + accepted_risks: Vec, +} + +#[derive(Debug, Deserialize)] +struct AcceptedRiskDef { + #[serde(default)] + query: String, + #[serde(default)] + reason: String, + #[serde(default)] + accepted_by: String, + #[serde(default)] + binary: String, + #[serde(default)] + endpoint: String, +} + +// --------------------------------------------------------------------------- +// Public types +// --------------------------------------------------------------------------- + +/// An explicitly accepted risk annotation. +#[derive(Debug, Clone)] +pub struct AcceptedRisk { + pub query: String, + pub reason: String, + pub accepted_by: String, + pub binary: String, + pub endpoint: String, +} + +// --------------------------------------------------------------------------- +// Loading +// --------------------------------------------------------------------------- + +/// Load accepted risks from a YAML file. +pub fn load_accepted_risks(path: &Path) -> Result> { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading accepted risks {}", path.display()))?; + let raw: AcceptedRisksFile = serde_yml::from_str(&contents) + .into_diagnostic() + .wrap_err("parsing accepted risks YAML")?; + + Ok(raw + .accepted_risks + .into_iter() + .map(|r| AcceptedRisk { + query: r.query, + reason: r.reason, + accepted_by: r.accepted_by, + binary: r.binary, + endpoint: r.endpoint, + }) + .collect()) +} + +// --------------------------------------------------------------------------- +// Matching +// --------------------------------------------------------------------------- + +/// Check if a single finding path matches an accepted risk. +fn path_matches_risk(path: &FindingPath, risk: &AcceptedRisk) -> bool { + if !risk.binary.is_empty() { + let path_binary = match path { + FindingPath::Exfil(p) => &p.binary, + FindingPath::WriteBypass(p) => &p.binary, + }; + if path_binary != &risk.binary { + return false; + } + } + if !risk.endpoint.is_empty() { + let endpoint_host = match path { + FindingPath::Exfil(p) => &p.endpoint_host, + FindingPath::WriteBypass(p) => &p.endpoint_host, + }; + if endpoint_host != &risk.endpoint { + return false; + } + } + true +} + +/// Mark findings as accepted where they match accepted risk annotations. +/// +/// A finding is accepted if **all** of its paths match at least one accepted +/// risk entry for that query. If only some paths match, the finding stays +/// active with the unmatched paths. +pub fn apply_accepted_risks(findings: Vec, accepted: &[AcceptedRisk]) -> Vec { + if accepted.is_empty() { + return findings; + } + + let mut result = Vec::new(); + for finding in findings { + let matching_risks: Vec<&AcceptedRisk> = accepted + .iter() + .filter(|r| r.query == finding.query) + .collect(); + + if matching_risks.is_empty() { + result.push(finding); + continue; + } + + if finding.paths.is_empty() { + // Pathless finding — accept if query matches. + result.push(Finding { + accepted: true, + accepted_reason: matching_risks[0].reason.clone(), + ..finding + }); + continue; + } + + let mut unmatched_paths = Vec::new(); + let mut matched_reason = String::new(); + for path in &finding.paths { + let mut path_accepted = false; + for risk in &matching_risks { + if path_matches_risk(path, risk) { + path_accepted = true; + matched_reason.clone_from(&risk.reason); + break; + } + } + if !path_accepted { + unmatched_paths.push(path.clone()); + } + } + + if unmatched_paths.is_empty() { + result.push(Finding { + accepted: true, + accepted_reason: matched_reason, + ..finding + }); + } else if unmatched_paths.len() < finding.paths.len() { + result.push(Finding { + paths: unmatched_paths, + ..finding + }); + } else { + result.push(finding); + } + } + result +} diff --git a/crates/openshell-prover/src/credentials.rs b/crates/openshell-prover/src/credentials.rs new file mode 100644 index 000000000..dffbc2e8b --- /dev/null +++ b/crates/openshell-prover/src/credentials.rs @@ -0,0 +1,269 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Credential descriptors and API capability registries. + +use std::collections::HashMap; +use std::path::Path; + +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +// --------------------------------------------------------------------------- +// Serde types +// --------------------------------------------------------------------------- + +#[derive(Debug, Deserialize)] +struct CredentialsFile { + #[serde(default)] + credentials: Vec, +} + +#[derive(Debug, Deserialize)] +struct CredentialDef { + #[serde(default)] + name: String, + #[serde(default, rename = "type")] + cred_type: String, + #[serde(default)] + scopes: Vec, + #[serde(default)] + injected_via: String, + #[serde(default)] + target_hosts: Vec, +} + +#[derive(Debug, Deserialize)] +struct ApiRegistryDef { + #[serde(default)] + api: String, + #[serde(default)] + host: String, + #[serde(default)] + port: u32, + #[serde(default)] + credential_type: String, + #[serde(default)] + scope_capabilities: HashMap>, + #[serde(default)] + action_risk: HashMap, +} + +#[derive(Debug, Deserialize)] +struct ApiActionDef { + #[serde(default)] + method: String, + #[serde(default)] + path: String, + #[serde(default)] + action: String, +} + +// --------------------------------------------------------------------------- +// Public types +// --------------------------------------------------------------------------- + +/// A credential injected into the sandbox. +#[derive(Debug, Clone)] +pub struct Credential { + pub name: String, + pub cred_type: String, + pub scopes: Vec, + pub injected_via: String, + pub target_hosts: Vec, +} + +/// A single API action (HTTP method + path + semantic name). +#[derive(Debug, Clone)] +pub struct ApiAction { + pub method: String, + pub path: String, + pub action: String, +} + +/// Capability registry for an API (e.g., GitHub REST API). +#[derive(Debug, Clone)] +pub struct ApiCapability { + pub api: String, + pub host: String, + pub port: u32, + pub credential_type: String, + pub scope_capabilities: HashMap>, + pub action_risk: HashMap, +} + +impl ApiCapability { + /// All actions enabled by the given scopes. + pub fn actions_for_scopes(&self, scopes: &[String]) -> Vec<&ApiAction> { + let mut result = Vec::new(); + for scope in scopes { + if let Some(actions) = self.scope_capabilities.get(scope) { + result.extend(actions.iter()); + } + } + result + } + + /// Write actions (POST, PUT, PATCH, DELETE) enabled by the given scopes. + pub fn write_actions_for_scopes(&self, scopes: &[String]) -> Vec<&ApiAction> { + self.actions_for_scopes(scopes) + .into_iter() + .filter(|a| { + let m = a.method.to_uppercase(); + m == "POST" || m == "PUT" || m == "PATCH" || m == "DELETE" + }) + .collect() + } + + /// Destructive actions (high or critical risk) enabled by the given scopes. + pub fn destructive_actions_for_scopes(&self, scopes: &[String]) -> Vec<&ApiAction> { + self.actions_for_scopes(scopes) + .into_iter() + .filter(|a| { + let risk = self.action_risk.get(&a.action).map(String::as_str); + matches!(risk, Some("high" | "critical")) + }) + .collect() + } +} + +/// Combined set of credentials and API registries. +#[derive(Debug, Clone, Default)] +pub struct CredentialSet { + pub credentials: Vec, + pub api_registries: HashMap, +} + +impl CredentialSet { + /// Credentials that target a given host. + pub fn credentials_for_host(&self, host: &str) -> Vec<&Credential> { + self.credentials + .iter() + .filter(|c| c.target_hosts.iter().any(|h| h == host)) + .collect() + } + + /// API capability registry for a given host. + pub fn api_for_host(&self, host: &str) -> Option<&ApiCapability> { + self.api_registries.values().find(|api| api.host == host) + } +} + +// --------------------------------------------------------------------------- +// Loading +// --------------------------------------------------------------------------- + +/// Load credential descriptors from a YAML file. +pub fn load_credentials(path: &Path) -> Result> { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading credentials file {}", path.display()))?; + let raw: CredentialsFile = serde_yml::from_str(&contents) + .into_diagnostic() + .wrap_err("parsing credentials YAML")?; + + Ok(raw + .credentials + .into_iter() + .map(|c| Credential { + name: c.name, + cred_type: c.cred_type, + scopes: c.scopes, + injected_via: c.injected_via, + target_hosts: c.target_hosts, + }) + .collect()) +} + +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 {source}"))?; + + 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, + }) +} + +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() { + 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 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/finding.rs b/crates/openshell-prover/src/finding.rs new file mode 100644 index 000000000..ab4d4f47f --- /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: u16, + 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: u16, + 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..feff7d1d5 --- /dev/null +++ b/crates/openshell-prover/src/lib.rs @@ -0,0 +1,210 @@ +// 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 model::build_model; +use policy::parse_policy; +use queries::run_all_queries; +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 +/// +/// 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, + registry_dir: Option<&str>, + accepted_risks_path: Option<&str>, + compact: bool, +) -> Result { + let policy = parse_policy(Path::new(policy_path))?; + + 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()?, + ), + }; + + let z3_model = build_model(policy, credential_set, binary_registry); + let mut findings = run_all_queries(&z3_model); + + if let Some(ar_path) = accepted_risks_path { + let accepted = load_accepted_risks(Path::new(ar_path))?; + findings = apply_accepted_risks(findings, &accepted); + } + + 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") + } + + // 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(); + assert!(readable.contains(&"/usr".to_owned())); + assert!(readable.contains(&"/sandbox".to_owned())); + assert!(readable.contains(&"/tmp".to_owned())); + } + + // 3. Workdir NOT included by default (matches runtime behavior). + #[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 (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 pol = policy::parse_policy(&policy_path).expect("parse policy"); + 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); + + 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" + ); + 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 pol = policy::parse_policy(&policy_path).expect("parse policy"); + 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); + + 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..b96e7fef2 --- /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: u16, +} + +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..b116fd5b0 --- /dev/null +++ b/crates/openshell-prover/src/policy.rs @@ -0,0 +1,424 @@ +// 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)] + include_workdir: bool, + #[serde(default)] + read_only: Vec, + #[serde(default)] + read_write: Vec, +} + +#[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: u16, + #[serde(default)] + ports: Vec, + #[serde(default)] + protocol: String, + #[serde(default)] + tls: String, + #[serde(default)] + enforcement: String, + #[serde(default)] + access: String, + #[serde(default)] + rules: Vec, + #[serde(default)] + 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: u16, + 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: false, + read_only: Vec::new(), + read_write: Vec::new(), + } + } +} + +impl FilesystemPolicy { + /// All readable paths (union of `read_only` and `read_write`), with workdir + /// added when `include_workdir` is true and not already present. + pub fn readable_paths(&self) -> Vec { + let mut paths: Vec = self + .read_only + .iter() + .chain(self.read_write.iter()) + .cloned() + .collect(); + if self.include_workdir && !paths.iter().any(|p| p == "/sandbox") { + paths.push("/sandbox".to_owned()); + } + paths + } +} + +/// The top-level policy model used by the prover. +#[derive(Debug, Clone)] +pub struct PolicyModel { + pub version: u32, + pub filesystem_policy: FilesystemPolicy, + pub network_policies: BTreeMap, +} + +impl Default for PolicyModel { + fn default() -> Self { + Self { + version: 1, + filesystem_policy: FilesystemPolicy::default(), + network_policies: BTreeMap::new(), + } + } +} + +impl PolicyModel { + /// All (policy_name, endpoint) pairs. + pub fn all_endpoints(&self) -> Vec<(&str, &Endpoint)> { + let mut result = Vec::new(); + for (name, rule) in &self.network_policies { + for ep in &rule.endpoints { + result.push((name.as_str(), ep)); + } + } + result + } + + /// Deduplicated list of all binary paths across all policies. + pub fn all_binaries(&self) -> Vec<&Binary> { + let mut seen = HashSet::new(); + let mut result = Vec::new(); + for rule in self.network_policies.values() { + for b in &rule.binaries { + if seen.insert(&b.path) { + result.push(b); + } + } + } + result + } + + /// All (binary, policy_name, endpoint) triples. + pub fn binary_endpoint_pairs(&self) -> Vec<(&Binary, &str, &Endpoint)> { + let mut result = Vec::new(); + for (name, rule) in &self.network_policies { + for b in &rule.binaries { + for ep in &rule.endpoints { + result.push((b, name.as_str(), ep)); + } + } + } + result + } +} + +// --------------------------------------------------------------------------- +// Parsing +// --------------------------------------------------------------------------- + +/// Parse an OpenShell policy YAML file into a [`PolicyModel`]. +pub fn parse_policy(path: &Path) -> Result { + let contents = std::fs::read_to_string(path) + .into_diagnostic() + .wrap_err_with(|| format!("reading policy file {}", path.display()))?; + parse_policy_str(&contents) +} + +/// Parse a policy YAML string into a [`PolicyModel`]. +pub fn parse_policy_str(yaml: &str) -> Result { + let raw: PolicyFile = serde_yml::from_str(yaml) + .into_diagnostic() + .wrap_err("parsing policy YAML")?; + + let fs = match raw.filesystem_policy { + Some(fs_def) => FilesystemPolicy { + include_workdir: fs_def.include_workdir, + read_only: fs_def.read_only, + read_write: fs_def.read_write, + }, + None => FilesystemPolicy::default(), + }; + + let mut network_policies = BTreeMap::new(); + if let Some(np) = raw.network_policies { + for (key, rule_raw) in np { + let endpoints = rule_raw + .endpoints + .into_iter() + .map(|ep_raw| { + let rules = ep_raw + .rules + .into_iter() + .map(|r| L7Rule { + method: r.allow.method, + path: r.allow.path, + command: r.allow.command, + }) + .collect(); + Endpoint { + host: ep_raw.host, + port: ep_raw.port, + ports: ep_raw.ports, + protocol: ep_raw.protocol, + tls: ep_raw.tls, + enforcement: ep_raw.enforcement, + access: ep_raw.access, + rules, + allowed_ips: ep_raw.allowed_ips, + } + }) + .collect(); + + let binaries = rule_raw + .binaries + .into_iter() + .map(|b| Binary { path: b.path }) + .collect(); + + let name = rule_raw.name.unwrap_or_else(|| key.clone()); + network_policies.insert( + key, + NetworkPolicyRule { + name, + endpoints, + binaries, + }, + ); + } + } + + Ok(PolicyModel { + version: raw.version.unwrap_or(1), + filesystem_policy: fs, + network_policies, + }) +} diff --git a/crates/openshell-prover/src/queries.rs b/crates/openshell-prover/src/queries.rs new file mode 100644 index 000000000..001255cea --- /dev/null +++ b/crates/openshell-prover/src/queries.rs @@ -0,0 +1,254 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Verification queries: `check_data_exfiltration` and `check_write_bypass`. + +use z3::SatResult; + +use crate::finding::{ExfilPath, Finding, FindingPath, RiskLevel, WriteBypassPath}; +use crate::model::ReachabilityModel; +use crate::policy::PolicyIntent; + +/// Check for data exfiltration paths from readable filesystem to writable +/// egress channels. +pub fn check_data_exfiltration(model: &ReachabilityModel) -> Vec { + if model.policy.filesystem_policy.readable_paths().is_empty() { + return Vec::new(); + } + + let mut exfil_paths: Vec = Vec::new(); + + for bpath in &model.binary_paths { + let cap = model.binary_registry.get_or_unknown(bpath); + if !cap.can_exfiltrate { + continue; + } + + for eid in &model.endpoints { + let expr = model.can_exfil_via_endpoint(bpath, eid); + + if model.check_sat(&expr) == SatResult::Sat { + // Determine L7 status and mechanism + let ep_is_l7 = is_endpoint_l7_enforced(&model.policy, &eid.host, eid.port); + let bypass = cap.bypasses_l7(); + + let (l7_status, mut mechanism) = if bypass { + ( + "l7_bypassed".to_owned(), + format!( + "{} — uses non-HTTP protocol, bypasses L7 inspection", + cap.description + ), + ) + } else if !ep_is_l7 { + ( + "l4_only".to_owned(), + format!( + "L4-only endpoint — no HTTP inspection, {} can send arbitrary data", + bpath + ), + ) + } else { + // L7 is enforced and allows write — policy is + // working as intended. Not a finding. + continue; + }; + + if !cap.exfil_mechanism.is_empty() { + mechanism = format!("{}. Exfil via: {}", mechanism, cap.exfil_mechanism); + } + + exfil_paths.push(ExfilPath { + binary: bpath.clone(), + endpoint_host: eid.host.clone(), + endpoint_port: eid.port, + mechanism, + policy_name: eid.policy_name.clone(), + l7_status, + }); + } + } + } + + if exfil_paths.is_empty() { + return Vec::new(); + } + + let readable = model.policy.filesystem_policy.readable_paths(); + let has_l4_only = exfil_paths.iter().any(|p| p.l7_status == "l4_only"); + let has_bypass = exfil_paths.iter().any(|p| p.l7_status == "l7_bypassed"); + let risk = if has_l4_only || has_bypass { + RiskLevel::Critical + } else { + RiskLevel::High + }; + + let mut remediation = Vec::new(); + if has_l4_only { + remediation.push( + "Add `protocol: rest` with specific L7 rules to L4-only endpoints \ + to enable HTTP inspection and restrict to safe methods/paths." + .to_owned(), + ); + } + if has_bypass { + remediation.push( + "Binaries using non-HTTP protocols (git, ssh, nc) bypass L7 inspection. \ + Remove these binaries from the policy if write access is not intended, \ + or restrict credential scopes to read-only." + .to_owned(), + ); + } + remediation + .push("Restrict filesystem read access to only the paths the agent needs.".to_owned()); + + let paths: Vec = exfil_paths.into_iter().map(FindingPath::Exfil).collect(); + + let n_paths = paths.len(); + vec![Finding { + query: "data_exfiltration".to_owned(), + title: "Data Exfiltration Paths Detected".to_owned(), + description: format!( + "{n_paths} exfiltration path(s) found from {} readable filesystem path(s) to external endpoints.", + readable.len() + ), + risk, + paths, + remediation, + accepted: false, + accepted_reason: String::new(), + }] +} + +/// Check for write capabilities that bypass read-only policy intent. +pub fn check_write_bypass(model: &ReachabilityModel) -> Vec { + let mut bypass_paths: Vec = Vec::new(); + + for (policy_name, rule) in &model.policy.network_policies { + for ep in &rule.endpoints { + // Only check endpoints where the intent is read-only or L4-only + let intent = ep.intent(); + if !matches!(intent, PolicyIntent::ReadOnly) { + continue; + } + + for port in ep.effective_ports() { + for b in &rule.binaries { + let cap = model.binary_registry.get_or_unknown(&b.path); + + // Check: binary bypasses L7 and can write + if cap.bypasses_l7() && cap.can_write() { + let cred_actions = collect_credential_actions(model, &ep.host, &cap); + if !cred_actions.is_empty() + || model.credentials.credentials_for_host(&ep.host).is_empty() + { + bypass_paths.push(WriteBypassPath { + binary: b.path.clone(), + endpoint_host: ep.host.clone(), + endpoint_port: port, + policy_name: policy_name.clone(), + policy_intent: intent.to_string(), + bypass_reason: "l7_bypass_protocol".to_owned(), + credential_actions: cred_actions, + }); + } + } + + // Check: L4-only endpoint + binary can construct HTTP + credential has write + if !ep.is_l7_enforced() && cap.can_construct_http { + let cred_actions = collect_credential_actions(model, &ep.host, &cap); + if !cred_actions.is_empty() { + bypass_paths.push(WriteBypassPath { + binary: b.path.clone(), + endpoint_host: ep.host.clone(), + endpoint_port: port, + policy_name: policy_name.clone(), + policy_intent: intent.to_string(), + bypass_reason: "l4_only".to_owned(), + credential_actions: cred_actions, + }); + } + } + } + } + } + } + + if bypass_paths.is_empty() { + return Vec::new(); + } + + let n = bypass_paths.len(); + let paths: Vec = bypass_paths + .into_iter() + .map(FindingPath::WriteBypass) + .collect(); + + vec![Finding { + query: "write_bypass".to_owned(), + title: "Write Bypass Detected — Read-Only Intent Violated".to_owned(), + description: format!("{n} path(s) allow write operations despite read-only policy intent."), + risk: RiskLevel::High, + paths, + remediation: vec![ + "For L4-only endpoints: add `protocol: rest` with `access: read-only` \ + to enable HTTP method filtering." + .to_owned(), + "For L7-bypassing binaries (git, ssh, nc): remove them from the policy's \ + binary list if write access is not intended." + .to_owned(), + "Restrict credential scopes to read-only where possible.".to_owned(), + ], + accepted: false, + accepted_reason: String::new(), + }] +} + +/// Run both verification queries. +pub fn run_all_queries(model: &ReachabilityModel) -> Vec { + let mut findings = Vec::new(); + findings.extend(check_data_exfiltration(model)); + findings.extend(check_write_bypass(model)); + findings +} + +// --------------------------------------------------------------------------- +// Helpers +// --------------------------------------------------------------------------- + +/// Check whether an endpoint in the policy is L7-enforced. +fn is_endpoint_l7_enforced(policy: &crate::policy::PolicyModel, host: &str, port: u16) -> 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..3acd52f82 --- /dev/null +++ b/crates/openshell-prover/src/registry.rs @@ -0,0 +1,279 @@ +// 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.). +//! +//! 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 include_dir::{Dir, include_dir}; +use miette::{IntoDiagnostic, Result, WrapErr}; +use serde::Deserialize; + +static EMBEDDED_REGISTRY: Dir<'_> = include_dir!("$CARGO_MANIFEST_DIR/registry"); + +// --------------------------------------------------------------------------- +// 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(); + } + for (reg_path, cap) in &self.binaries { + if reg_path.contains('*') { + if let Ok(pattern) = glob::Pattern::new(reg_path) { + if pattern.matches(path) { + return cap.clone(); + } + } + } + } + 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, + } + } +} + +// --------------------------------------------------------------------------- +// Loading +// --------------------------------------------------------------------------- + +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 {source}"))?; + + 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 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() { + 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 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 +} diff --git a/crates/openshell-prover/src/report.rs b/crates/openshell-prover/src/report.rs new file mode 100644 index 000000000..27207a6ae --- /dev/null +++ b/crates/openshell-prover/src/report.rs @@ -0,0 +1,393 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Terminal report rendering (full and compact). + +use std::collections::{HashMap, HashSet}; +use std::path::Path; + +use owo_colors::OwoColorize; + +use crate::finding::{Finding, FindingPath, RiskLevel}; + +// --------------------------------------------------------------------------- +// Compact titles (short labels for each query type) +// --------------------------------------------------------------------------- + +fn compact_title(query: &str) -> &str { + match query { + "data_exfiltration" => "Data exfiltration possible", + "write_bypass" => "Write bypass \u{2014} read-only intent violated", + _ => "Unknown finding", + } +} + +// --------------------------------------------------------------------------- +// Compact detail line +// --------------------------------------------------------------------------- + +fn compact_detail(finding: &Finding) -> String { + match finding.query.as_str() { + "data_exfiltration" => { + let mut by_status: HashMap<&str, HashSet> = HashMap::new(); + for path in &finding.paths { + if let FindingPath::Exfil(p) = path { + by_status + .entry(&p.l7_status) + .or_default() + .insert(format!("{}:{}", p.endpoint_host, p.endpoint_port)); + } + } + let mut parts = Vec::new(); + if let Some(eps) = by_status.get("l4_only") { + let mut sorted: Vec<&String> = eps.iter().collect(); + sorted.sort(); + parts.push(format!( + "L4-only: {}", + sorted + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", ") + )); + } + if let Some(eps) = by_status.get("l7_bypassed") { + let mut sorted: Vec<&String> = eps.iter().collect(); + sorted.sort(); + parts.push(format!( + "wire protocol bypass: {}", + sorted + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", ") + )); + } + if let Some(eps) = by_status.get("l7_allows_write") { + let mut sorted: Vec<&String> = eps.iter().collect(); + sorted.sort(); + parts.push(format!( + "L7 write: {}", + sorted + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", ") + )); + } + parts.join("; ") + } + "write_bypass" => { + let mut reasons = HashSet::new(); + let mut endpoints = HashSet::new(); + for path in &finding.paths { + if let FindingPath::WriteBypass(p) = path { + reasons.insert(p.bypass_reason.as_str()); + endpoints.insert(format!("{}:{}", p.endpoint_host, p.endpoint_port)); + } + } + let mut sorted_eps: Vec<&String> = endpoints.iter().collect(); + sorted_eps.sort(); + let ep_list = sorted_eps + .iter() + .map(|s| s.as_str()) + .collect::>() + .join(", "); + if reasons.contains("l4_only") && reasons.contains("l7_bypass_protocol") { + format!("L4-only + wire protocol: {ep_list}") + } else if reasons.contains("l4_only") { + format!("L4-only (no inspection): {ep_list}") + } else if reasons.contains("l7_bypass_protocol") { + format!("wire protocol bypasses L7: {ep_list}") + } else { + String::new() + } + } + _ => String::new(), + } +} + +// --------------------------------------------------------------------------- +// Risk formatting +// --------------------------------------------------------------------------- + +fn risk_label(risk: RiskLevel) -> String { + match risk { + RiskLevel::Critical => "CRITICAL".to_owned(), + RiskLevel::High => "HIGH".to_owned(), + } +} + +fn print_risk_label(risk: RiskLevel) { + match risk { + RiskLevel::Critical => print!("{}", "CRITICAL".bold().red()), + RiskLevel::High => print!("{}", " HIGH".red()), + } +} + +// --------------------------------------------------------------------------- +// Compact output +// --------------------------------------------------------------------------- + +/// Render compact output (one-line-per-finding for demos and CI). +/// Returns exit code: 0 = pass, 1 = critical/high found. +pub fn render_compact(findings: &[Finding], _policy_path: &str, _credentials_path: &str) -> i32 { + let active: Vec<&Finding> = findings.iter().filter(|f| !f.accepted).collect(); + let accepted: Vec<&Finding> = findings.iter().filter(|f| f.accepted).collect(); + + for finding in &active { + print!(" "); + print_risk_label(finding.risk); + println!(" {}", compact_title(&finding.query)); + let detail = compact_detail(finding); + if !detail.is_empty() { + println!(" {detail}"); + } + println!(); + } + + for finding in &accepted { + println!( + " {} {}", + "ACCEPTED".dimmed(), + compact_title(&finding.query).dimmed() + ); + } + if !accepted.is_empty() { + println!(); + } + + // Verdict + let mut counts: HashMap = HashMap::new(); + for f in &active { + *counts.entry(f.risk).or_default() += 1; + } + let has_critical = counts.contains_key(&RiskLevel::Critical); + let has_high = counts.contains_key(&RiskLevel::High); + let accepted_note = if accepted.is_empty() { + String::new() + } else { + format!(", {} accepted", accepted.len()) + }; + + if has_critical || has_high { + let n = counts.get(&RiskLevel::Critical).unwrap_or(&0) + + counts.get(&RiskLevel::High).unwrap_or(&0); + println!( + " {} {n} critical/high gaps{accepted_note}", + " FAIL ".white().bold().on_red() + ); + 1 + } else if !active.is_empty() { + println!( + " {} advisories only{accepted_note}", + " PASS ".black().bold().on_yellow() + ); + 0 + } else { + println!( + " {} all findings accepted{accepted_note}", + " PASS ".white().bold().on_green() + ); + 0 + } +} + +// --------------------------------------------------------------------------- +// Full terminal report +// --------------------------------------------------------------------------- + +/// Render a full terminal report with finding panels. +/// Returns exit code: 0 = pass, 1 = critical/high found. +pub fn render_report(findings: &[Finding], policy_path: &str, credentials_path: &str) -> i32 { + let policy_name = Path::new(policy_path) + .file_name() + .map_or("policy.yaml", |n| n.to_str().unwrap_or("policy.yaml")); + let creds_name = Path::new(credentials_path) + .file_name() + .map_or("credentials.yaml", |n| { + n.to_str().unwrap_or("credentials.yaml") + }); + + println!(); + println!( + "{}", + "\u{250c}\u{2500}\u{2500} OpenShell Policy Prover \u{2500}\u{2500}\u{2510}".blue() + ); + println!(" Policy: {policy_name}"); + println!(" Credentials: {creds_name}"); + println!(); + + let active: Vec<&Finding> = findings.iter().filter(|f| !f.accepted).collect(); + let accepted: Vec<&Finding> = findings.iter().filter(|f| f.accepted).collect(); + + // Summary + let mut counts: HashMap = HashMap::new(); + for f in &active { + *counts.entry(f.risk).or_default() += 1; + } + + println!("{}", "Finding Summary".bold().underline()); + for level in [RiskLevel::Critical, RiskLevel::High] { + if let Some(&count) = counts.get(&level) { + match level { + RiskLevel::Critical => { + println!(" {:>10} {count}", "CRITICAL".bold().red()); + } + RiskLevel::High => println!(" {:>10} {count}", "HIGH".red()), + } + } + } + if !accepted.is_empty() { + println!(" {:>10} {}", "ACCEPTED".dimmed(), accepted.len()); + } + println!(); + + if active.is_empty() && accepted.is_empty() { + println!("{}", "No findings. Policy posture is clean.".green().bold()); + return 0; + } + + // Per-finding details + for (i, finding) in active.iter().enumerate() { + let label = risk_label(finding.risk); + let border = match finding.risk { + RiskLevel::Critical => format!("{}", format!("[{label}]").bold().red()), + RiskLevel::High => format!("{}", format!("[{label}]").red()), + }; + + println!("--- Finding #{} {border} ---", i + 1); + println!(" {}", finding.title.bold()); + println!(" {}", finding.description); + println!(); + + // Render paths + render_paths(&finding.paths); + + // Remediation + if !finding.remediation.is_empty() { + println!(" {}", "Remediation:".bold()); + for r in &finding.remediation { + println!(" - {r}"); + } + println!(); + } + } + + // Accepted findings + if !accepted.is_empty() { + println!("{}", "--- Accepted Risks ---".dimmed()); + for finding in &accepted { + println!( + " {} {}", + risk_label(finding.risk).dimmed(), + finding.title.dimmed() + ); + println!( + " {}", + format!("Reason: {}", finding.accepted_reason).dimmed() + ); + println!(); + } + } + + // Verdict + let has_critical = counts.contains_key(&RiskLevel::Critical); + let has_high = counts.contains_key(&RiskLevel::High); + let accepted_note = if accepted.is_empty() { + String::new() + } else { + format!(" ({} accepted)", accepted.len()) + }; + + if has_critical { + println!( + "{}{accepted_note}", + "FAIL \u{2014} Critical gaps found.".bold().red() + ); + 1 + } else if has_high { + println!( + "{}{accepted_note}", + "FAIL \u{2014} High-risk gaps found.".bold().red() + ); + 1 + } else if !active.is_empty() { + println!( + "{}{accepted_note}", + "PASS \u{2014} Advisories only.".bold().yellow() + ); + 0 + } else { + println!( + "{}{accepted_note}", + "PASS \u{2014} All findings accepted.".bold().green() + ); + 0 + } +} + +fn render_paths(paths: &[FindingPath]) { + if paths.is_empty() { + return; + } + + match &paths[0] { + FindingPath::Exfil(_) => render_exfil_paths(paths), + FindingPath::WriteBypass(_) => render_write_bypass_paths(paths), + } +} + +fn render_exfil_paths(paths: &[FindingPath]) { + println!( + " {:<30} {:<25} {:<15} {}", + "Binary".bold(), + "Endpoint".bold(), + "L7 Status".bold(), + "Mechanism".bold(), + ); + for path in paths { + if let FindingPath::Exfil(p) = path { + let l7_display = match p.l7_status.as_str() { + "l4_only" => format!("{}", "L4-only".red()), + "l7_bypassed" => format!("{}", "bypassed".red()), + "l7_allows_write" => format!("{}", "L7 write".yellow()), + _ => p.l7_status.clone(), + }; + let ep = format!("{}:{}", p.endpoint_host, p.endpoint_port); + // Truncate mechanism for display + let mech = if p.mechanism.len() > 50 { + format!("{}...", &p.mechanism[..47]) + } else { + p.mechanism.clone() + }; + println!(" {:<30} {:<25} {:<15} {}", p.binary, ep, l7_display, mech); + } + } + println!(); +} + +fn render_write_bypass_paths(paths: &[FindingPath]) { + println!( + " {:<30} {:<25} {:<15} {}", + "Binary".bold(), + "Endpoint".bold(), + "Bypass".bold(), + "Intent".bold(), + ); + for path in paths { + if let FindingPath::WriteBypass(p) = path { + let ep = format!("{}:{}", p.endpoint_host, p.endpoint_port); + let bypass_display = match p.bypass_reason.as_str() { + "l4_only" => format!("{}", "L4-only".red()), + "l7_bypass_protocol" => format!("{}", "wire proto".red()), + _ => p.bypass_reason.clone(), + }; + println!( + " {:<30} {:<25} {:<15} {}", + p.binary, ep, bypass_display, p.policy_intent + ); + } + } + println!(); +} diff --git a/crates/openshell-prover/testdata/accepted-risks.yaml b/crates/openshell-prover/testdata/accepted-risks.yaml new file mode 100644 index 000000000..6af5c7146 --- /dev/null +++ b/crates/openshell-prover/testdata/accepted-risks.yaml @@ -0,0 +1,7 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +accepted_risks: + - query: inference_relay + reason: "Demo environment — inference.local not configured." + accepted_by: demo diff --git a/crates/openshell-prover/testdata/credentials.yaml b/crates/openshell-prover/testdata/credentials.yaml new file mode 100644 index 000000000..b186ccf9a --- /dev/null +++ b/crates/openshell-prover/testdata/credentials.yaml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +credentials: + - name: github-pat + type: github-pat + scopes: + - repo + injected_via: GITHUB_TOKEN + target_hosts: + - api.github.com + - github.com diff --git a/crates/openshell-prover/testdata/empty-policy.yaml b/crates/openshell-prover/testdata/empty-policy.yaml new file mode 100644 index 000000000..458bab0e4 --- /dev/null +++ b/crates/openshell-prover/testdata/empty-policy.yaml @@ -0,0 +1,4 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 diff --git a/crates/openshell-prover/testdata/policy.yaml b/crates/openshell-prover/testdata/policy.yaml new file mode 100644 index 000000000..e98d95319 --- /dev/null +++ b/crates/openshell-prover/testdata/policy.yaml @@ -0,0 +1,50 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 + +filesystem_policy: + include_workdir: true + read_only: + - /usr + - /lib + - /proc + - /dev/urandom + - /app + - /etc + - /var/log + read_write: + - /sandbox + - /tmp + - /dev/null + +landlock: + compatibility: best_effort + +process: + run_as_user: sandbox + run_as_group: sandbox + +# Intent: read-only GitHub access for the agent. +# The REST API has L7 enforcement — only GET allowed. +# github.com is included for git clone — "it just needs connectivity." +network_policies: + github_api: + name: github-api + endpoints: + # REST API — L7 enforced, read-only + - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: read-only + # github.com — for git clone. + # No protocol field — L4 only. + - host: github.com + port: 443 + binaries: + - { path: /usr/local/bin/claude } + - { path: /usr/bin/git } + - { path: /usr/bin/curl } + - { path: /usr/bin/gh } + - { path: /sandbox/.uv/python/**/python3* } diff --git a/deploy/docker/Dockerfile.ci b/deploy/docker/Dockerfile.ci index fe3241cb3..b09c93e11 100644 --- a/deploy/docker/Dockerfile.ci +++ b/deploy/docker/Dockerfile.ci @@ -23,6 +23,9 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ curl \ git \ build-essential \ + clang \ + libclang-dev \ + libz3-dev \ pkg-config \ libssl-dev \ openssh-client \