Vitalik 长文:AI 破解时代网络安全仍偏防御,形式化验证是终极答案
jessi_cata · x · 2026-09-17
Vitalik Buterin 发文回应「AI 黑客让网络安全完蛋」的流行论调,提出相反判断:网络安全天然偏防御,前提是软件开发方式升级。他本人约 90% 净资产持有加密货币,等于押注这一判断。
- 核心论点:如果 AI 能证明 Navier-Stokes 与费马大定理,那么原则上 AI 也能把「这个程序是安全的」作为数学定理来证明,即使程序非常复杂。「安全」一词隐藏了大量定义上的模糊之处,这是难点所在。
- 形式化验证新浪潮:近几个月以太坊前沿研究圈兴起新范式——直接用低级语言(EVM 字节码、汇编)或 Lean 写代码,再用 Lean 中可自动校验的数学证明验证正确性。Yoichi Hirai 称之为「软件开发的最终形态」:既能产出极高效的代码,又比传统开发方式安全得多。
- 文章脉络:从斐波那契数列「每第三个数是偶数」的归纳法证明示例入手,科普形式化验证的基本概念,并讨论它能做什么、弱点与边界在哪里。
- 作者还转引他人观点指出:目前的主流方案仍是「全程序验证」——数据库、网络、缓存等所有层都要验证,而现代 AI 恰好有能力做这件事;加密货币行业已经在实践从设计上就正确的联网软件。
「安全」频道最新
- OpenAI 披露罕见事件：模型把自己的越狱指令写进上下文压缩摘要 — tomekkorbak · 2026-09-17
- 网友争论 METR 捐款透明度，晒出官网回应资助方质疑 — austinc3301 · 2026-09-17
- METR 资金透明度遭质疑:捐助方是谁、想要什么故事? — kevinnbass · 2026-09-17
- Agent 开发新实践:用「同意记录」把用户授权变成可查数据 — blaizedsouza · 2026-09-17
- Flock 监控摄像头被曝漏洞遍地,源码内藏硬编码凭证 — micahflee · 2026-09-17
- 模型如何区分训练、评测与真实用户推理？仍无人说得清 — flowersslop · 2026-09-17