技术摘要：代理模型检测

问题陈述

验证由大型语言模型（LLM）生成的系统代码带来了独特的挑战，这些挑战加剧了形式化验证中已存在的困难。虽然 LLM 能够生成大量用于操作系统、编译器和驱动器的代码（使用 C 和 Rust 等语言），但生成的代码库往往缺乏显式的形式化规范。此外，LLM 生成代码中的安全契约通常隐式地编码在调用点，而非在函数边界处强制执行。

这种隐式编码导致了一种特定的故障模式：辅助函数（例如字节索引读取器、偏移算术写入器）通常缺乏边界和溢出保护，而是依赖周围的调用者逻辑来维持不变量。因此，代码在处理格式良好的输入时功能正常，但在面对对抗性或精心构造的输入时则会失效。传统的验证工具在此类场景下难以应对，因为它们要么过度报告（在没有上下文的情况下将辅助函数标记为损坏），要么报告不足（因为当前的调用者未触发这些错误而遗漏漏洞）。此外，现有的基于 LLM 的验证方法通常在算术和内存安全方面缺乏完备性，而传统的演绎检查器则难以应对系统代码的规模和循环密集的特性，且缺乏生成具体反例的能力。

方法论：代理模型检测

作者提出了代理模型检测（Agentic Model Checking），这是一种将 LLM 代理与有界模型检测（BMC）后端相结合的验证范式，其核心原则是：“代理提出，求解器验证。”

该系统实例化为BMC-Agent，通过一个流水线运行，其中 LLM 代理处理需要语义判断的任务，而确定性的 BMC 后端（C 语言使用 CBMC，Rust 使用 Kani）负责处理所有与完备性相关的决策。

核心架构承诺

1. 自顶向下的规范推断：

   • 代理根据调用者上下文，自顶向下地推断每个函数的前置条件和后置条件。
   • 规范以受限的领域特定语言（DSL）生成，该语言可确定性翻译为后端原生的 assume/assert 原语。
   • 除了防御性的无崩溃检查外，系统还会生成功能正确性规范（例如参考等价表达式、代数恒等式），从而将验证从单纯的避免崩溃提升到行为忠实度层面。

2. 组合式验证：

   • 验证按函数分解。每个函数在其推断的规范下独立进行检查。
   • 被调用的函数（被调用者）被其后置条件约束的存根（stubs）所替代。这实施了一种**假设 - 保证（assume-guarantee）**纪律，即被调用者的后置条件成为调用者的假设。
   • 这种方法防止了全程序状态爆炸，使验证能够随着单个函数状态空间的大小进行扩展，而非整个程序。

3. 多阶段反例验证：

   • BMC 反例不被视为即时的漏洞报告。它们需经过严格的验证流水线，以区分活跃的代码库崩溃与潜在故障或建模伪影：
     • 输入可达性： 将见证输入沿调用图向上传播，以确定调用者是否能提供这些值。
     • 被调用者可行性： 使用真实的被调用者函数体重新运行 BMC，以确保见证可通过真实实现到达。
     • 动态重放： 编译一个桩程序（harness）以在主机系统上执行见证，捕获信号（SIGSEGV、SIGABRT 等）以确认动态崩溃。
     • 真实性审计： LLM 代理审查完整上下文（规范、桩程序、见证状态），将发现分类为真实或不真实，过滤掉框架不变量伪影（例如未初始化的全局变量、不可能的硬件状态）。

4. 自适应精炼循环（规范层面的 CEGAR）：

   • 当反例被分类为虚假（例如循环展开伪影）时，系统不会简单地抑制它。相反，LLM 会提出精炼方案（收紧前置条件、加强被调用者契约或调整求解器参数）。
   • 一个完备性守卫确保这些精炼不会掩盖真实漏洞。
   • 接受的精炼方案被持久化存储在知识库（规范存储和模式库）中，并传播到所有调用者，从而有效地将 CEGAR 从谓词抽象扩展到规范层面，并具备组合传播能力。

主要贡献

本文概述了六项主要贡献：

