C*: Unifying Programming and Verification in C
Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao, Zhenjiang Hu
cs.PL, cs.SE
2025-04-03
北大与上交把分离逻辑符号执行和HOL Light证明核嵌进C,证明用C来写。10个小程序加pKVM的attach_page过了验证,后者57行实现配1616行证明。
C 写的系统软件要形式化验证,现成工具把写代码的人挡在门外。一类做法把 C 翻进 Coq,在定理证明器里做证明,VST、AutoCorres、Live Verification 都走这条路,程序员要学一套完全不同的证明范式。另一类把断言或精化类型写回 C 源文件,Frama-C、VST-A、RefinedC、CN 属于这一类;自动化不够时,还是得切回 Coq。VeriFast 允许写有限的证明命令和 ghost lemma,证明能力固定,用户扩不了。
北大与上海交大的 C 想同时做到三件事:验证写在 C 里、证明能力够用、写下一行代码时能看见当前证明状态。目标读者是写内核和分配器的人,不是定理证明专家。
C 在 C 上叠了两套已有技术:分离逻辑的前向符号执行,加上 LCF 风格的高阶逻辑证明核。后者直接复用 HOL Light 的 OCaml 内核,没有在 C 里从零再造一个证明器。分离逻辑在 HOL Light 里被公理化,堆解释成地址到字节的有限映射,
规格用 C 属性写。函数前置条件是 [[require]],后置是 [[ensure]],循环不变量是 [[invariant]]。断言里的分离逻辑谓词用反引号包成 quotation,可以插值。谓词是 C 里的一等值,C 类型是 term,对象逻辑类型是 hprop。标准库提供 dataat、undefdataat、arrayat 这类 maps-to 谓词,用户也能自己定义归纳类型和表示谓词,比如用 llrepr(p, l) 把链表指针和逻辑层的整数列表接起来。
证明写在 [[proof]] 块里,里面是普通 C:可以声明变量、调函数、写循环。证明块从符号执行引擎取出当前符号堆 getsymbolicstate(),用一条已证的分离逻辑蕴涵改它,再 setsymbolicstate() 写回去。引擎有一条硬约束:执行赋值或解引用前,被访问地址的 dataat / undefdataat 必须作为分离合取的一项显式出现。不在,就得先写证明,把数组或用户谓词拆成引擎认识的形状。论文里的 clear 例子就是这样:循环不变量只说「后面是一段未初始化数组」,存一个字节之前,证明过程 singleoutlocation 先把这段数组的头元素拆出来。
这对应两种验证风格。声明式:在程序点断言期望状态,引擎生成验证条件,后面批量证。操作式:证明块当场改符号状态,跟符号执行交错跑,这就是他们说的实时验证。部署阶段验证注解都是 C 属性,gcc 或 clang 直接编译,证明代码被忽略。
证明检查分三阶段。编译器把实现切成被证明块隔开的片段。操作式证明程序把片段喂给符号执行引擎并跑证明块。残余证明程序处理没消掉的验证条件。标准库里的 localapply 负责最烦的结构活:把要改的合取项抬到最左,套帧规则,再把存在量词补回去。证明规则就是返回 thm 的 C 函数。
评测是 10 个小程序加一个真实案例。小程序多改编自 VeriFast 仓库,buddy 分配器例子来自 CN,另有几条为了测复杂控制流手写。
| 程序 | 实现行 | 证明块 | 验证条件 | 证明行 | 规格/断言行 |
| swap | 15 | 0 | 0 | 0 | 7 |
| mallocfree | 9 | 1 | 0 | 9 | 8 |
| clear | 9 | 7 | 0 | 120 | 11 |
| reverse | 18 | 7 | 1 | 375 | 58 |
| attachpage | 57 | 6 | 3 | 1616 | 451 |
swap 纯声明式就能过,零行证明。清零函数 clear 9 行实现配 120 行证明。链表原地反转 reverse 要 375 行证明,还补了 4 条逻辑引理和 2 条所有权引理,这些引理可以复用。真实案例是 Android pKVM 伙伴分配器的 attachpage:57 行实现,451 行规格,1616 行证明,证明对实现大约 28 倍,规格大约 8 倍。验证时发现 CN 原文规格不够强,推不出所有空闲块都在双向链表里,C 沿用了这套更弱的规格。
覆盖了多分支、互递归、break/continue/提前 return、全局变量、可取地址的局部变量、多层指针、malloc/free。不支持 switch、goto、for、do-while。两个本科生做完这套评测。
对写内核、hypervisor、分配器的人,这条路的卖点是证明语言就是 C。Live Verification 也能边写边证,证明脚本是 Coq 的 Ltac,和写 C 是两套肌肉记忆。VeriFast 自动化更好,证明接口是固定命令集。C 把可扩展性押在「证明规则就是 C 函数」上,专家做成库,普通程序员调用。
眼下还不能当生产工具。没有 IDE 显示符号状态,没有 SMT 后端消平凡事实,分离逻辑结构变换要写不少样板。两个本科生列的痛点就是这三条。它更接近一个语言设计原型:证明如果能写成 C,写系统软件的人会不会自己验。
原型和论文里画的理想工作流有缺口。作者拿不到外部符号执行引擎的内部状态,每个证明块要手动跑两遍引擎,一遍取状态、一遍写回。这和「写一行就能看当前堆」差一截。
信任基包含符号执行引擎、HOL Light 内核、以及那套分离逻辑公理。证明程序是 C,内核是 OCaml,中间靠接口粘。
评测规模小。attachpage 是单函数,不是整个分配器。没有和 VeriFast、CN、VST 在同一程序上比证明长度或人时,也没报告验证耗时。不支持的 C 特性都是系统代码里常见的。接 Z3/Why3、补 IDE、扩证明库,都写在未来工作里,还没做。