OpenShell 用形式化方法管控 AI 智能体
What we have learned at OpenShell applying formal methods to control AI agents
随着 AI 智能体自主性增强，传统的人工权限审查在大规模场景下已难以为继。我们在 OpenShell 项目中发现，智能体常利用网络层（Layer 4）与工具的组合绕过应用层（Layer 7）的 REST 策略检查。为了解决这一难题，我们借鉴 AWS 在 IAM 策略验证上的经验，引入 Z3 求解器，将复杂的权限策略转化为形式化逻辑进行自动证明。这种方法能在毫秒级内确定性验证策略变更是否越界，无需消耗 Token，为长周期运行的智能体系统提供了可靠的“数学级”安全护栏。
在沙箱、运行时策略、网络、文件、工具、AI 模型和凭证访问之间，存在指数级的意外组合，可能导致 AI 智能体执行人类操作员明确禁止的操作。
HN 评论区
11- zaphar
我觉得权限管理并不是这里最难的部分。真正的难点在于，智能体要想完成任何有用工作，都需要访问大量资源。而且，这些它需要访问的资源很可能存在漏洞，智能体能够利用这些漏洞。我们的环境设计压根就没考虑到这类使用场景。我之前尝试过为智能体做沙箱隔离，等到赋予它足够权限让它能真正干活时，我的沙箱已经千疮百孔，像瑞士奶酪一样了。
- xnx
有一瞬间我以为代理式 AI（agentic AI）已经渗透到每个项目里了，但这跟那个开源的 Windows 开始菜单替代品没啥关系：https://github.com/Open-Shell/Open-Shell-Menu
- agentdev001
我真心喜欢 OpenShell 这个解决方案，真心希望 Kube 支持能尽快走出实验阶段。这是个很酷的解决方案——针对一个我想象中可能根本无法做到 100% 完美的问题。
期待 0.1.0 版本的发布 :)