来源笔记
Agentic Model Checking
摘要
BMC-Agent 通过让 LLM 智能体编写并修订规格，而由 CBMC 或 Kani 进行检查，来验证 LLM 生成的系统代码。它面向需要穷尽式有界搜索和具体反例的底层 C 和 Rust 缺陷。
问题
- LLM 生成的系统代码通常缺少形式化规格，并且把安全假设藏在调用点，因此公共 API 在对抗性输入下可能崩溃。
- 只靠 LLM 审查可以标出有风险的模式，但它不能证明在整个输入范围内没有整数、指针、边界或 panic 缺陷。
- 直接做有界模型检查需要规格，而且会产生可能不可达或只是模型产物的反例，所以发现结果需要经过可达性和重放检查。
方法
- LLM 智能体根据调用方上下文和源代码，推断每个函数的前置条件、后置条件，以及可选的功能正确性检查。
- 这些推断出的规格使用受限 DSL，可直接映射到 C 的
__CPROVER_assume和__CPROVER_assert，或 Rust 的kani::assume和kani::assert。 - 每个函数单独用 CBMC 或 Kani 检查；被调用函数会替换成受其后置条件约束的存根。
- 在报告缺陷前，验证流水线会通过输入可达性、被调用方可行性、动态重放和真实性审计来检查反例。
- 不现实的见证会触发规格或模型修订，修订会先经过健全性保护，再重新运行检查器。
结果
- 在 VibeOS 上，这篇论文声称发现了 34 个真实缺陷，分布在 12 个模块中；VibeOS 是一个 15,000 行代码的 LLM 生成 ARM64 C 内核，其中 16 个缺陷被复现为运行时故障。
- 在五个成熟、经过 OSS-Fuzz 强化的目标
jq、OpenSSL、libcurl、libxml2 和 protobuf upb 上，它报告了jq中 2 个未定义行为缺陷，并且在经过大量 fuzz 的解析器表面上给出了有界的干净验证结果。 - 在树外的 Realtek r8125 Linux 驱动上，它报告了
rtl8125_tool_ioctl中 1 个受CAP_NET_ADMIN约束的 MMIO 边界检查绕过。 - 在
claudes-c-compiler上，这是一个 50,000 行的 LLM 生成 Rust C 编译器，它声称发现了 25 个真实缺陷：24 个是公共 API 字节辅助函数中的 panic 类缺陷，另 1 个是由行为规格发现的功能正确性违例。 - 它还声称对选定的 ELF 哈希和头部写入辅助函数证明了有界功能等价。
- 默认 BMC 设置包括展开上限 k=4 和每个函数 120 秒超时；Kani 会在需要时重试，把展开上限从 4 提高到 16，或把切片边界从 4 缩小到 2 再到 1。