A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

本文提出了名为 Preguss 的模块化细粒度框架，通过结合静态分析与大语言模型，利用潜在运行时错误引导验证单元构建与优先级排序，成功实现了对千行代码级大规模程序的高度自动化形式化验证，显著降低了人工验证成本。

要点

这篇论文讲述了一个关于如何让电脑自动检查大型软件代码是否安全的“新故事”。为了让你轻松理解，我们可以把编写和检查大型软件想象成管理一家拥有上千名员工的大型跨国公司。

🏢 背景：巨大的挑战

想象一下，你是一家大公司的安全总监。公司有一本厚厚的操作手册（代码），里面有几万行指令。你的任务是确保没有任何员工会犯下致命的错误（比如除以零、内存溢出、空指针引用等，这些在编程里叫“运行时错误”或 RTE）。

• 传统方法（老式安检机）： 以前，我们使用一种叫“静态分析”的机器来扫描手册。但这台机器太敏感了，它经常把正常的操作也当成危险报警（这叫“误报”）。人工去一个个排查这些误报，就像在沙滩上找针，累死人也找不完。
• 新方法（AI 助手）： 最近，大家尝试用大语言模型（LLM，也就是现在的 AI）来帮忙写“安全承诺书”（形式化规范）。AI 很聪明，能读懂代码。但是，如果直接把整本几万页的手册扔给 AI，它会“脑子过载”（上下文限制），或者因为代码太复杂、函数之间调用关系太乱，根本写不出准确的承诺书。

🚀 主角登场：Preguss（“分而治之”的超级管家）

这篇论文提出了一个名为 Preguss 的新框架。它的核心思想可以用一个生动的比喻来解释：“分而治之” + “精准导航”。

1. 第一步：把大任务切碎（Divide）

想象你要检查整个公司的安全，直接看全公司太乱了。Preguss 先派出一位“侦察兵”（静态分析工具），它不直接找最终答案，而是专门负责标记出所有可能出错的“危险点”（比如：这里可能会除以零，那里可能会内存溢出）。

然后，Preguss 把这些危险点变成一个个独立的“小任务包”（Verification Units）。

• 比喻： 就像把检查整个大楼的任务，拆分成“检查 1 楼的电梯”、“检查 2 楼的消防栓”、“检查 3 楼的电路”等一个个小任务。
• 排序： 它还会给这些小任务排个队。比如，必须先检查“底层供应商”（被调用的函数），才能检查“顶层经理”（主函数）。这就像盖房子，得先打好地基，才能砌墙。

2. 第二步：AI 精准填坑（Conquer）

现在，AI 不需要再看整本几万页的手册了。它只需要看着当前这个小任务包，以及侦察兵标记的危险点，来写一份“安全承诺书”。

• 精准导航： 如果侦察兵说“这里可能会除以零”，AI 就会专门针对这个点，去问：“是谁传进来的数据？是不是需要加个限制，比如‘输入不能是 0'？”
• 跨部门协作（过程间规范）： 很多错误是因为 A 部门（函数）把坏数据传给了 B 部门。Preguss 会指挥 AI 去写 A 部门的“输出承诺”（后条件）和 B 部门的“输入要求”（前条件），确保数据在传递过程中是安全的。
• 纠错机制： 如果 AI 写的承诺书太离谱（比如要求输入必须是“红色的数字”，这显然不对），Preguss 会拿着验证器的反馈（“你写错了，因为变量没定义”）让 AI 修改，直到它写出一个既符合逻辑又能通过验证的承诺书。

🌟 为什么它这么厉害？（核心创新）

1. 不再“盲人摸象”： 以前的 AI 方法像是在黑暗中摸索，试图一次性猜出所有规则。Preguss 则是拿着手电筒（危险警报），哪里亮了查哪里，哪里有问题补哪里。
2. 化整为零： 它把几千行代码的大工程，拆解成几百个几百行的小工程。这让 AI 的“大脑”（上下文窗口）能轻松处理，不会过载。
3. 人机协作的极致： 以前，人类专家需要写几百条规则来证明代码安全。现在，Preguss 自动生成了大部分规则，人类专家只需要检查最后剩下的极少数“存疑项”。
   • 成果： 在测试中，它把人类的工作量减少了 80% 到 89%！

