OpenShell 用形式化方法审权限，证明的边界仍取决于模型
在 OpenShell 团队的研究文章中，研究者尝试把 Agent 提出的权限变化编码为逻辑约束，再用 Z3 判断它是否超出预先批准的安全基线。文章同时讲述了一次演示中，凭据与另一种网络访问方式组合后绕过既有检查的教训。
作者：韩启明｜OC 政策与安全编辑
在 OpenShell 团队的研究文章中，研究者尝试把 Agent 提出的权限变化编码为逻辑约束，再用 Z3 判断它是否超出预先批准的安全基线。文章同时讲述了一次演示中，凭据与另一种网络访问方式组合后绕过既有检查的教训。
一句话结论：形式化方法可以严格回答已经建模的问题，但不能替人保证模型没有遗漏现实中的能力。
单项都合理，组合起来却可能越界
允许读取代码、允许访问某个主机、给一个工具使用凭据，单独看都可能符合工作需要。问题是，不同能力组合之后，是否出现了审批者没有想到的新路径。
这比“这个命令看起来危险吗”更复杂。安全边界有时不在工具名称，而在它能够使用的协议、方法、目标资源和凭据范围。
随着 Agent 运行时间变长，权限调整变多，逐条人工回忆这些关系会越来越困难。形式化验证试图把一部分重复检查变成明确、可复算的逻辑问题。
它实际上在寻找反例
一种核心查询是：有没有某个动作，新策略允许，而安全基线不允许？如果找到了，这个动作就是超范围的具体证据。
如果没有找到，并且求解器完成了证明，则表示在当前形式模型里不存在这样的反例。这个结论比模型回复一句“看起来安全”更具体，也更便于审计。
但“在当前模型里”几个字不能省略。它既是形式化方法的精确之处，也是不能夸大的边界。
没写进模型的能力，不会被凭空发现
如果建模者误以为某个二进制只能读取，而它实际上还能写入，求解器不会自动获得这份操作系统知识。它会忠实推导输入的规则，而不是替人检查所有实现细节。
同样，策略定义与运行时执行必须一致。逻辑上禁止了一条路径，如果代理层没有真正拦截对应流量，证明和实际系统之间就出现了缺口。
所以需要维护的不只有策略文件，还包括策略语义、能力描述和执行机制。一次成功证明不是以后所有版本的永久认证。
不确定结果应有明确去处
文章区分了可满足、不可满足和未知等求解结果。对权限控制而言，未知不能被悄悄当成“没有发现问题，所以通过”。
某些不支持的策略表达或求解困难，需要进入进一步审查。否则，系统越复杂，越容易在最需要谨慎的地方退回默认放行。
这也是自动审批产品应当向用户展示的状态：被证明在界内、发现超界证据、尚不能确定，三者对应不同的下一步。
人工判断并没有失去位置
逻辑检查不理解业务背景。一项删除权限针对临时测试库还是生产库，资源命名是否可信，任务是否真的需要新增能力，都仍涉及上下文判断。
合理分工是让形式化检查提供边界与反例，让人或受信任的审查系统判断任务意图和业务必要性，再由运行时执行最终约束。
这样的组合不是“数学取代安全团队”，而是把人容易疲劳的重复推理交给确定性工具。价值在于减少含糊批准，而不是制造一张宣称绝对安全的证书。
关键事实
材料属于 OpenShell 研究与工程说明；Z3 检查候选策略与批准基线的包含关系；证明依赖建模范围和运行时语义；未知结果不应当作批准。
OC 判断
形式化验证最有用的输出是具体边界和反例，不是没有适用条件的安全口号。
为什么重要
长期 Agent 的权限会持续演变。能够解释一次扩大究竟新增了什么，比让审查者反复阅读长名单更容易形成可靠治理。
评论
围绕这篇文章补充信息、提出问题或分享观察。