NVIDIA 把「Agent 安全运行时」做成了官方基础设施：OpenShell 内核级拦截 + 策略形式化验证，17.8k star 背后是对隔离层的收编

九月那篇《NVIDIA 出手了！Open Agent Safety Platform 发布》，讲的是这次发布想对外讲的故事：OpenShell 划边界，Sentry 在 BlueField-4 上做毫秒隔离，联合 100 多家组织。那篇是新闻，是平台层面的叙事。

这篇拆它内部。我把 OpenShell 的架构文档、安全配置指南、策略验证引擎那几页，加上仓库的目录结构读了一遍。读完之后我觉得最值得写的是三件事：四层执法点怎么分工、为什么一个 Agent 运行时里会塞进一个 SMT 求解器、以及那个只有七个方法的 Rust 接口。至于「它也能做沙箱」，反倒是最不值得说的一点。

第三件事是题眼。17.8k star 这个数字本身没什么，但它背后那个接口的设计，意味着隔离层正在被收编成一个标准。

先把零件摆清楚

OpenShell 的架构里有两个词反复出现，先分清它们：可信侧和沙箱侧。

一次沙箱创建的过程是这样的。你调 gateway（控制面，管沙箱生命周期和对外连接），它让 compute driver 去铺资源：driver 创建 workload、装好外网围栏、给出一份经过验证的描述符。同时它起一个独立的 supervisor，跟 workload 建一条受保护的通道，把隔离边界搭起来。supervisor 确认边界成立之后，才让 agent 起来，然后回头连 gateway 拿策略、凭据、日志和交互会话。

这里有一条我觉得设计得很干净的分工：

组件	它拥有什么
Supervisor	策略决策。策略、凭据、DNS 解析、已批准的外部连接，全部留在 agent 的 workload 之外
Compute driver	放置与围栏。创建运行时资源、装外网围栏、提供经过验证的描述符
Isolation backend	共同行为。把共享的调用翻译成跟沙箱运行时之间的一条受保护会话

而 sandbox 自己呢？它跟 agent 住在边界里面，管 agent 的进程，知道每个请求是哪个程序发出来的，施加进程控制，然后把 TCP 和 DNS 流量转给 supervisor。

注意最后那句「知道每个请求是哪个程序发出来的」。这一句是后面策略粒度的基础：它的网络策略按二进制授权，粒度细到容器里的具体程序。

内核级拦截：四层执法点，和一条分界线

官方把沙箱安全拆成四层，每一层都写明了执法点，以及能不能在运行时改：

层	保护什么	执法点	运行时能改吗
网络	未授权出网与数据外泄	CONNECT 代理 + OPA 策略引擎	能，`openshell policy update` 或 `set`
文件系统	系统二进制被篡改、凭据被偷、配置被改	Landlock LSM（内核级）	不能，必须重建沙箱
进程	提权、fork 炸弹、危险系统调用	Seccomp BPF + 权限降级（setuid / setgid）	不能，必须重建沙箱
提供方凭据	凭据暴露与未授权的服务访问	网络策略 + profile 端点绑定 + 代理替换	能，挂载或卸载提供方

这张表我盯了很久。它有意思的地方在那条竖着切下来的线：文件系统和进程锁死在沙箱创建时，网络和凭据可以在运行时改。

为什么这么切？我猜是因为可逆性。文件系统可见性和进程权限一旦放开，你在同一个沙箱里没法收回来，所以只能在创建那一刻定死，要改就重建。而网络目的地和凭据注入是可逆的，随时收紧都来得及，所以放开给运行时。

这条线把「最小权限」从一个口号变成了一个有时间语义的机制。多数沙箱产品只回答「允许什么」，它多回答了一个「什么时候可以改」。

还有两个细节值得单独拎出来。

一个是 landlock 这个配置段。文档里的描述是：如果 OpenShell 应用不了你的文件系统规则，沙箱还起不起得来。这是个 fail-closed 还是 fail-open 的开关。它没有被藏起来，而是作为策略里的一个独立段让你显式选。内核级强制最怕的就是「规则没生效但没人知道」，把这个选择摆到台面上，说明作者想过这个问题。

另一个是凭据。文档的说法是：agent 从来见不到真凭据，OpenShell 只在发往已批准端点的请求上把凭据加上去。 换句话说，凭据不在沙箱里，是在 supervisor 那一侧做替换注入的。这一条的价值在于它同时解决了两个问题：agent 偷不到，被 prompt injection 操纵的 agent 也偷不到，因为它手里压根没有。

至于最外圈那层围栏，叫外网围栏，规则很粗暴：除了到 supervisor 的那条受保护通道，workload 的一切出网全部拒绝。文档里有一句我挺喜欢的话：每个运行时用它自己的原生工具来搭这层围栏。这句话不优雅，但很诚实，也预告了后面那个接口的存在。

