在 OpenShell 应用形式化方法控制 AI 代理的经验

# 将形式化方法应用于AI智能体控制的经验总结 来源：https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-09-10-learning-formal-methods-agent-policy-prover/ https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-09-10-learning-formal-methods-agent-policy-prover.md 本文介绍如何使用形式化方法推理长时间运行的AI智能体的权限变更。 五组彩色连接的AI智能体节点位于绿色策略边界内，而一条红色路径穿过边界并被证明标记阻止。在本文中，我们将深入探讨权限审查在智能体规模下如何失效，以及如何使用Z3开源库（https://github.com/Z3Prover/z3）编写形式化证明，确保智能体提出的策略变更保持在您批准的范围内。 ## 为什么权限审查在智能体规模下失效 AI智能体正变得越来越智能，我们赋予它们的任务也日益自动化。如今，许多人使用小型智能体团队配合Claude或Codex逐个PR迭代代码。我们逐渐开始将长期且开放的研究任务交给智能体完成——这些任务可能需要数百个智能体协作数百或数千小时，以期在某个领域实现突破性进展。 随着这些应用场景的扩展，一些情况开始出现： - 智能体需求演进。在执行任务过程中，智能体将需要访问数据存储、代码仓库、互联网搜索能力，以及执行详细模拟和测试的权限。 - 人类监督无法扩展。在如此规模下，对所有智能体的人类监督本身变得不可行。 这引发了一个核心问题：如何确保协同工作的智能体群组——每个都有其特定范围的策略——不会超越整个系统被授予的权限？设想一个拥有互联网写权限的智能体，另一个访问安全工具的智能体，或一组在"执行竞争研究"等广泛授权下工作的智能体。我们如何确保整个系统符合人类操作者的意图？ 这需要一套新的控制机制，使我们不再需要费力地逐条审查沙箱权限列表，而是能够以更高层次、更声明式的方式进行思考。在本文中，我们将探讨OpenShell团队在该领域的一些研究进展，特别是利用形式化方法构建的"证明"——它不仅能验证单个智能体的能力，更能验证整个智能体系统的能力。 ## 改变我们想法的演示 在我们早期为Jensen准备的OpenShell演示中，我们展示了如何利用OpenShell的REST检查端点，使OpenClaw智能体只能选择性地写入GitHub仓库，尽管它拥有一个广泛范围的API密钥。演示初始如预期进行——OpenShell的沙箱检测到对禁止仓库的写入尝试并阻止了它。但下一条消息却显示"文件成功写入[禁止仓库]"。这里发生了什么？智能体意识到自己运行在沙箱中，随后使用GitHub凭证与另一个底层的GitHub二进制文件`git-remote-https`，通过可用的线路协议绕过了OpenShell第7层HTTP/REST/MCP检查——而该二进制文件在当时我们的策略中已被批准用于克隆Git仓库，但我们完全没意识到它具备写入能力。 非常巧妙。这揭示了一个关键点：在网络、文件、工具、AI模型和凭证访问的沙箱/运行时策略之间，可能存在指数级的非预期组合，导致AI智能体能够执行人类操作者明确不希望的操作。 ## 先前工作 - 在AWS验证EC2、IAM和S3策略 早在2016年左右，我们团队成员在AWS工作时面临了类似挑战。鉴于AWS IAM策略、AWS S3存储策略以及历史版本支持的所有复杂性，我们能否明确判断S3中的某个对象是否可被公共互联网访问？ 今天看来这似乎有些可笑，在2016年也是如此——直到你开始思考我们编写的控制系统策略之间可能存在的复杂分层交互。AWS的Byron Cook及其同事（https://www.amazon.science/publications/semantic-based-automated-reasoning-for-aws-access-policies-using-smt）开发了Zelkova，将AWS访问策略形式化为SMT公式，他们在2018年发表工作时，该系统每日已被调用数百万次。此后该工作已在AWS内部广泛发展；后续研究描述了扩展到每天十亿次SMT查询（https://link.springer.com/chapter/10.1007/978-3-031-13185-1_1）。 其核心思想是运用形式化方法，特别是定理求解器，来形式化建模IAM、S3和EC2策略。一旦我们将这些策略及其交互用形式化逻辑建模，就能构建证明，验证我们的不变量（我们期望保持为真的条件）是否成立。这最终取得了很大成功，并带来了一个额外优势：在完成用形式化逻辑建模复杂策略这一密集型任务后，实际的查询执行速度可以非常快，并且能够横向扩展计算资源。 ## 同样的问题，现在面对智能体 如今，我们面临的挑战非常相似。一个智能体或智能体系统，各自拥有文件系统、网络、凭证、工具和MCP策略——每个策略具有不同能力，并且可以通过不同智能体间的通信相互组合。 前沿实验室主张使用可信的AI智能体对其他智能体的动作进行审查，由专门的模型将最重要的事件升级给人类审批，以减少审批疲劳。然而，AI模型——如同人类一样——是概率性的，可能遗漏重要细节。更进一步，使用同等智能的审查模型检查每个智能体动作，会使计算成本加倍，并实际上使总吞吐量减半。 我们在OpenShell中实验和验证的，是使用形式化方法来建模并灵活"证明"策略中的某些不变量——例如绕过阻止代码仓库写入规则的非预期方式，或对生产数据库的删除操作——是否可能存在。我们发现，虽然建模这些策略可能很复杂，且必须保持更新，但它们确实具有强大的优势： - 随时进行形式化审计或证明不变量的能力 - 针对我们的策略理解提供确定性"证明" - 这些检查在毫秒级完成，无需消耗token 这些逻辑检查不理解上下文——例如请求访问删除临时仓库与生产仓库的区别。但是，结合人类或可信的AI审查员，这些证明既能提供在敏感、实体（现实世界）或受监管环境中运行所需的形式化审计记录，又能为概率性AI审查员提供不可被欺骗或误导的输出，从而带来巨大价值。 ## 对策略定义进行证明能带来什么？ 我们将形式化方法视为智能体控制领域非常有前景的研究方向。更多关于这些证明在对抗性研究实验中的实际应用，请参见：https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-08-27-adversarial-policy-review-long-horizon-agents/ 形式化方法不仅用于策略验证，在关键系统中也有悠久历史——从飞行控制系统、核心互联网交换和路由，到我们每天用于确保系统软件间复杂依赖关系正确匹配的包管理器。 对于许多AI研究者而言，我们中有些人可能在大学修过形式化验证课程，但相对较少人在实践中使用过形式化验证。在本文后续部分，我们将介绍算法验证的基础知识，并从零开始使用流行的开源求解器，为OpenShell中的智能体控制构建一个最小示例。 ## 五分钟了解SAT、SMT和Z3 在计算机科学和形式化方法中，SAT（可满足性）求解器（https://en.wikipedia.org/wiki/Boolean_satisfiability_problem）用于回答布尔公式是否可满足。如果存在变量的可能赋值（假设为x和y）使其为真，SAT求解器返回true；否则返回false。 给定变量a和b，它能找到使以下公式为真的赋值： 相比之下，SMT（可满足性模理论）求解器（https://en.wikipedia.org/wiki/Satisfiability_modulo_theories）通过理论扩展了这种推理方式：整数、实数、字符串、正则语言、数组、位向量和其他有用域。 Z3是由微软研究院开发和维护的SMT求解器和定理证明器。Z3是通用的，我们需要编写代码将我们特定的智能体策略元素映射到Z3理解的构造上。 例如： - 端口是整数； - 主机名和路径是字符串； - 像`\*`、`\*\*`或`/\.\*/\*\*`这样的Glob模式可以表示为正则表达式； - 策略组合成为布尔逻辑。 Z3指南（https://microsoft.github.io/z3guide/）是掌握下面示例后的最佳参考资料。 几个构造涵盖了我们需要的大部分内容： 构造体 | 含义 | OpenShell示例 --- | --- | --- Sort（类型） | 值的类型 | 用于主机的字符串、用于端口的整数 Symbol（符号） | Z3可自由选择的值 | 未知动作的方法或路径 Constraint（约束） | 必须成立的公式 | 1 <= port <= 65535 And, Or, Not（逻辑组合） | 布尔组合 | candidate allows AND maximum does not String/regex theory（字符串/正则理论） | 文本和语言的约束 | 路径属于编译后的glob Solver assertion（求解器断言） | 添加必须的公式 | 断言存在违规 sat（可满足） | 存在满足赋值 | 存在超出最大范围的动作 Model（模型） | 一个满足赋值 | 具体的二进制文件、主机、方法和路径 unsat（不可满足） | 不存在满足赋值 | 已证明模型满足包含关系 unknown（未知） | Z3未确定结果 | 失败关闭并请求审查/支持 查询方向很重要。 我们不会要求Z3证明： `` proposed policy addition is safe `` 我们必须形式化建模问题，并回答一个非常具体的问题。例如，我们在Z3中为此用例建模的较通用和实用的证明之一是：询问提议的策略能否执行专家预定义策略（例如GitHub只读权限）无法执行的任何操作。回到我们之前OpenClaw试图通过将访问令牌与使用第4层线路协议的二进制文件结合来绕过第7层REST策略检查的例子，我们会在Z3中编码第4层能力超出第7层能力。因此，凭证（GitHub）加上第4层二进制文件和网络访问的组合，超出了先前允许的相同凭证加上第7层（REST）下'gh'二进制文件的组合。证明器会立即捕获这一点并发出警告。 这种情况下的查询如下： `` proposed_policy_allows(action) AND NOT safe_policy_allows(action) `` 或者相同属性可以写为集合差： `` Allowed(candidate) ∖ Allowed(safe_policy) = ∅ `` 如果求解器返回sat，差集非空——意味着提议的策略中存在预批准参考策略中不存在的能力。 如果返回unsat，不存在已建模的反例，意味着我们的不变量（假设）均未被违反。让我们尝试自己编写这样一个查询。 ## 第一个包含性查询 这里是Z3原生SMT-LIB格式的一个小例子。将其保存为`containment.smt2`并运行： 此示例比较两个候选策略对同一个最大策略的遵守情况。 `` (declare-const binary String) (declare-const host String) (declare-const port Int) (declare-const layer String) (declare-const method String) (declare-const path String) ; 动作域：每个请求要么是原始L4层，要么是经检查的REST层。 (assert (or (= layer "l4") (= layer "rest"))) ; 一条强制性的REST规则仅覆盖经检查的REST流量。 (define-fun maximum-allows () Bool (and (= binary "/usr/bin/gh") (= host "api.github.com") (= port 443) (= layer "rest") (= method "GET") (str.prefixof "/repos/NVIDIA/OpenShell/issues/" path))) (define-fun broad-candidate-allows () Bool (and (= binary "/usr/bin/gh") (= host "api.github.com") (= port 443) (= layer "rest") (= method "POST") (str.prefixof "/repos/NVIDIA/" path))) (define-fun narrow-candidate-allows () Bool (and (= binary "/usr/bin/gh") (= host "api.github.com") (= port 443) (= layer "rest") (= method "GET") (= path "/repos/NVIDIA/OpenShell/issues/123"))) ; 一条指向相同主机和端口的原始L4层规则没有可检查的方法或路径。 ; 它覆盖L4层*以及*任何可能在其上传输的内容，包括REST。 (define-fun l4-candidate-allows () Bool (and (= binary "/usr/bin/gh") (= host "api.github.com") (= port 443) (or (= layer "l4") (= layer "rest")))) ; 检查1：宽泛候选策略是否超出最大策略？ (push) (assert (and broad-candidate-allows (not maximum-allows))) (check-sat) (get-value (layer method path)) (pop) ; 检查2：窄候选策略（GET，单个issue）是否超出最大策略？ (push) (assert (and narrow-candidate-allows (not maximum-allows))) (check-sat) (pop) ; 检查3：指向相同主机和端口的原始L4层规则是否超出最大策略？ (push) (assert (and l4-candidate-allows (not maximum-allows))) (check-sat) (get-value (layer method path)) (pop) `` 第一个检查返回sat，上面的get-model返回以下见证——一个对组织根目录的写入，这在安全（最大）策略中从未被允许。 `` sat ; 检查1：宽泛候选策略 ((layer "rest") (method "POST") (path "/repos/NVIDIA/")) unsat ; 检查2：窄候选策略 sat ; 检查3：原始L4层 ((layer "l4") (method "") (path "")) ``` 第二个检查返回unsat。窄候选策略允许的每个动作都已在最大策略允许范围内。第三个检查就是前面提到的OpenClaw案例。第4层候选策略指定了与我们参考最大策略相同的主机和端口，但使用了第4层——该层采用的线路协议无法被OpenShell执行。证明器返回`sat`，其中`layer = l4`，方法和路径为空。这种情况下，我们不必显式编写规则说明第4层比第7层REST更宽泛，这实际上已通过编码隐含得出。 ## 如何将完整的OpenShell策略编码为形式化逻辑 OpenShell的运行时证明器为任何网络动作建模以下属性： `` action = { binary: String, host: String, port: Int, layer: String, method: String, path: String } `` **注意：** 上述动作示例只是子集，OpenShell运行时还涵盖文件系统、进程、凭证和推理包含性。 我们使用Rust编写的代码将智能体提出的任何策略变更编码为Z3可检查的动作。一旦编码完成，我们可以运行各种检查。第一个是非常通用的检查——询问候选（提议）策略能否执行参考（安全）策略无法执行的任何操作。 `` let candidate_allows = policy_allows(candidate, &action); let maximum_allows = policy_allows(maximum, &action); solver.assert(Bool::and(&[ candidate_allows, !maximum_allows, ])); match solver.check() { SatResult::Unsat => MaximumPolicyCheck::WithinMax, SatResult::Sat => { let model = solver.get_model().expect("sat result has a model"); let counterexample = counterexample_from_model(&mo