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

是什么

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

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

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

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

为什么重要

不理解 VST，下面这些事都没法解释：

• 为什么 CompCert 证明了编译器正确，仍挡不住你的 C 代码本身有 bug
• 为什么 Hoare / separation 逻辑能管指针，却长期停在教科书语言上
• 为什么 DeepSpec 能把 SHA-256、HMAC 证到机器码层仍和数学定义一致
• 为什么”端到端验证”必须同时握住程序逻辑、编译器正确性、战术库三条线

这是 Hoare → separation → 真 C 编译器这条链上，面向真实 C 子集与已验证编译器的早期工业级落地之一。

核心要点

VST 的”章”由三块组成。

1. Verifiable C：CompCert 认得的 C 子集上的 Hoare-style 程序逻辑，规则全用 separation 逻辑（* 表示”两块内存互不重叠”）。类比：合同条款写清每块货架各归谁。
2. Soundness 定理：凡是这套逻辑推出来的 {P} c {Q}，都对 CompCert 的 Clight（C 的一种中间表示，像”还没变成汇编的精简 C”）操作语义成立。类比：海关章在中转仓仍有效。
3. VST-Floyd 战术：把符号执行和规范形自动化，让博士生能在合理时间内证完千行级 C。类比：盖章流水线，不用每页手盖。

合起来：写规约 → Floyd 推出三元组 → soundness 接到 Clight → CompCert 编到 asm，每步都有 Coq 证明。端到端。

VST 还有一个常被忽视的设计：所有内容都在 Coq 里——规约、证明、战术全是显式可重放的项，没有”外部 SMT 突然没回应”的黑盒。代价是要学 Coq；收益是 30 年后同一 kernel 仍能验过。

实践案例

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

C:   int sum(int *a, int n) { ... }
SPEC:
  PRE  [ a 指向长度 n 的数组 ]
  POST [ 返回值 = a 的元素之和 ]
证明: 用 VST-Floyd 推出 { PRE } sum { POST }

逐部分解释：

1. PRE/POST：你承诺的”进门条件 / 出门结果”（海关申报单）
2. VST-Floyd：帮你在 Coq 里推出 Verifiable C 三元组
3. soundness：三元组对 Clight 语义成立
4. CompCert：Clight → asm 保留行为 → asm 也满足同一 PRE/POST

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

swap(p, q):   想交换 *p 与 *q
普通 Hoare:  必须手写"p 与 q 会不会别名"
separation:  PRE = p ↦ x * q ↦ y   (* = 两块互不重叠)

逐步：

1. 若 p 与 q 可能指向同一格，写 *p = z 可能顺带改掉 *q
2. 用 * 写进 PRE，等于声明两块货架分开
3. 赋值 *p = z 后，q ↦ y 自动仍成立——VST 把这翻译成 CompCert 的 block×offset 内存模型

案例 3：mbedTLS HMAC 被证过

Beringer / Petcher / Appel 2015：

C:    mbedTLS 的 HMAC-SHA256
SPEC:
  PRE  [ 密钥与消息已就绪 ]
  POST [ 输出字节 = FIPS 198-1 公式算出的 HMAC ]
证明: VST-Floyd 推出三元组 → CompCert 传到 asm

逐部分解释：

1. FIPS 198-1：监管标准说明书上的数学公式（日常桥接：考试答案卷）
2. PRE/POST：C 实现必须对上这份答案卷
3. 机器码等价：海关章从 C 盖到 asm，源码对、编译对、落地仍对

踩过的坑

1. 证明工作量极大：经验比约 1:30–1:80——证一千行 C 要写三万到八万行 Coq；Floyd 再自动也重，所以多用于”证一次值很多年”的模块。
2. C 的未定义行为是雷区：溢出、悬空指针、对齐违规——spec 必须显式排除 UB，否则证不出来。
3. spec 写错证明也白搭：VST 保证”你证的东西对机器码成立”；PRE/POST 写错（忘了”指针非空”）再漂亮也没用。
4. 改一行就可能重跑大段证明：C 或 PRE 微调，常要重放大段 Coq；学习曲线还要求同时懂 C 内存、separation、Coq、CompCert。

适用 vs 不适用场景

适用：

• 密码学库关键算法（千行级模块；证明/代码行数比常 30–80× 仍划算）
• 内核 / 嵌入式安全关键路径（端到端验证思路，如 CertiKOS 同类目标，未必直接用 VST）
• 需要交给监管看的场景（DARPA / NSF / 高等级安全认证）

不适用：

• 普通业务代码、快速迭代产品（spec 一改证明全废，周级重证成本吃不消）
• 不熟 Coq 的团队（半年起步学习成本可能压垮项目）
• 重度依赖 C 标准库 / 系统调用的代码（VST 对这部分支持有限）
• 需要频繁改接口的库（PRE/POST 一动，下游证明连锁失效）

历史小故事（可跳过）

• 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 仍在降证明成本。

学到什么

1. 形式化证明不必停在源码层：soundness + 编译器正确性接力，可拉到机器码。
2. “工具链”是关键词：整条链每一步都被证，单点证明价值有限。
3. 战术库有工程价值：Floyd 让漂亮但实操爆炸的框架变得能用。
4. 学习路径：先 Hoare → 再 separation → 再 CompCert → 最后才碰 VST；直接上手会被淹没。
5. 可重放是隐性资产：Coq kernel 还在，VST 证明就能再验——工业代码很少有这种时间稳定性。
6. 理论 → 工具 → 落地的接力：1969 Hoare → 2002 Reynolds → 2006 Leroy → 2014 Appel，VST 是这条链当下的尽头之一。

延伸阅读

• 教材主页：Princeton VST（教程与 Coq 库）
• 配套教程：Appel “Verifiable C”（比本书薄的用户手册）
• DeepSpec：deepspec.org
• reynolds-separation-logic —— VST 把这套数学接到真 C
• compcert —— VST 下游，承接证明传递
• hoare-logic —— 一切的起点
• cakeml —— ML 版同类端到端思路

关联

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

反向链接

（暂无反向链接）