形式化验证：为什么一个 Agent 运行时里会有 SMT 求解器

这是整篇里我最没想到的部分。

OpenShell 有一个叫 policy prover 的组件，官方定义是「策略验证引擎，用一个 SMT 求解器检查策略是否满足特定性质，比如不越出允许的访问边界」。它做两种检查。

边界检查。你写一份 boundary policy，定义这个环境允许的最大访问范围；再拿一份 candidate policy 去比。如果 candidate 允许了 boundary 不允许的东西，检查失败，并且给你一个反例。命令长这样：

openshell-prover check candidate.yaml --boundary boundary.yaml

通过的时候输出 result: within_boundary，还有一行 coverage 告诉你这次检查覆盖了哪些域：domains=filesystem,network_l4,network_rest,process,landlock。失败的时候会多一行 counterexample，把「candidate 允许但 boundary 不允许」的具体访问指出来。

提案风险检查。这个更有意思：每次 agent 通过 policy advisor 提出一条新的网络规则时，这个检查自动跑，看这条新规则相比沙箱当前策略有没有引入风险访问，比如访问云元数据地址，或者给提供方凭据开了一个新目的地。

两种检查回答的是不同问题，文档特意说了一句：通过其中一个不代表通过另一个。

那为什么一个跑 agent 的东西里会有求解器？答案藏在文档的一句话里：openshell-prover 这个 CLI「主要是给 agent 用的」。举的例子是，一个父 agent 可以用它来检查自己给子 agent 写的策略是否还在自己的最大允许范围内。

这就说得通了。如果策略是 agent 自己写的，那策略本身就必须被验证。 形式化方法进这个产品，跟学术界喜欢它没什么关系，是因为 agent 会自己生成策略，而生成的策略需要一个可判定的检查器来兜底。

更值得记的是它承认边界的方式。文档写得很直白：这些保证只覆盖它模型所表达的策略特性和行为，OpenShell 正在持续扩展这个模型。而且如果一份策略用了模型覆盖不到的东西，比如 GraphQL 或者 MCP 规则，prover 会报告它无法检查这份策略，而不是忽略那几条规则。

宁可不检查，也不假装检查过。这个取舍比覆盖率值钱得多。做形式化验证最容易翻车的方式，就是在模型覆盖不到的地方默默放行，然后在文档里写一句「已验证」。

收编：一个 Rust 接口，七个方法

现在说到题眼。

OpenShell 的 supervisor 要用一个 Rust 接口 IsolationBackend 来启动和控制 agent 的 workload。接口定义在 openshell-isolation-interface 这个 crate 的 contract.rs 里，默认实现在 openshell-sandbox-backend。仓库里还有一份 RFC 0012，专门讨论这个设计。

它的七个方法我列在下面，重点看每个方法返回什么类型：

调用	做什么	返回
`IsolationBackend::attach()`	把一个已验证的运行时描述符绑到一个已接纳的沙箱上	`BoundBoundary`
`BoundBoundary::confirm()`	在 agent 代码跑起来之前，检查 workload 的控制项	`ConfirmedBoundary`
`ReadyBoundary::start_agent()`	再检查一遍启动控制项，然后启动 agent	`RunningBoundary`
`RunningBoundary::agent()`	等待、发信号、附着或停止 agent 进程	`BoundaryProcess`
`RunningBoundary::exec()`	在同一个边界里开 exec 和终端会话	`BoundaryExec`
`RunningBoundary::loopback_connector()`	够到 workload 里的 loopback 服务，用于转发	`BoundaryLoopbackConnector`
`BoundBoundary::network_mediation_source()`	接收带调用程序标记的 TCP 打开和 DNS 查询	`NetworkMediationSource`

每一步都返回一个新类型，官方对这件事的说明只有一句，但很关键：这样 supervisor 就没法在一个还没被确认的边界上启动 agent。

这是 Rust 里常说的类型状态模式：把流程约束编进类型里，让非法顺序在编译期就不成立，而不是靠运行时检查加一句「请先调用 confirm」。在一个安全运行时的核心接口上用这个模式，意图很明确：把启动顺序变成编译器的规则，而不是文档里的建议。

然后是它为什么叫「收编」。文档里接着写了这么一句：因为 supervisor 只依赖这个接口，所以另一个 backend 可以用不同的隔离机制提供同样的操作，而不需要改动 gateway 的 API 或者策略模型。

换个说法：隔离怎么做，是可以换的；接口长什么样，是 NVIDIA 定的。

这就是 17.8k star 背后真正在发生的事。OpenShell 没有去发明一种新的隔离技术，它把已有的隔离技术（容器、Podman、Kubernetes、虚拟机、Windows 的 MXC）收进一个统一的接口，然后把这个接口和策略模型一起开源。策略模型是它定义的，隔离实现是可插拔的。做隔离层的那批公司，往后要面对的问题不再是「我的隔离比你的强」，而是「我的实现符不符合这个接口」。

