首次机器可验证的 x86 glibc 二进制端到端证明，意味着什么？

第一份机器可验证的 x86 glibc 二进制端到端证明

我在 Hacker News 上刷到一个帖子，标题是 Zellic's and V12's Work on x86 Binary Formal Verification，1 分，0 条评论 来源：HN。点进去之前我以为是个小项目，但博客第一句让我停了下来。作者说，他们相信这是首份已发表的机器可验证证明，覆盖了一个执行静态链接 64 位 x86 glibc 二进制的 Linux 进程的端到端行为 来源：V12。

端到端，意味着证明覆盖的是整个进程的行为。我见过的形式化验证大多停在源代码层面，证明的是 C 或 Rust 代码的性质，编译器怎么把代码变成二进制，不在证明范围内。这次是直接对二进制做证明，而且覆盖的是 glibc 这么基础的库。

作者说，这是 Zellic 和 V12 内部持续合作的一部分，目标是让 x86 程序在二进制级别的形式化验证可扩展 来源：V12。这会是系列博客的第一篇，后续还有更多细节 来源：V12。换句话说，这次发布更像是一次亮相，不是终点。

为什么选择二进制级别：更小的信任基与 x86 的复杂性

为什么要做二进制级别？作者给的第一个理由是信任基。二进制级别的模型更小，覆盖更全面，不需要依赖编译器无 bug 之类的假设 来源：V12。你可以对最终跑在机器上的东西做证明，不用去信任从源代码到二进制这条链条上的任何一环。

这个框架还能覆盖不同编译器、编程语言生成的二进制，甚至直接手写的优化机器码 来源：V12。这意味着，不管你用什么语言、什么工具链，只要产出的是 x86 二进制，就能用同一套方法验证。这对一个安全团队来说，价值很明显。

当然，x86 不是那么好碰的。作者承认，x86 指令集比 RISC-V 这类架构更难建模 来源：V12。但 x86 在现实部署中使用得广泛得多，这个取舍值得。项目从一开始就把前沿模型和专家人工指导结合起来，目标是构建一个可扩展、可复用的 glibc 与 x86 机器码验证工作流 来源：V12。

作者说，形式化验证是“big unlock”，能最小化需要安全分析的信任基 来源：V12。这个说法反直觉。大多数安全审计的结论是“我们的方法没找到 bug”，作者认为形式化验证能提供比这强得多的保证 来源：V12。证明文件很大，但自动检查，不需要人看；需要人工信任和验证的只剩检查器、执行模型这类一次性成本，以及比证明小得多的程序特定语句 来源：V12。

多源交叉验证：HN 元数据与博客声明的对照

回到 HN 的元数据。帖子只有 1 分、0 评论 来源：HN，和博客“系列第一篇”的早期定位吻合。我特意对了 URL，HN 摘要引用的文章链接和博客地址完全一致，标题也一字不差 来源：HN来源：V12。这个结果还没进入社区公开讨论，我不确定这是因为它太小众，还是发布太早。

HN 标题用的是“Work”，博客正文用的是“we believe to be the first”，没有用“we have proven” 来源：HN来源：V12。作者显然在把结果定位为一项工作，未声称已获独立验证。这种克制我欣赏。形式化验证领域的惯例是，作者声称的“第一”需要同行评审和历史考证。

一家公司自己宣布“我们相信这是第一”，和社区确认“这确实是第一”，中间的距离不短。我不确定这份证明最终会不会被承认。但方向是对的。把信任基压到最小，让机器检查证明，人不用去读代码。这个思路，比任何单个证明都更值得关注。

原文：

Zellic's and V12's Work on x86 Binary Formal Verification · 来源：Hacker News

作者：itfan123 值班编辑 · 发布于 2026年10月31日