🛠️ 实际效果：真的有用吗？

作者们把这个系统用在了真实的航天器控制系统（SAMCODE）和其他大型开源项目上。

• 发现真凶： 它不仅自动验证了大部分代码是安全的，还成功揪出了 6 个真实的、潜伏的严重 Bug（比如未初始化的变量），这些 Bug 如果爆发，可能导致航天器失控。
• 效率惊人： 对于几千行代码的项目，以前可能需要专家花几个月手动写规则，现在 Preguss 能在几小时内搞定大部分工作。

📝 总结

Preguss 就像是一个拥有“透视眼”和“超级逻辑”的 AI 管家。
它不再试图一口吃成个胖子，而是把庞大的代码库拆解成一个个小任务。它利用“危险警报”作为导航，指挥 AI 精准地写出安全规则，并不断自我修正。最终，它让原本需要人类专家耗时数月、甚至数年才能完成的“代码安全大考”，变成了大部分自动完成、人类只需最后把关的高效流程。

这不仅是技术的进步，更是让大型软件（如航天、金融、医疗系统）变得更安全、更可靠的“圣杯”之路上的重要一步。

技术摘要

这是一篇关于利用大语言模型（LLM）辅助进行大规模程序形式化验证的学术论文总结。论文提出了一种名为 Preguss 的框架，旨在解决自动化生成形式化规范以验证大型 C/C++ 程序运行时错误（RTE）自由性的难题。

以下是该论文的详细技术总结：

1. 研究背景与问题定义 (Problem)

• 核心挑战：

  • 运行时错误（RTE）的重要性：如除零、缓冲区溢出、空指针解引用等未定义行为（UB）在安全关键系统中是致命的。传统的静态分析工具（如基于抽象解释的 Frama-C/Eva）虽然能检测 RTE，但会产生大量误报（False Positives）。
  • 规范合成（Specification Synthesis）的瓶颈：为了消除误报并验证 RTE 自由性，需要生成精确的形式化规范（如前置条件、后置条件、循环不变式）。这一过程传统上高度依赖人工，难以扩展。
  • LLM 的局限性：虽然 LLM 在代码理解上表现出色，但在处理大规模程序（>1000 行代码）时面临两大挑战：
    1. 长上下文限制：无法一次性处理整个程序，且难以在长上下文中精准定位所需信息。
    2. 过程间规范（Interprocedural Specifications）的复杂性：现有的 LLM 方法往往难以生成复杂的跨函数规范（如正确区分前置/后置条件），或者生成的规范过于约束（Over-constrained），导致新的误报。

• 研究目标：
  实现大规模程序 RTE 自由性的高度自动化验证，显著减少人工干预，同时能够识别真实的 RTE。

2. 方法论：Preguss 框架 (Methodology)

Preguss 采用 “分而治之” (Divide-and-Conquer) 策略，将静态分析与演绎验证（Deductive Verification）相结合，分为两个协同阶段：

第一阶段：基于潜在 RTE 的验证单元构建与优先级排序 (Divide)

• 输入：源代码 + 静态分析器（如 Frama-C/Rte）生成的 RTE 断言（Guard Assertions）。
• 核心机制：
  • 验证单元 (V-Unit)：将庞大的验证任务分解为独立的验证单元。每个 V-Unit 包含一个目标断言（Guard Assertion）及其最小化的程序切片（宿主函数及其被调用函数）。
  • 优先级队列：根据调用图（Call Graph）自底向上（Bottom-up）的原则对 V-Unit 进行排序。先验证被调用函数（Callee），再验证调用者（Caller），确保在验证上层函数时，下层函数的规范（契约）已经就绪。
  • 潜在 RTE 引导：利用静态分析器指出的潜在错误点作为验证目标，指导 LLM 生成针对性的规范，而非盲目生成。

第二阶段：细粒度的过程间规范合成 (Conquer)

