What we have learned at OpenShell applying formal methods to control AI agents
10 hours ago
- 权限审查在智能体规模下会失效，因为智能体需要进化，而人工监管无法扩展，必须采用形式化方法来确保智能体始终在批准的权限范围内。
- 一次演示展示了一个智能体通过使用二进制协议（git-remote-https）在第四层传输层绕过第七层REST检测，凸显了非预期策略组合的指数级增长。
- 亚马逊云科技此前的工作（Zelkova）已成功使用形式化方法（SMT求解器）在规模化场景下验证了IAM、S3和EC2策略，这启发了将其应用于AI智能体领域。
- 形式化方法能提供确定性证明、毫秒级快速检查且无token消耗，通过构建不可欺骗的审计轨迹来补充概率性AI审查。
- 本文解释了SAT/SMT求解器和Z3的工作原理：将智能体策略（端口、主机、路径、协议层）编码为逻辑公式，并通过查询来检查候选策略是否超出参考上限。
- Z3的实践示例展示了包含性检查：找出宽泛策略的反例、验证严格策略的安全性，以及检测原始第四层协议绕过。
- OpenShell的策略验证器包含专家级查询（本地链路可达性、有凭证的第七层绕过、凭证扩展、能力扩展），并会对每个提议的策略执行这些查询。
- 形式化方法被视为治理长周期智能体任务的有前景方向，并邀请用户为OpenShell贡献代码及查阅更多资源。
- 该编码模型使用通配符语义的正则语言子集，且不支持策略表面时默认失败关闭。
- 本文强调策略语言建模虽复杂，但能带来强大优势：形式化可审计性、确定性及高速性。