CheinTian / notes
Clipping · 9 分钟

形式化验证 LLM 生成的代码（FATTW 2026, Lucas Cordeiro）

FATTW 2026 会议演讲（与 ASE 2026 联合举办）：LLM 负责猜测（不变量、契约、harness），证明引擎负责裁决（ESBMC/k-induction/Vampire）。以 310,531 个 C 程序基准、Test-Comp/SV-COMP 竞赛成绩和 AWS/NVIDIA/vLLM 生产代码漏洞为证据，论证『模型建议 + 证明引擎确认』的设计原则。

ssvlab.github.io Lucas Cordeiro (The University of Manchester / UFAM)
#clippings#AI#LLM#formal-verification#model-checking#symbolic-execution#esbmc#SMT#FuSeBMC#ibmc#SpecVerify#k-induction#LLM-agent

📝 摘要

本演讲论证一个核心论点：LLM 生成代码的速度已远超人类审查能力，而大多数 AI 生成代码当前无法被认证。解决方案不是让 LLM 直接给出结论，而是让 LLM 与证明引擎分工协作——LLM 负责快速猜测（循环不变量、契约、spec、测试输入、harness），证明引擎负责穷尽裁决（ESBMC、Vampire）。

核心概念：「模型建议，证明引擎确认」（The design rule: Let the model suggest, but let the proof engine confirm）。LLM 快但不 sound，验证器 sound 但慢，接口（interface）的设计本身即研究问题。错误的不变量只拖慢时间，绝不牺牲正确性；但错误的 spec 会静默放行错误——spec 必须有人类把关。

关键技术栈 / 关键要点：

  1. ESBMC — 开源 context-bounded model checker，支持 C/C++/CUDA/CHERI/Java-Kotlin/Python/Rust/Solidity 等，流程为 source → CFG → 符号执行 → 验证条件 → SMT solver → 属性成立 / 反例 / unknown
  2. k-induction — 三步：B(k) 基例找真 bug、F(k) 前向条件、I(k) 归纳步；无限循环卡住时加一个不变量即可闭合证明
  3. 三大协同模式 — A. FuSeBMC（工具协同：BMC+fuzzing 共享覆盖目标，Test-Comp 2026 三项第一）；B. ibmc（LLM 提不变量 → Vampire 验证可归纳性 → ESBMC 用之证明，ASE 2024 杰出论文，101/133 程序证明成功且无一错误）；C. SpecVerify（LLM 从自然语言需求生成属性，Claude 路线 0 误报并发现 2 个浮点错误，GPT-4o 路线 8 个误报）

关键结论 / 实践建议： 零误报比更高的证明率更重要（开发者会因狼来了而放弃工具）；可复现的反例是赢得上游修复的关键（18 个修复被上游合并，含 AWS SDK for C++ 2 个 CVE）。五个经验 + 三个待解挑战（验证速度追上生成速度、agent 工作流的保证、可信证据链）详见下文。

1. 背景：图灵 1949 年的问题，至今未解

  • 1948 Manchester Baby——第一台存储程序计算机。「存储的程序就是数据：可以被另一个程序写、改、生成」。程序正确性之问由此诞生
  • 1949 Turing 《Checking a Large Routine》发问："How can one check a routine in the sense of making sure that it is right?" 答案雏形：程序点上的断言 + 停机论证
  • 1967–69 Floyd / Hoare：断言与不变量成为逻辑（Hoare logic）
  • 现状 生成式 AI：代码写得比读得快，「没有人类在循环中」

四次图灵奖构成演讲的地基（目标：让正确性机器可检验）：

年份 得主 贡献
1978 Robert W. Floyd 创立自动程序验证子领域
1980 C. A. R. Hoare Hoare logic：前置/后置条件、不变量
1996 Amir Pnueli 时序逻辑，程序与系统验证
2007 Clarke, Emerson, Sifakis 模型检测技术——ESBMC 的直接系谱所在

2. 差距：好的代码便宜了，审查者离开了

大规模基准：最好的模型也只有 1/6 通过验证

