VST — 把 C 程序的数学证明一路带到机器码

是什么

VST（Verified Software Toolchain，可验证软件工具链）是一本书，也是一套真能跑的 Coq 库。它干的事可以一句话说清：让你在 Coq 里证明一段 C 代码满足某个规约，然后这个证明会顺着 CompCert 编译器一路传到机器码上，不掉链子。

日常类比：跨国快递的海关盖章。

你在源头（C 代码）寄一个箱子，海关盖章说”里面是合法物品”
中转（编译）时海关章不能被撕掉、不能被换
终点（机器码）开箱时章还在，谁都没法做手脚

VST 干的就是把”逻辑证明”做成那个永远撕不掉的章。这本书 600 多页，讲清楚这个章具体怎么盖、怎么传。

为什么重要

这是 Hoare 逻辑 → separation 逻辑 → 真 C 编译器 三步合体的第一次工业级落地。

在 VST 之前的状况：

Hoare 逻辑（1969）只对教科书的 while 语言成立
separation 逻辑（Reynolds 2002）能管指针，但还是教科书语言
CompCert（Leroy 2006）证明了 C 编译器自己正确，但没人替你证 C 代码本身正确

这中间有一个鸿沟：就算编译器不出 bug，你的 C 代码本身可能就有 bug。VST 把这个鸿沟填上——你证 C 代码满足 spec，VST 保证这个证明对编译出来的汇编也成立。

DeepSpec NSF Expedition（Appel 主导的大项目）整个栈都用 VST：SHA-256、HMAC、HMAC-DRBG、mbedTLS 的关键模块都被 VST 证过。

核心要点

VST 的”章”由三块组成。

Verifiable C：CompCert 认得的 C 子集上的一套 Hoare-style 程序逻辑，规则全用 separation 逻辑（带 * 的合取，“两块内存互不重叠”那种）。
Soundness 定理：在 Coq 里证明，凡是这套程序逻辑能推出来的三元组 {P} c {Q}，都对 CompCert 的 Clight 操作语义成立。这是”章不会掉”的数学保证。
VST-Floyd 战术：硬证 separation 逻辑会累死人，VST 提供一套 Coq 战术，把符号执行和规范形（canonical form）自动化掉，让一个普通博士生也能在合理时间内完成千行 C 的证明。

合起来：你写规约 → 用 VST-Floyd 推出 {P} c {Q} → soundness 把它接到 Clight → CompCert 把 Clight 编到 asm，每一步都有 Coq 证明。端到端。

VST 还有一个常被忽视的设计：所有内容都在 Coq 里。规约用 Coq 写，证明用 Coq 写，连战术也是 Coq 战术。这意味着没有”外部 SMT 求解器突然没回应”那种黑盒——一切都是显式构造、可重放、可审计的项（term）。代价是要学 Coq；收益是再过 30 年这个证明仍然能被同一个 kernel 检验通过。

实践案例

案例 1：盖章传递的全过程

你写的 C 代码：
  int sum(int *a, int n) { ... }

你写的 spec（Coq 里）：
  PRE  [ a 指向长度 n 的数组 ]
  POST [ 返回值 = a 的元素之和 ]

你做的事：
  用 VST-Floyd 战术，在 Coq 里推出
  { PRE } sum 的代码 { POST }   ← 这是 Verifiable C 的三元组

接下来不用你管，VST + CompCert 替你做：

soundness 定理：上面的三元组对 Clight 语义成立
CompCert：Clight → asm 保留行为
结论：asm 代码也满足那个 PRE/POST

这就是”章一路到机器码”。

案例 2：为什么必须是 separation 逻辑

普通 Hoare 逻辑写 swap(p, q) 会很难，因为 *p 和 *q 可能是同一块内存（别名）。每条赋值你都得把”会不会被别名干扰”写进前置条件。

separation 逻辑用 p ↦ x * q ↦ y（* 表示”两块互不重叠”）一句话解决——只要前置条件这么写，编译器读到 *p = z 就知道 q ↦ y 没被动过。VST 把这套机制翻译成对 CompCert 内存模型（block × offset 二维地址）的具体操作。

案例 3：mbedTLS HMAC 被 VST 证过的真实例子

