新大质疑 Anthropic 形式化验证：123 个库的「内存安全」证明有漏洞
xuanalogue · x · 2026-11-01
Anthropic 此前宣布与 Theorem 合作，用 Claude 在数周内为 123 个真实开源库生成形式化证明、验证安全属性。新加坡国立大学 FOCS/KISP 实验室的 Umang Mathur、Prateek Saxena 等人深入检查其公开证明后提出质疑。
- 核心发现：公开的 specification 并未完整刻画「内存安全」的本意（程序只访问有权访问的内存、且时机正确）。
- 后果：一个程序可以满足该 spec 却仍含内存安全漏洞，「verified memory safe」的表述可能让人高估实际保障。
- 关键论点：让 AI 做验证时 spec 尤为重要——模型为让证明被接受，可能利用 spec 的遗漏；AI 使证明更容易生成的同时，更要审视「证明了什么」。
- 作者肯定这是自动验证领域的积极进展，且证明已公开可查，但呼吁对这类声明保持谨慎，避免夸大保障。
「安全」频道最新
- OpenAI 总裁 Brockman 谈用 AI 找并修复软件安全漏洞 — No Priors · 2026-11-02
- UK Biobank 数据泄露后即将重新向研究者开放 — zakkohane · 2026-11-01
- Simon Willison 演示如何接管他人 ChatGPT 账号 — paaloeye · 2026-11-01
- 法官允许 NAACP 起诉 xAI 数据中心污染案继续推进 — SnoozeDoggyDog · 2026-11-01
- Grok Bot 查 iPhone 隐私日志,称 Claude 夜间动用麦克风 312 次 — RachelVT42 · 2026-11-01
- 回应《Against SURA》：对齐难与反 AI 浅薄论可以同时成立 — JacquesThibs · 2026-11-01