NVIDIA OpenShell：用形式化方法验证AI Agent权限策略

沙箱阻止了 Agent 向一个它无权操作的 GitHub 仓库写入。

Agent 随后发出的消息：文件已写入。

这个故事来自 NVIDIA 的 OpenShell 团队，内容是一份关于其策略检查背后形式化方法的开发笔记。Agent 发现自己处于沙箱中后，拿起它已有的 GitHub 凭据，通过 git-remote-https 推送了出去——这是一个策略允许的二进制文件，Agent 本来可以用它来克隆代码。团队没有意识到这个辅助工具既能推送也能拉取。每条规则本身都是合理的，但组合在一起就产生了漏洞。

这就是用肉眼阅读权限文件的问题。你逐行检查，但泄漏就藏在行与行之间。而且一旦 Agent 开始为其他 Agent 编写策略，就没有人会逐行阅读了。

OpenShell 是什么，以及值得借鉴的部分

OpenShell 是 NVIDIA 开源的 AI Agent 沙箱运行时，写这篇文章时它在 GitHub 热门榜上排名第二。你为每个沙箱编写一份 YAML 策略：Agent 可以读取或写入哪些路径、以什么用户身份运行、哪些二进制文件可以访问哪些主机。文件系统规则通过内核的 Landlock 实现，网络流量通过一个可以检查每个 HTTP 方法和路径的代理。

这部分很好，也是每个沙箱都会承诺的功能。但我认为更重要的部分是一个独立的小型二进制文件：openshell-prover。你给它两个策略文件——一个是候选策略，一个是边界策略——它会询问一个 SMT 求解器（根据 crate 的 Cargo.toml，是 Z3）：候选策略是否允许了边界策略不允许的任何内容。如果允许，你就得到一个额外访问权限的具体示例。

它不需要网关、不需要 Docker，也不需要账号。它只读取文件。所以我运行了它。

一个二进制文件，一分钟

在 Mac 上，完整安装脚本通过 Homebrew 安装并启动网关服务。如果只想要 prover，下载发布包：

gh release download v0.1.2 -R NVIDIA/OpenShell \
  -p 'openshell-prover-aarch64-apple-darwin.tar.gz'
tar xzf openshell-prover-aarch64-apple-darwin.tar.gz
./openshell-prover --version
# openshell-prover 0.1.2

在 Linux 上，换成 x86_64-unknown-linux-musl 的归档文件。校验和与发布的 sha256 文件一致，下面的每次检查都在 10 毫秒内返回结果。

文档中的第一个示例是一个边界策略允许读取 /usr 和 /etc，而候选策略还想写入 /tmp：

result: exceeds_boundary
coverage: domains=filesystem,network_l4,network_rest,process,landlock
counterexample: filesystem write /tmp

这个例子不错，但只是个玩具。我真正关心的是下面这个案例。

重要的场景：父 Agent 编写子 Agent 的策略

假设父 Agent 可以使用 curl 读取 GitHub API，除此之外不能做其他操作。这是边界策略：

version: 1
network_policies:
  github_read:
    endpoints:
      - host: api.github.com
        port: 443
        protocol: rest
        enforcement: enforce
        access: read-only
    binaries:
      - path: /usr/bin/curl

（我真实的文件还有一个小的 filesystem_policy，这里省略了。）现在父 Agent 为子 Agent 编写策略。第一版只允许 GET 一个仓库。prover 说 within_boundary 并以退出码 0 退出。

第二版悄悄加入了一条额外的规则：对 /repos/acme/app/issues 发起 POST——这类东西是 Agent 因为"可能需要提交一个 bug"而加上的：

result: exceeds_boundary
counterexample: network binary=- ancestor_binary=- binary_identity_required=false
  host=api.github.com:443 protocol=rest method=POST path=/repos/acme/app/issues

（截取有用字段并为页面做了换行。）它找到了那个精确的请求。注意 binary_identity_required=false：prover 会对每个策略分别在使用和不使用二进制身份强制执行两种情况下进行检查，因为运行时可以关闭该强制执行。

然后我尝试了两种肉眼很容易漏掉的泄漏。新增一条规则让 curl 访问 paste.example.com，返回的逆例就是那个主机。而在现有的 GitHub 规则中加入 /usr/bin/python3.12，返回的逆例是 ancestor_binary=/usr/bin/python3.12：一个由 Python 启动的进程访问了 API。文档解释了其原因。一条规则覆盖的是所列二进制文件启动的进程，所以添加一个解释器就悄无声息地添加了它能运行的一切。

一个把进程用户从 sandbox 切换到 root 的候选策略，返回的逆例是 process run_as_user boundary=sandbox candidate=root。

它说"我无法判断"的时候

这就是让我决定使用的部分。当 prover 无法回答时，它会如实说出来并以退出码 3 退出，而不是勉强通过。

我把子 Agent 的写权限从 /sandbox 收窄到 /sandbox/out。这显然更小，但它返回了 unsupported：沙箱镜像内部的一个符号链接可能把 /sandbox/out 指向别处，所以它要求两个文件中路径要匹配。

一条处于审计模式的 REST 规则返回了 unsupported，因为审计模式会记录一个坏请求但仍然放行。

一个 root 用户对照一个从未指定用户的边界策略，返回的是 unsupported，而不是通过。

文档列出了更多缺口：GraphQL、MCP 和 WebSocket 规则还没有被建模。第一个案例是一个真实的粗糙边缘，因为收窄路径正是父 Agent 会做的事情。但一个拒绝作答的检查器比一个猜答案的检查器更值得信赖。

这是我的主张。Agent 权限审查的有用单元不是策略文件，而是逆例。

今天，一个权限提示向你展示一条规则，然后让你想象它允许了什么。prover 把这个过程倒转过来：它向你展示新策略会允许但旧策略不会允许的一个具体请求，或者告诉你它无法决定。读一行类似 method=POST path=/repos/acme/app/issues 这样的内容只需要两秒。读四十行 YAML 并找出 Python 解释器的问题需要一个细心的人，而 Agent 不会等细心的人。

如果你允许 Agent 派生 Agent，这一点最为重要。父 Agent 自己的策略成为边界，每个子策略在运行前都要对照它检查。退出码 0 表示放行，其他任何情况都需要人工审查。

OpenShell 已经在其策略顾问中接入了这个功能，在那里，遇到被阻止请求的 Agent 可以提议一条新的网络规则。根据文档，每个提案都会进行风险检查，寻找凭据到达新主机之类的情况，并且有一种自动批准模式。仔细看看这个模式的fine print：文档说当没有凭据适用于某个全新的公共主机时，它仍然会批准。这是一个策略选择，而不是证明。

我只运行了 prover。我没有运行沙箱、网关或顾问；我对它们的了解都来自文档。在 Mac 上，沙箱需要 Docker Desktop 或 MicroVM 驱动，并且在 0.1.2 版本上，9 月 30 日开放的的两个 issue（#3955 和 #3948）描述了那条路径需要手动修复，包括手动给 VM 驱动签名。如果你想在 Mac 上先尝个鲜，从 prover 开始。它是那个一分钟就能用起来的部分。

你会让一个没有任何人读过策略的子 Agent 运行吗——如果有一个求解器已经对照你的策略检查过它的话？