1. 代理模型检测范式： 一个框架，其中 LLM 代理管理语义任务（规范推断、检查选择、分类），而 BMC 后端确保完备性，从而实现了对 LLM 生成的 C 和 Rust 代码的无规范验证。
2. 自顶向下规范层： 一种机制，用于推断每个函数的前/后置条件，并通过翻译为 CBMC/Kani 的 DSL 选择语义上合理的算术检查（例如溢出、指针检查）。
3. 组合式验证架构： 一种可扩展的方法，在假设 - 保证契约下独立检查函数，并在调用图层级间并行化。
4. 验证流水线： 一个四阶段过程（可达性、可行性、动态重放、真实性审计），将发现分类为不同的证据层级（例如“确认的动态”、“确认的系统入口”）。
5. 多级精炼循环： 一个将 CEGAR 提升至规范层面的系统，利用虚假反例驱动组合式精炼，并使这些精炼在多次运行中持久存在。
6. BMC-Agent 实现与评估： 一个在多样化语料库上评估的可用工具，展示了其确认真实缺陷、在模糊测试的库上产生有界清洁验证以及证明功能等价性的能力。

评估结果

作者在涵盖 C 和 Rust 的四个语料库上评估了 BMC-Agent：

• VibeOS (C)： 一个 15,000 行由 LLM 生成的 ARM64 内核。BMC-Agent 在 12 个模块中确认了34 个真实漏洞。其中，16 个被动态复现（SIGSEGV/SIGABRT），14 个被确认为系统入口点，4 个为形式化模型违规。
• 成熟开源库 (C)： 在 jq、OpenSSL、libcurl、libxml2 和 protobuf upb 上进行了评估。该工具披露了 jq 中的2 个未定义行为缺陷（已作为 GHSA 提交），并在经过重度模糊测试的解析器表面上产生了有界清洁验证（例如 OpenSSL ASN.1 中 24 个叶函数中的 15 个验证清洁）。
• Realtek r8125 驱动程序 (C)： 在 rtl8125 工具 ioctl 中发现了一个受 CAP_NET_ADMIN 限制的 MMIO 边界检查绕过漏洞，该漏洞通过标志选择器启用特定的溢出检查后被触发。
• claudes-c-compiler (Rust)： 一个 50,000 行由 LLM 生成的 C 编译器。BMC-Agent 确认了25 个真实漏洞，主要是公共 API 字节辅助函数上的 panic 类缺陷（切片越界、整数溢出）以及一个功能正确性违规。它还建立了 ELF 哈希和头部写入辅助函数的有界功能等价性。

结果中的关键观察：

• 该工具的精度归功于真实性阶段检测器（过滤框架伪影）、每函数标志选择（在标准配置中默认关闭检查）以及反馈循环（将重复模式转换为永久不变量）。
• 在 Rust 编译器案例中，漏洞遵循一种特定的反模式：LLM 编写了没有边界检查的辅助函数，依赖调用者来维持不变量。这导致了代码在处理格式良好的输入时正常工作，但在面对对抗性输入时失效，这种特征与典型的人工编写编译器逻辑错误截然不同。

意义与主张

本文主张，代理模型检测通过自动化契约推断并将其与完备的有界模型检测相结合，解决了 LLM 生成系统代码中的“规范差距”。

• 完备性与可扩展性： 通过将完备性委托给 BMC 并使用代理进行语义判断，该方法避免了纯 LLM 推理的不完备性，同时克服了全程序验证的可扩展性限制。
• 可操作的验证： 多阶段验证流水线确保报告的漏洞不仅仅是理论上的反例，而是根据其可达性和动态影响进行分类，区分活跃崩溃与潜在的加固任务。
• 组合传播： 系统精炼规范并将其跨调用图传播的能力，使其能够从虚假反例中学习，从而在不人工干预的情况下随时间提高验证质量。

作者对未来工作保持谦逊，指出广泛的定量评估（大规模下的精确率/召回率）、对规范正确性假设的更深入分析以及通过令牌优化降低成本是必要的下一步。他们强调，当前的结果证明了该流水线确认缺陷和验证清洁表面的能力，但并未声称已解决了无限制地验证所有 LLM 生成代码的通用问题。