仓库里还有什么值得看

我顺手翻了目录结构，有几个地方能看出这东西的形态。

crates/ 下面，除了前面提到的接口和 backend，还有一串 driver：docker、podman、kubernetes、vm、mxc（Windows 原生，里面有 etw_consumer.rs，走 ETW 消费事件）、vault、db-credstore、kubernetes-secrets。凭据相关的 driver 单独成 crate，说明「凭据不进沙箱」在实现上是一件要专门做事的工作，不是一个开关。

openshell-crypto 是独立的一个 crate，里面有 aws_lc.rs、pki/、aead.rs、jwt.rs、tls.rs。密码学实现单独抽出来，而且绑的是 AWS-LC，这个选择在安全圈是有讲究的。

openshell-core 里我注意到几个文件名：spiffe.rs、isolation_registration.rs、provider_credentials.rs、resource_admission.rs、proposals.rs、binary_identity（这个是独立 crate）。spiffe.rs 这个存在本身就说明，Agent 的身份体系正在和运行时安全层合流，我前几天写身份联邦那篇的时候还没料到会在这里再撞上它。

还有 openshell-conformance，里面有 scenarios/policy_behavior.rs、sandbox_lifecycle.rs、file_transfer.rs、smoke.rs。有 conformance 套件意味着这套东西是打算被别人实现的，进一步印证了接口化那条路。

最后一个小细节，我觉得挺有意思：这个仓库自己就在用 agent 干活。.agents/skills/ 下面挂着一批 SKILL.md，管 triage、review、release、sbom；scripts/agents/gator/ 里是他们的一个评审 agent，而且带着自己的 policy.yaml。写 Agent 安全运行时的团队，用 Agent 来维护这个仓库，并且给这个 Agent 也配了策略文件。

硬件那一半，简单带过

9 月那篇已经讲过 Sentry 和 BlueField-4 了，这里只补一点新数字，因为它们是十月二十一号那篇参考架构文章里的。

NVIDIA 说 Vera CPU 有 88 个 Olympus 核、第二代可扩展一致性结构、LPDDR5X 内存，在关键 agent 任务上比 x86 快最多 2 倍。CoreWeave 测出来的数字是：沙箱启动快 3 倍以上，agent 循环完成快 1.8 倍，单个机架支撑超过 11,000 个并发 agent 环境。加上 BlueField-4 和 Sentry 的硬件级监控，检测到策略违规可以在毫秒级隔离。

这些数字来自厂商和它的合作方，按惯例要打折看：方向可信，绝对值存疑。

我的三个判断

第一，隔离层正在从产品差异变成接口标准。这对做隔离技术的公司是个坏消息。OpenShell 把「怎么隔离」抽象成七个方法，把「允许什么」抽象成一份 YAML，然后两个都用 Apache-2.0 放出来。往后隔离实现的竞争会往两个方向挤：要么比这个接口更好用，要么比它更快更省。中间那层「我也能沙箱」的空间，正在被这个接口吃掉。

第二，形式化验证进产品流程的触发条件，是 agent 开始自己写策略。这个因果关系值得记下来。过去大家觉得策略是人写的，人写的策略靠评审就够了，所以形式化验证一直停在论文里。现在父 agent 要给子 agent 写策略，写出来的东西需要一个可判定的检查器，求解器就有了位置。我怀疑这个模式会扩散到别的安全产品上，只要那个产品的配置开始由模型生成。

第三，「最小权限」正在被加上时间维度。四层执法点那条分界线把控制项分成了不可逆和可逆两类，前者锁死在创建时，后者允许运行时收紧。这件事听起来朴素，但它回答的是一个真问题：权限放开之后还能不能收回来。多数系统在设计权限时只想着怎么给，没想清楚怎么收。

写在最后

NVIDIA 这次的姿态，跟它做 CUDA 的时候是同一套：不发明那个技术，定义那个接口，然后把接口开源到没人能绕开。

隔离技术早就有了，容器、VM、gVisor、Firecracker 都在。Landlock 和 Seccomp BPF 是内核里现成的。SMT 求解器是学术界几十年的东西。OpenShell 做的事情是把这些零件收进一个可插拔的接口和一份统一的策略模型，再配上一个会自己写策略的 Agent 时代所需要的检查器。

至于它会不会成为标准，我觉得决定因素不在技术。它已经开源、已经有 17.8k star、已经有配套的硬件和参考架构。剩下的变量是那些已经在做隔离的公司愿不愿意实现这个接口。从商业上讲，多数公司不愿意；但从工程上讲，客户会用「符不符合 OpenShell 接口」来提需求。