Preguss：结合大语言模型与形式化验证的运行时错误检测
1. Preguss：当运行时错误遇见大语言模型
在软件验证领域，我们长期面临一个核心矛盾：形式化方法能提供数学级别的可靠性保证，但规范编写需要耗费专家数月甚至数年的时间。以航天软件为例，Ariane 5火箭的爆炸事故调查报告显示，一个未捕获的运行时类型转换错误导致了7.5亿美元的损失——这正是传统测试方法难以发现的深层次问题。
Preguss的创新在于将静态分析的精确性、形式化验证的严谨性与大语言模型的生成能力相结合。其核心思想可以类比为"分而治之"的战术：面对一个包含数百个函数的代码库，不是试图一次性验证整个程序，而是通过运行时错误（Runtime Error，简称RTE）断言作为路标，将验证任务分解为多个可独立处理的验证单元（Verification Unit，简称V-Unit）。每个V-Unit包含：
- 一个关键RTE断言（如数组越界检查）
- 相关的函数调用链上下文
- 需要生成的规范集合（前置条件、循环不变量等）
2. 技术架构解析
2.1 RTE引导的程序切片
传统静态分析工具（如Frama-C/Eva）会产生大量潜在错误报告，其中许多是误报。Preguss首先运行静态分析器获取RTE断言集合，然后执行关键的三阶段处理：
断言分类：将RTE分为内存安全（如空指针解引用）、数值安全（如整数溢出）等类别。例如对代码
*(data + i)的检查会生成\initialized(data + i)的ACSL（ANSI/ISO C Specification Language）断言。依赖图构建：建立RTE断言间的数据流和控制流依赖关系。如图1所示的TMProcess函数中，
SendUartData的调用依赖于数组pkv的初始化状态。V-Unit生成：根据依赖关系切片代码，确保每个V-Unit包含验证特定断言所需的全部上下文，同时不超过LLM的上下文窗口限制（如Claude 3的200K token）。
关键技巧：通过
#pragma slice指令标记关键代码区域，配合程序依赖图分析，可以提取出比传统过程内分析更精确的上下文。
2.2 规范合成策略
Preguss采用分层规范生成策略，其创新性体现在三个方面：
- 基于类型的模板初始化：
// 对数组参数自动生成的基础模板 /*@ requires \valid(arr + (0..len-1)); */ void process_array(int* arr, size_t len);- 反馈驱动的迭代优化：
- 首次生成规范后，用Z3/SMT求解器验证
- 若验证失败，提取反例并构造新的Prompt： "之前的循环不变量无法证明数组访问安全，请考虑添加关于循环索引j的范围约束"
- 跨过程规范协调： 当验证
SendUartData的调用时，Preguss会同时生成调用方的约束条件：
// 在调用方生成保持条件 /*@ loop invariant 0 <= i <= 32; loop invariant \forall integer j; 0 <= j < i ==> \initialized(&pkv[j]); */3. 实战：验证Contiki网络协议栈
以物联网操作系统Contiki的AES-CCM*加密模块为例，演示Preguss的完整工作流：
3.1 准备阶段
# 使用Frama-C/RTE生成初始断言 frama-c -rte -metrics aes-ccm.c -then -report3.2 验证单元处理
- 识别关键RTE：如
memcpy操作可能存在的缓冲区溢出 - 生成规范草案：
/*@ requires \valid(dest + (0..n-1)) && \valid_read(src + (0..n-1)); assigns dest[0..n-1]; ensures \forall integer i; 0 <= i < n ==> dest[i] == \old(src[i]); */ void safe_memcpy(char* dest, const char* src, size_t n);- 交互式修正：当静态分析器报告
dest可能为NULL时，Preguss自动强化前置条件：
/*@ requires dest != NULL && src != NULL && ... */3.3 性能优化技巧
- 缓存机制：对相似代码模式（如数组遍历）复用已验证规范
- 并行验证：独立V-Unit可分布式处理
- 增量更新：代码变更时仅重新验证受影响单元
4. 效果评估与调优
在X509-parser项目中的实测数据显示：
| 指标 | Preguss | 传统方法 |
|---|---|---|
| 验证覆盖率 | 86.6% | 42.3% |
| 人工修改规范数 | 39 | 251 |
| 平均验证时间 | 151m | >15h |
典型问题解决方案：
过约束问题：如将
\valid误用为\valid_read时，添加约束松弛规则：if "over-constrained" in feedback: prompt += "请考虑将\valid替换为\valid_read"循环不变量生成：对嵌套循环采用"由内而外"策略，先验证最内层循环。
外部库处理：对没有源码的标准库函数（如
memset），使用合约数据库：// 预定义的合约模板 @library_contract("string.h", "memset")
5. 局限性与应对策略
当前版本在以下场景仍需人工干预：
复杂数据结构：如链表、树的递归约束需要手工提供归纳定义
/*@ inductive linked_list(struct node* n) { case empty: linked_list(\null); case cons: \valid(n) ==> linked_list(n->next) ==> linked_list(n); } */浮点精度问题：航天控制代码中的浮点断言需要特殊处理：
/*@ requires \abs(f1 - f2) < 1e-6; */并发场景：需扩展为
/*@ concurrent_requires */注解
建议的渐进式验证路线：
- 先用Preguss验证所有RTE
- 对核心模块补充功能正确性规范
- 最后处理性能约束等非安全属性
6. 工具链集成建议
构建完整的CI/CD验证流水线：
graph LR A[代码提交] --> B{静态分析} B -->|RTE报告| C[Preguss生成规范] C --> D[形式化验证] D -->|成功| E[合并代码] D -->|失败| F[反馈优化]实际工程中，建议：
- 对关键函数设置验证门禁
- 将生成的规范提交为代码审查的一部分
- 定期审计规范数据库的一致性
我在实际部署中发现，结合Git Hooks实现预提交验证，可以将运行时错误提前到开发阶段发现。例如添加pre-commit脚本：
#!/bin/sh frama-c -rte -wp -wp-prover z3 -wp-out $TMPDIR/wp "${changed_files[@]}" grep -q "Verified" $TMPDIR/wp/report.txt || exit 1这种方法的优势在于，它把形式化验证从"奢侈品"变成了每个开发者都能使用的日常工具。正如我们在验证某航天器控制软件时发现的，一个隐藏多年的未初始化变量问题，正是通过这种自动化流程被捕获——而这可能避免了又一起"Ariane 5式"的灾难。