310,531 个 C 程序 × 9 个 LLM，全部做模型检测（FormAI 研究）：

模型 程序数 VS %（通过正式验证）
CodeLlama-13B 11,838 15.48%
Llama2-13B 17,779 12.36
Gemma-7B 36,787 11.62
GPT-3.5-turbo 76,168 7.29
GPT-4o-mini 38,921 4.23%（最新反而最低）
全部 9 个 310,531 8.27%

📎 Tihanyi, Bisztray, Ferrag, Jain & Cordeiro, "How secure is AI-generated code", Empirical Software Engineering 30(2):47, 2025

  • 检查失败 ≠ 程序坏了——只意味着无法认证，这本身就是问题
  • 不是模型发布问题——最新模型得分最低，说明是全行业性挑战
  • 代码便宜了，审查者却走了：Google 称 75% 新代码由 AI 写（Pichai, Google Cloud Next, 2026-04）；Anthropic 称超 80% 合并代码由 AI 生成（"When AI builds itself", 2026-06）；agent 交付结果而不是步骤，没人审查步骤
  • 成本曲线：代码生产成本陡降、知道它正确的成本几乎不降 → 「未验证代码」鸿沟面积急剧扩大

为什么不能只靠「更多测试」或「第二个模型」？

  • 更多测试：测试采样输入，if (x == 0x13371337) 这种条件只在 1/2³² 的输入命中。一项研究里 661 个被 ESBMC 证实的违规，598 个逃过了所有 sanitizer 运行
  • LLM 评审：换一个同样不可靠的裁判，还常与生成器共享训练数据（"Looks correct to me."）
  • 形式化验证：每个输入都有证明，或给出可执行反例；但过去需要专家写属性/不变量——而这不变量恰好就是模型擅长的猜测对象
  • Rust 也救不了：Safe Rust 排除内存破坏，排除不了逻辑错误

3. 引擎：ESBMC 与 k-induction

ESBMC 一览

  • 开源 context-bounded model checker**，检测或证明运行时错误不存在**（C/C++/CUDA/CHERI/Java-Kotlin/Python/Rust/Solidity，单/多线程）
  • 流水线：Source program → Control-flow graph → Symbolic execution → Verification conditions → SMT solver
  • 三个输出：Property holds（属性成立）/ Counterexample（可执行反例）/ Unknown
  • 许可证 Apache 2.0；资金来自 Arm、Intel、NVIDIA、EPSRC、Ethereum F.、Rust F.、EU H2020 ELEGANT、UKRI
  • 获 ASE 2023 Most Influential Paper Award（该 ASE 2009 论文）
  • 输出是机器可复核的证据，不是置信度分数

k-induction：从有界搜索到无界证明

  • B(k) 基例：BMC 深度 k，找真 bug
  • F(k) 前向条件：所有循环在 k 内展开 → 证明
  • I(k) 归纳步：在 k 步成立则下一步也成立 → 证明
  • 算法：for k=1,2,...: if B(k) bugs → FAILED; if F(k) holds → SUCCESSFUL; if I(k) holds → SUCCESSFUL; return UNKNOWN
  • 示例：一个断言需要 100 次展开才成立（x=0;y=50 副本循环），加一个归纳不变量后边界消失：0 <= x <= 100、x<=50 → y==50、x>50 → y==x
  • 结论：纯 k-induction 在无限循环上停滞，一个不变量就能闭合证明——不变量综合正是 LLM 的用武之地

契约：一次证明函数，处处复用

c
int my_abs(int x) {
    __ESBMC_requires(x > INT_MIN);
    __ESBMC_ensures(__ESBMC_return_value >= 0);
    __ESBMC_ensures(__ESBMC_return_value == x || __ESBMC_return_value == -x);
    return x < 0 ? -x : x;
}
  • 防改动：破坏契约的编辑在函数体或调用点立即失败
  • 可扩展：50 个调用点用契约 1.8s 验证，内联需要 9.4s
  • 💡 LLM 提议的契约 + ESBMC 检查：ConVer (arXiv:2605.27051)、Partial Contracts Suffice (arXiv:2607.10291)

