开发者为 OpenCode 推出静态验证插件 拦截不安全 AI 工具调用

一位开发者基于 Erik Meijer 的形式化验证论文「Guardians of the Agents」及其参考实现，为 AI 编程代理工具 OpenCode 构建了一款安全验证插件，在工具调用执行前进行静态检查，阻止路径穿越、密钥泄露等不安全操作。

背景与设计思路

该插件的设计灵感来自 Erik Meijer 撰写的论文「Guardians of the Agents」，该文探讨如何对 AI 工作流进行形式化验证；参考实现由 Nada Amin 完成并开源在 Guardians 仓库。开发者在此基础上，将验证能力以插件形式接入 OpenCode 的 TypeScript 插件体系，从而在不动核心验证器的前提下，为 AI 代理加上了一层「安全闸门」。

工作机制

插件通过四个步骤完成拦截与验证，整体开销约 1.5 毫秒：

• 拦截：利用 OpenCode 提供的 TypeScript 插件钩子「tool.execute.before」，在 bash、read、edit、write 等工具调用真正执行前截获候选请求。
• 旁路验证：将工具参数转发给本地运行的 Python 守护进程，统一调用 guardians.verify()。
• 形式化检查：使用 Z3 求解器进行路径包含判断，阻止诸如 ../../../../etc/passwd 这类路径穿越攻击；对 .env 等敏感数据进行污点追踪，避免其流入输出文件或 shell 命令；并通过安全自动机强制执行「先读后编辑」等规则。
• 预执行中止：一旦检测到违规，插件立即抛出异常，阻止任何对磁盘的副作用，迫使 AI 代理自我修正后再发起调用。

实现与集成

仓库通过将 metareflection/guardians 直接以 Git 子模块（命名为 guardians-core）的形式引入，保持核心验证器与上游同步更新，避免分叉带来的维护负担。项目源码与安装说明已在 GitHub 开源，开发者公开征求社区反馈与改进建议。