Beringer / Petcher / Appel 2015 工作：

C 实现：mbedTLS 现成的 HMAC-SHA256 代码
Coq spec：FIPS 198-1 标准里 HMAC 的数学定义
证明：C 代码每次调用都和数学定义产出同样字节
价值：编译出来的 mbedTLS 库，机器码层面和 FIPS 标准等价

这是密码学库少有的端到端保证。

踩过的坑

证明工作量极大：经验比是 1:30 到 1:80 ——证一千行 C 要写三万到八万行 Coq。VST-Floyd 把战术做得很自动，但还是非常重。这是为什么 VST 主要用在密码学和操作系统内核这种”证一次值很多年”的场景。
C 的未定义行为是雷区：整数溢出、悬空指针、对齐违规——CompCert 的 C 语义对这些有明确规定（很多算 UB，整个程序行为不保证）。你的 spec 必须显式排除 UB，否则证不出来。Appel 在书里花了好几章讲这个。
spec 写错证明也白搭：VST 保证”你证的东西对机器码成立”。但你证的是什么取决于你写的 PRE/POST。spec 写错（比如忘了说”指针非空”），证明再漂亮也没意义。这是所有形式化方法的通病。
学习曲线：得同时懂 C 内存模型、separation 逻辑、Coq、CompCert 中间表示。Appel 这本书 600 页就是为了把这条曲线压平，但仍然只适合愿意投半年起步时间的人。

适用 vs 不适用场景

适用：

密码学库（关键算法的端到端保证）
操作系统内核关键路径（CertiKOS 用了类似思路）
安全关键嵌入式（航天、医疗设备的核心子模块）
需要”证给监管看”的场景（DARPA / NSF / 高等级安全认证）

不适用：

普通业务代码（成本不划算）
快速迭代的产品（spec 一改证明全废）
不熟 Coq 的团队（学习成本可能压垮项目）
重度依赖 C 标准库 / 系统调用的代码（VST 对这部分支持有限）

历史小故事（可跳过）

2002 年：Reynolds 把 O Hearn / Ishtiaq 的工作整理成 separation 逻辑。能管指针了，但只对玩具语言。
2006 年：Leroy 的 CompCert 把”编译器自己被证”做成现实。中间表示是 Clight。
2011 年：Appel 团队第一篇 VST 论文，把 separation 逻辑的可靠性证到 Clight 语义上。
2014 年：这本书出版，把 8 年的工作整理成可读的 600 页教材兼参考手册。
2015 年起：DeepSpec、mbedTLS HMAC、SHA-256 一系列实战项目用 VST 证下来。
2020s：VST 仍然在演进，重点是降低证明成本（更自动的战术、自动化合成 spec）。

学到什么

形式化证明不必停在源码层：通过 soundness + 编译器正确性的接力，可以一直拉到机器码——这个思路是 VST 给业界的最大启发。
“工具链”是关键词：单点证明（一个语言、一个编译器、一个库）价值有限，VST 强调的是整条链上每一步都被证。
战术库的工程价值：VST-Floyd 让一个数学上漂亮但实操爆炸的框架（separation 逻辑 + CompCert 内存）变得能用——好理论 + 好战术 = 真能跑。
学习路径：先 Hoare → 再 separation → 再 CompCert → 最后才碰 VST。直接上手会被淹没。
可重放是隐性资产：30 年后只要 Coq kernel 还能跑，VST 证明仍然能被同一套规则验过——工业代码很少有这种时间稳定性。
理论 → 工具 → 落地的接力：1969 Hoare → 2002 Reynolds → 2006 Leroy → 2014 Appel，每一步都是”上一代成果再往前推一格”，VST 是这条链当下的尽头。

关联

reynolds-separation-logic —— VST 的逻辑基石；VST 把它从玩具语言搬到 CompCert C
compcert —— VST 下游编译器；soundness 接的就是 Clight 语义
hoare-logic —— VST 程序逻辑的原型，VST 加了 separation * 算子
cakeml —— ML 路线的对照实验，端到端思路一致但语言不同
isabelle-hol-2002 —— 同样级别的证明助手，Appel 选了 Coq
calculus-of-constructions —— Coq 的理论根基，VST 全部建在它上面