反例即测试，证明即证书

esbmc --generate-ctest-testcase --unwind 6 生成可复现测试（test_case.c → ASan 报 stack-buffer-overflow）；修复 i < n 后 --k-induction 得 VERIFICATION SUCCESSFUL。

4. 三种「猜测」进入点（THREE PATTERNS）

Pattern A：工具协同 | Pattern B：LLM 提供证明要素 | Pattern C：LLM 提供规格 共同原则：猜测是廉价的，检查从不省略；在 C 上，检查还需要一个人。

A. FuSeBMC — 工具与工具协同（测试输入 / 种子）

  • 三引擎组合：BMC 可达性（精）、AFL 广覆盖（广）、选择性 fuzzer（路径敏感）
  • TRACER 协调器：共享内存记录已覆盖目标，新覆盖变下一轮种子
  • 成果：Test-Comp 2026 C.Overall / C.Cover-Error / C.Cover-Branches 三项第一；SV-COMP 2026 ESBMC-kind 在 C.ReachSafety 第 2（冠军 CPAchecker）
  • **Rust Foundation（2025-08）**批准 ESBMC 加入 Rust 标准库验证计划（与 Flux、Kani、VeriFast）

B. ibmc — LLM 提供不变量，Vampire 裁决可归纳性

  • 流程：C 程序 → 标记循环 → LLM 提不变量（带示例+CoT）→ 语法过滤 → Vampire 验证可归纳性 → ESBMC 用不变量替换循环检查
  • 反馈环：未证明 → 同提示语再问（更多不变量）；模型输出在 Vampire 证明其可归纳之前永不进入证明
  • 工程洞察：67–75% 的尝试无法解析（语法约束）；纯过滤会限制灵活性；提示中过多解释会分散注意力
  • 成果：133 个 code2inv 程序，ibmc 解出 101 个（union of 6 configs；单一配置约 58% ≈ 77 个），全部与基准 ground truth 一致，无一错误证明；对比 plain BMC 16、k-induction 46、（参考）SeaHorn 115
  • 不同引擎互补：ibmc∩k-induction 独占 37，SeaHorn 独占 10——组合优于单一冠军
  • 🏆 ACM SIGSOFT Distinguished Paper Award, ASE 2024
  • 📎 Pirzada, Reger, Bhayat & Cordeiro, "LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling", ASE 2024, pp.1395–1407, DOI 10.1145/3691620.3695512

C. SpecVerify — LLM 从自然语言需求生成属性

  • 双路径：需求文档 →（上）Simulink 模型 → Embedded Coder → 生成 C 代码；（下）LLM 形式化需求 → LLM 写 C 断言（结构化引导下）→ ESBMC 检查
  • 反馈环：反例回放到真实系统（fed back, not believed）
  • 成果（58 个 Lockheed Martin CPS 需求）：验证率 Claude+ESBMC 46.5%（= CoCoSim），SLDV 36.2% 但同样零误报；匹配专家手写属性 79.31%（46/58）；0 误报；发现 2 个此前未报告的浮点错误
  • ⚠️ 模型选择左右结果：GPT-4o 同一管线产生 8 个误报；Claude 3.5 Sonnet 路线仍漏 2 个违规

本幕教训：「The value should be reasonable.」没有语义。

  • 哪个界？assert(bottom < x && x < top) 的 bottom/top 从何来？range1/limit1/limit2… 需求指哪个 limit？
  • 模型会带着全副自信静默挑一个且不告诉你；检查器对「过严」会误报，对「过松」会静默放行——检查器看不见
  • 完全自动化在此止步：spec 必须有人类决定
  • 📎 Wang, Farrell, Cordeiro & Zhao, "Supporting Software Formal Verification with Large Language Models", IEEE RE 2025, pp.423–431, DOI 10.1109/RE63999.2025.00049

5. 生产代码实战（CODE THAT SHIPS）