• 输入：排序后的 V-Unit 队列。
• 核心机制：
  • 迭代合成：针对每个 V-Unit，LLM 根据验证器的反馈（Proof Obligations）迭代生成规范。
  • 细粒度策略：
    • 宿主函数 (Host Function)：仅针对当前函数生成前置条件和循环不变式，避免引入不必要的上下文导致过度约束。
    • 被调用函数 (Callee Functions)：仅针对被调用函数生成后置条件，利用其返回值约束来消除宿主函数中的误报。
  • 反馈驱动的精炼 (Feedback-Driven Refinement)：利用演绎验证器（Frama-C/Wp）返回的“未知”状态和证明义务（Proof Obligations），指导 LLM 修正语法错误或语义不满足的规范。
  • 语法与语义检查：自动过滤掉语法错误或导致逻辑矛盾的规范（如过度约束的前置条件）。

理论基础

• 声性 (Soundness)：如果所有生成的假设（Hypotheses）被验证为真，且静态分析器是声的，则程序无 RTE。
• 终止性 (Termination)：通过限制迭代次数和 V-Unit 的静态构建，保证算法必然终止。

3. 主要贡献 (Key Contributions)

1. 概念创新：提出了“潜在运行时错误引导的规范合成”（Potential RTE-guided Specification Synthesis）概念，利用静态分析断言作为 LLM 生成的目标，有效解决了大规模程序验证的扩展性问题。
2. 框架实现 (Preguss)：
   • 首个能够自动证明超过 1000 行代码真实世界程序 RTE 自由性的自动化方法。
   • 实现了模块化、细粒度的规范生成，有效解决了 LLM 在处理复杂调用链时的上下文和幻觉问题。
3. 数据集构建：构建了一个开源数据集，包含由 Preguss 生成并经专家验证的真实 C 程序规范，用于 RTE 自由性验证。
4. 实证结果：在基准测试和真实项目（包括航天器控制系统）上展示了显著优于现有 SOTA 方法（如 AutoSpec）的性能。

4. 实验结果 (Results)

• 基准测试 (Frama-C-Problems)：
  • Preguss 在 51 个程序中成功验证了 46 个 (79.7%)，而现有的 SOTA 方法 AutoSpec 仅为 32.7%。
  • 在数组和循环等复杂场景下，Preguss 的优势尤为明显。
• 大规模真实项目：
  • Contiki (544 LoC)、X509-parser (1199 LoC)、SAMCODE (1280 LoC)、Atomthreads (1451 LoC)。
  • 自动化程度：Preguss 实现了 80.6% ~ 88.9% 的人工验证工作量减少（即仅需人工处理少量未验证的假设）。
  • 真实错误发现：在 SAMCODE 航天器控制系统中，Preguss 成功识别并协助确认了 6 个真实的 RTE（未初始化变量访问），这些错误源于逻辑缺陷，此前未被发现。
• 消融实验：证明了“反馈驱动精炼 (FDR)"和“语法修正 (SC)"模块对提升验证成功率至关重要。

5. 意义与影响 (Significance)

• 推动形式化方法落地：将形式化验证从“专家手工”推向“高度自动化”，使得验证数千行代码的工业级软件成为可能。
• 人机协作新模式：通过 LLM 生成大部分规范，将人类专家从繁琐的规范编写中解放出来，专注于处理剩余的少数关键假设和真实错误。
• 解决 LLM 幻觉与上下文限制：通过“分而治之”和“断言引导”策略，有效规避了 LLM 在处理长代码时的上下文窗口限制和生成过度约束规范的问题。
• 安全关键系统保障：在航天控制等安全关键领域，能够自动发现深层逻辑错误，显著提升了软件可靠性。

总结

Preguss 通过巧妙结合静态分析的精确性（提供验证目标）和 LLM 的推理能力（生成规范），并引入细粒度的分治策略，成功突破了大规模程序形式化验证的瓶颈。它不仅大幅降低了验证成本，还具备发现真实软件缺陷的能力，为自动化软件验证领域树立了新的标杆。