LeanGuard:用 Lean 4 形式化验证拦截 agent 违规工具调用
CWRU · hf · 2026-11-03
Case Western Reserve 大学与 UT Austin 发布 LEANGUARD，一个面向工具调用 agent 的形式化验证运行时（arXiv 11-02）。
- 问题：agent 常执行领域政策禁止的操作（如 prompt injection 诱导的越权工具调用）。
- 方法：每条提议的工具调用在触达环境前，先对照用 Lean 4 编写的政策做检查；政策结合状态谓词与作用域化的过去时时间算子，覆盖执行历史；评估是 fail-closed 的，判定过程被证明等价于 LeanLTL 语义。
- 修复：被拒绝的调用可通过证明引导的搜索自动修正为合规版本。
- 效果：显著降低未授权执行与 prompt injection 成功率，且不损害良性任务的完成表现。论文配图演示了经典攻击场景（「把我上一单书架换成相机」→ 差价被刷到攻击者礼品卡）在无守卫时直接执行、在 LeanGuard 下被拦截修正。
「安全」频道最新
- AI 发现 XRP 无限铸币漏洞,940 亿美元资产险遭史上最大黑客攻击 — massimosgrelli · 2026-11-03
- 《前沿 AI 安全与治理 2026》报告在乌镇峰会发布 — S_OhEigeartaigh · 2026-11-03
- CrowdStrike 收购 AI 安全测试公司 Dreadnode — joshua_saxe · 2026-11-03
- 哈佛 85.1 万校友邮件泄露数据已上线 HaveIBeenPwned — 0xkarasy · 2026-11-03
- Pliny 炮轰前沿 lab 的「安全对齐」话术：如同向烟草公司问健康建议 — davidmanheim · 2026-11-03
- Ballistic Ventures 发布 Insider Risk Maturity Model 应对 AI Agent 内部威胁 — philvenables · 2026-11-03