新猜测 = harness： 基准有答案键，真实代码没有。LLM agent 写 harness 及其假设 → ESBMC 检查 +「注入 bug 的双胞胎」必须失败的对照 + 维护者合并修复。维护者成为新的答案键。

代码库 发现 上游已修复 成功证明
AWS SDK for C++ 12 7（含 2 个 CVE） 22 · 有界输入
NVIDIA OpenSMA 固件 11 1（已报告已修复） 22 · 无界
vLLM 8 5 21 · 有界输入
Google Chromium Dashboard 10 3 22 · 有界输入
AWS Neuron NKI samples 2 2 19 · 混合
  • 8 个代码库（harness 全部公开）、2 个 AWS SDK C++ CVE、18 个修复被上游合并

典型案例

  • AWS SDK C++ Base64 解码器 → 2 个 CVE：
    • CVE-2026-19642（堆写入）：AAAA= —— 长度计算把 = 计入而循环没有，2 字节缓冲写入 buffer[2]
    • CVE-2026-19643（signed char 读）：\xFF 变成 256 项表的巨大索引
    • 版本 1.11.862 一版修两 CVE，另 +2 DateTime 溢出 +3 cJSON 缺陷
    • 反例本身就是 bug report：可带 sanitizer 直接运行的具体输入
  • NVIDIA OpenSMA 固件：routing_table.ec.cur_eid.at(interface) = eid;——getter 有边界检查，setter 没有。iface=2 通过 validator，at() 越界检查在 -fno-exceptions 下直接 abort：拒绝服务而非内存破坏。NVIDIA 已确认并镜像修复（issue #1, 2026-05）
  • vLLM（服务模型的引擎本身就是普通软件）：
    • --block-size 0 → 引擎初始化 ZeroDivisionError ✅ 已修复
    • --hash-block-size -k → 初始化死循环 ✅ 已修复
    • --max-logprobs <负值> → 静默接受 ❗ ✅ 已修复
    • --num-gpu-blocks-override 0 → bare AssertionError ❗ 仍 open

6. 真实代码上的五条经验（论文演讲不会讲的）

  1. 零误报胜过更高的证明率——假警报会在开发者心中杀死工具的信任（Coverity / Google 前车之鉴）
  2. 维护者只修带具体输入的发现——18 个修复跨 5 个代码库
  3. 生成器的质量会传导——SpecVerify 换 GPT-4o 立即从 0 误报变 8 误报
  4. 我们并不赢下每场竞赛——SeaHorn 证明多于 ibmc，CoCoSim 追平 SpecVerify；组合优于单冠军
  5. 验证器本身也有陷阱——零 VCC、被禁用的扩张断言、静默什么都不检查的契约：证据本身需要被检查

7. 三个开放挑战（为什么需要一起解决）

挑战 产业带来 学术界带来
1 验证速度追上生成速度（agent 秒级生成，工业证明以分钟/小时计） agent traces 增量式证明复用（incremental proof reuse）
2 Agent 工作流的保证（验证单个 agent ≠ 验证它们组成的工作流） 真实工作流 组合式契约（compositional contracts）
3 可信的证据（DO-178C 已接受形式化证据 DO-333；谁来检查检查者？） 认证需求 witnesses / validators

8. 总结

LLMs are fast but unsound. Proof engines are sound but slow. Cooperation gives you both, if you design the interface on purpose.

—— LLM 快但不 sound；证明引擎 sound 但慢；只要你有意设计接口，二者协作兼备。

演讲者联系方式：Lucas Cordeiro — lucas.cordeiro@manchester.ac.uk · github.com/esbmc/esbmc

致谢（贡献者）：FuSeBMC — Alshmrany, Aldughaim, Bhayat；ibmc — Pirzada, Reger, Bhayat；SpecVerify — Wang, Farrell, Zhao；FormAI — Tihanyi, Bisztray, Ferrag, Jain；ESBMC — Wu, Sá Menezes 及全体贡献者。资助：EPSRC, UKRI, CNPq, CAPES, British Council, Intel, Amazon, Ethereum, Rust Foundation, Motorola, Flextronics, Nokia, Arm。

返回 Clippings