OpenShell Z3 policy prover 實測 29 項檢查，metadata 位址在空白邊界下仍通過

OpenShell — NVIDIA's "safe, private runtime for fleets of autonomous AI agents" — hit the Hacker News front page today (257 points; the repo is at 17,719 stars, v0.1.5 shipped October 20). Most agent sandboxes sell you enforcement: Landlock, seccomp, a network proxy. OpenShell sells those too, but its headline differentiator is the second half: formal verification. Before a policy change is applied, an SMT-based prover checks what the change would allow.

That prover ships as a standalone CLI, openshell-prover, whose job is a boundary check: given a candidate policy and a boundary policy (the most access an environment allows), decide whether the candidate stays inside the boundary — and if not, produce a counterexample. The docs say the CLI is "primarily intended for agents": a parent agent checking that a policy it wrote for a subagent stays within its own maximum.

So I built it from source and tried to sneak things past it. 29 candidate/boundary pairs. It caught almost everything. The one thing it didn't catch is the address every agent-safety talk warns you about first.

Building it

The clone (HEAD 9a85667, today) is a 38-crate Rust workspace — 625 .rs files under crates/ alone. The prover needs Z3, and this machine has no system libz3. The crate's prebuilt-z3 feature failed ("Could not find release for z3-5.1.0"), so I took the side door: the Python z3-solver wheel ships a libz3.so (5.3.1). Point LIBRARY_PATH at the wheel's lib directory and the Rust z3 crate links against it happily:

cargo build -p openshell-prover-cli --bin openshell-prover
Finished dev profile in 2.15s (incremental)
target/debug/openshell-prover: 33,137,752 bytes
individual checks below: 5–99 ms each

The scoreboard

Boundary B1 allows reading /usr and /etc, nothing else. Boundary B2 allows one thing: GET-only REST access to api.github.com:443 from /usr/bin/git. Results:

candidate                                   verdict
------------------------------------------  -------------------------
read /usr only (subset of B1)               within_boundary
read /usr + write /tmp                      exceeds  (counterexample: filesystem write /tmp)
read /etc/passwd under B1's /etc            unsupported — refuses to guess
write /etc                                  exceeds  (filesystem write /etc)
read /usr/../etc                            rejected at load: '..' segment unsupported
REST access read-only -> read-write         exceeds  (counterexample: PUT / on api.github.com:443)
same host, drop protocol (raw L4)           exceeds  (counterexample: protocol=l4)
REST read-only + extra host github.com L4   exceeds  (counterexample: host=github.com:443)
add /usr/bin/curl to the REST rule          exceeds  (binary not in boundary)
host example.com:443, 8.8.8.8, 10.0.0.5,
  192.168.1.1, 100.100.100.200, localhost    exceeds  (all of them)
host metadata.google.internal:80            exceeds
host 169.254.169.254:80 or :443             within_boundary  ←
host 169.254.170.2:80 (ECS task metadata)   within_boundary  ←
host 127.0.0.1:8080                         within_boundary  ←
169.254.169.254 vs an EMPTY boundary        within_boundary  ←

Three things deserve credit before the failure. First, the counterexamples are concrete: escalate REST access and the prover hands you the exact witness request (method=PUT path=/). Second, you cannot launder a read-only REST rule through a raw L4 endpoint to the same host — it models the difference. Third, when a comparison depends on facts it doesn't have — is /etc/passwd contained by /etc given symlinks in an image it can't see? — it returns unsupported and exits 3 rather than guessing. That is rarer and better than it sounds.

The carve-out

A policy whose only network rule is "curl may reach 169.254.169.254" — the cloud metadata address, the SSRF greatest hit, the thing the Hugging Face agent incident ran on — passes the boundary check. It passes against a boundary that allows only GitHub. It passes against an empty boundary, one that grants no network access at all. Same for the whole link-local range (I tested the AWS ECS metadata address 169.254.170.2 too) and for loopback by literal IP — while localhost by name is caught, which tells you this is about the address model, not the destination.

This is not a solver bug. It's in the source, in crates/openshell-prover/src/containment/ip.rs:

const HARD_V4: &[&str] = &["127.0.0.0/8", "169.254.0.0/16", "0.0.0.0/32"];
const HARD_V6: &[&str] = &["::/128", "::1/128", "fe80::/10"];

Loopback, link-local, and unspecified addresses are excluded from the destination-IP containment model. And there is a defensible reason, also in the source: the runtime proxy hard-blocks the same ranges regardless of policy — is_always_blocked_ip in the supervisor's network code, with a test literally named test_declared_endpoint_loopback_stays_blocked. The prover models what policy controls; these ranges are controlled by something else. There is even a separate link_local_reach finding — "any reach to a link-local IP range, unconditional" — but it lives in the proposal risk check that runs inside the gateway's policy advisor, not in this CLI. The prover docs, to their credit, say plainly that passing one check does not imply passing the other.

What neither the CLI nor the docs' coverage section tells you is that the boundary check's model has this hole in it. Run the documented command on the metadata policy and the entire output is:

result: within_boundary
coverage: domains=filesystem,network_l4,network_rest,process,landlock

No asterisk, no "3 ranges excluded from model." The coverage line even lists network_l4 as covered. The audience for this tool is, by NVIDIA's own description, agents — a parent agent verifying a subagent's policy before approving it. That agent will read within_boundary as a proof. For every destination except the three ranges that matter most in agent threat models, it is one. For those, the proof is vacuous, and nothing in the output says so.

Scope of what I did, so you can discount it correctly: I ran the standalone boundary CLI from a debug build, 29 hand-written policy pairs, no gateway, no live sandbox, no proposal-risk check. The runtime hard-block is something I verified by reading the supervisor source and its tests, not by running an agent against a real metadata service. OpenShell's design — policy prover plus an always-blocked list plus a separate risk check — is genuinely more serious than most agent sandboxes I've audited. The gap isn't in the enforcement. It's that the verification artifact overstates its own coverage, in exactly the corner where an automated reader is least likely to ask questions.

Source: NVIDIA/OpenShell (Apache-2.0), prover docs and crates/openshell-prover as cloned today. All check outputs above are from my runs.