BODHI: 精确的操作系统内核规范推断

# BODHI：精确的操作系统内核规格推断 来源：https://arxiv.org/html/2605.23931 ###### 摘要 操作系统内核的形式化验证需要精确的规格说明来捕获系统调用的预期行为。手动编写这些规格说明需要深厚的领域专业知识，这促使人们使用大型语言模型（LLM）来自动化这一过程。然而，在 OSV-Bench（一个包含 245 个规格生成任务的基准，源自 Hyperkernel 操作系统内核）中，最佳报告的 Pass@1 仅为 55.10%[12 (https://arxiv.org/html/2605.23931#bib.bib1)]。我们提出了一种领域知识提示方法（BODHI），该方法在标准的小样本提示基础上，增加了一份结构化的 C 到 Python 翻译指南，涵盖 15 个类别的领域特定翻译模式。受结构化思维链（SCoT）提示[11 (https://arxiv.org/html/2605.23931#bib.bib2)]的启发，该指南通过关注点分离来组织翻译，将前置条件提取和后置条件生成作为不同的类别。在来自六家供应商（Anthropic、Mistral、Amazon、DeepSeek、Meta、Alibaba）的九个模型上进行了评估，涵盖了密集、混合专家和推理架构，BODHI 提升了所有测试模型的表现，提升幅度从 +11% 到 +32% 不等。最佳配置（Claude Opus 4.6 + BODHI）达到了 96.73% 的 Pass@1。BODHI 减少了语法和语义错误，对具有足够指令遵循能力以利用结构化参考材料的模型效果最为显著。这些结果表明，领域知识注入是一种与模型无关的技术，极大地缩小了通用代码生成与形式化规格合成之间的差距。

## I 引言

形式化软件验证利用严谨的数学推理来证明系统没有错误，这对于安全关键系统（如操作系统内核）至关重要，因为软件错误可能导致灾难性后果[5 (https://arxiv.org/html/2605.23931#bib.bib3)]。然而，构建形式化规格说明（验证的前提）仍然是瓶颈，需要深厚的领域专业知识。例如，为支持高效 RPC 而更新 seL4 微内核时，修改的代码不到 5%，但由此产生的规格和证明调整花费了大约一人年的工作量[8 (https://arxiv.org/html/2605.23931#bib.bib4)]。大型语言模型在代码生成方面表现出了强大的能力[1 (https://arxiv.org/html/2605.23931#bib.bib5),7 (https://arxiv.org/html/2605.23931#bib.bib6)]，但它们在生成形式化规格说明方面的性能仍然有限。OSV-Bench[12 (https://arxiv.org/html/2605.23931#bib.bib1)]是目前最大的 OS 内核规格生成基准，在源自 Hyperkernel 操作系统[19 (https://arxiv.org/html/2605.23931#bib.bib7)]的 245 个任务上评估了 12 个大型语言模型。每个任务需要将 C 语言系统调用实现转换为 Python/Z3 状态机规格说明。表现最佳的模型仅达到了 55.10% 的 Pass@1，暴露了自然语言代码生成与形式化规格合成之间的显著差距。这一差距源于规格生成过程中固有的一些挑战：

- • 长上下文复杂度：每个任务提示包含约 26K 个 token，包括一个编程模型、少量示例、目标系统调用的功能描述和代码。
- • 语义鸿沟：C 内核代码必须转换为声明式的 Z3[18 (https://arxiv.org/html/2605.23931#bib.bib8)] Python 规格说明，这两种编程风格本质上是不同的。
- • 关注点交织：在 C 代码中，前置条件（错误检查逻辑）和后置条件（状态变更逻辑）在结构上混合在一起，但在规格说明中必须清晰区分。
- • 领域特定知识：诸如页表项（PTE）公式、引用计数语义、TLB 刷新操作和 IPC 状态机等内核 API 模式高度专业化，通用 LLM 训练并未涵盖这些内容。

我们采用了一种简单而有效的方法来应对这些挑战：基于一组标准提示和少量示例，提供一份全面的结构化 C 到 Python 翻译指南。我们将这种方法称为 BODHI。该指南是一份 519 行的参考文档，分为 15 个类别，为 Hyperkernel 领域中遇到的每种主要构造提供了清晰的翻译模式。借鉴结构化思维链（SCoT）提示[11 (https://arxiv.org/html/2605.23931#bib.bib2)]的原则，它将翻译任务组织成不同的关注点类别（前置条件提取、后置条件模式、字段访问语法和领域特定公式），而不是要求模型仅从少数示例中推断所有模式。

在本文中，我们做出了以下贡献：

- • 一份针对 OSV-Bench 规格生成的领域特定翻译指南，涵盖 15 个类别的 C 到 Python/Z3 翻译模式，这些模式源自对已验证的真实规格说明的分析。
- • 在来自六家供应商的九个模型上，对 BODHI 进行了全面评估，每个任务使用独立的 API 调用，证明了其在不同架构上的模型无关有效性。
- • 详细分析显示，BODHI 减少了语法和语义错误，对具有足够指令遵循能力但领域知识不完整的中间层模型提升效果最大。
- • 在 OSV-Bench 上取得了 96.73% Pass@1 的新最佳结果，大幅超越了之前 55.10% 的最佳结果。

## II 背景

### II-A OSV-Bench

OSV-Bench[12 (https://arxiv.org/html/2605.23931#bib.bib1)]是一个用于评估 LLM 在 OS 内核验证中生成规格说明的基准。它基于 Hyperkernel[19 (https://arxiv.org/html/2605.23931#bib.bib7)]构建，Hyperkernel 是一个使用 Z3 SMT 求解器[18 (https://arxiv.org/html/2605.23931#bib.bib8)]进行验证的形式化验证操作系统内核。245 个任务中的每一个都需要为系统调用生成一个 Python/Z3 状态机规格说明。该规格说明了前置条件和后置条件。任务提示包括：(1) 系统验证假设文档，(2) 定义可用类、常量和函数的编程模型，(3) 系统调用规格的小样本示例，以及 (4) 目标系统调用的功能描述和（可能包含错误的）C 语言实现。这 245 个任务涵盖了 49 个系统调用，并注入了不同类型的错误。每个任务的 C 语言实现可能包含五种错误类型中的一种或多种：错误的指针操作、错误的权限检查、内存泄漏、缓冲区溢出和缺少边界检查。此外，有 49 个任务包含正确的实现。当且仅当 Z3 验证器在所有内核实现变体上产生与 oracle 规格说明一致的结果时，规格说明才是正确的。规格说明在包含 Hyperkernel 构建系统和 Z3 求解器的 Docker 环境中进行验证[12 (https://arxiv.org/html/2605.23931#bib.bib1)]，遵循第 II-B 节 (https://arxiv.org/html/2605.23931#S2.SS2) 中描述的验证流程。主要指标是 Pass@1：LLM 生成的规格说明在首次尝试时通过验证的任务比例。已发布的 OSV-Bench 评估涵盖了 12 个 LLM，最佳 Pass@1 达到了 55.10%（Doubao-1.5-pro）[12 (https://arxiv.org/html/2605.23931#bib.bib1)]。值得注意的是，增强推理的模型（o1、DeepSeek-R1）并未超越标准的指令遵循模型，这表明规格生成需要领域特定知识，而非通用推理能力。

### II-B Z3 与验证流程

OSV-Bench 中的规格说明使用 Z3[18 (https://arxiv.org/html/2605.23931#bib.bib8)] 的 Python API 编写，Z3 是一个可满足性模理论（SMT）求解器。SMT 求解器确定逻辑公式在固定宽度位向量和数组等理论上的可满足性，这些理论直接模拟了操作系统内核中的硬件寄存器、内存页和内核数据结构。每个规格说明都是一个 Python 函数，它将一个系统调用的预期行为编码为状态机转换。形式上，对于系统调用 \(s\)，其规格说明是一个函数：
\[ f_s(\mathbf{S}, \mathbf{a}) \rightarrow (\phi, \mathbf{S}') \qquad (1) \]
其中 \(\mathbf{S}\) 表示当前内核状态（一组映射和标量字段的集合），\(\mathbf{a}\) 表示系统调用参数，\(\phi\) 是前置条件（一个 Z3 布尔表达式，表示所有有效性检查的合取），\(\mathbf{S}'\) 是后状态。当 \(\phi\) 成立时，后状态满足 \(\mathbf{S}' = \texttt{update}(\mathbf{S})\)，否则 \(\mathbf{S}' = \mathbf{S}\)。图 1 (https://arxiv.org/html/2605.23931#S2.F1) 展示了 Hyperkernel 使用的验证流程。C 语言实现被编译为 LLVM 中间表示（IR）[9 (https://arxiv.org/html/2605.23931#bib.bib9)]，工具链对 IR 执行符号执行，提取一个逻辑公式，该公式捕获了实现对所有可能输入的行为。将实现提取的行为表示为 \(g_s(\mathbf{S}, \mathbf{a})\)，Z3 检查行为等价性：
\[ \text{verify}(s) \iff \forall \mathbf{a}: g_s(\mathbf{S}, \mathbf{a}) \equiv f_s(\mathbf{S}, \mathbf{a}) \qquad (2) \]
如果存在不一致，Z3 会产生一个反例：具体的 \(\mathbf{a}^*\) 使得 \(g_s(\mathbf{S}, \mathbf{a}^*) \not\equiv f_s(\mathbf{S}, \mathbf{a}^*)\)。如果没有这样的 \(\mathbf{a}^*\) 存在，则该系统调用被验证为正确。

C 语言实现 → LLVM IR → 实现行为
编译 → 符号执行
规格说明 (Python/Z3) → Z3 求解器 → 公式 → 约束
✓ 已验证 × 反例
等价 发散

图 1: Hyperkernel 验证流程。C 语言实现（左）被编译为 LLVM IR 并通过符号执行提取行为公式。规格说明（右）提供 Z3 约束。Z3 检查一致性：如果公式对所有输入都满足约束，则系统调用被验证；否则产生反例。

这种“一键式”方法无需手动证明：给定正确的规格说明，验证完全自动化。因此，瓶颈从证明构建转移到规格编写，这正是 OSV-Bench 评估的内容，也是 BODHI 所要解决的问题。

### II-C 结构化思维链 (SCoT)

思维链（CoT）提示[22 (https://arxiv.org/html/2605.23931#bib.bib10)]通过在最终答案之前引出中间推理步骤来改进 LLM 推理。结构化思维链（SCoT）[11 (https://arxiv.org/html/2605.23931#bib.bib2)]将思维链框架推广到代码生成，利用顺序、分支和循环等程序结构来指导中间推理过程。SCoT 不是生成自由形式的推理文本，而是首先生成一个捕获目标程序控制流的伪代码骨架，然后在该骨架中填充实现细节。这种对输出生成过程的结构分解在 HumanEval 和 MBPP 等代码生成基准上显示出了优于基本 CoT 的效果[11 (https://arxiv.org/html/2605.23931#bib.bib2)]。

我们从 SCoT 中汲取灵感，但以根本性的不同方式将其适应于规格生成场景。SCoT 通过构建模型生成代码的方式来分解输出，而 BODHI 则通过将领域特定的翻译模式组织成结构化参考材料（第 III 节 (https://arxiv.org/html/2605.23931#S3)）来分解输入。

提示（约 31K tokens）
# 系统提示：你是一位操作系统内核验证专家。... 仅提供 Python 代码块中的规格说明代码。
# 编程模型：proc_state = {PROC_RUNNING: BitVecVal(3,64), ...} page_type = {PAGE_TYPE_FREE: BitVecVal(0,64), ...} # 常量、类、字段、辅助函数 ...
# 5 样本示例：示例 1: sys_alloc_port [描述] + [C] → [规格] # ... 另外 4 个系统调用示例及其真实规格
# 翻译指南 (BODHI):
## 1. 规格说明模板——函数结构
## 2. 前置条件——对每个 C 错误检查取反
## 4. 映射字段语法——read() vs write[]
## 7. PTE 公式——x86 与 IOMMU 模式
# ... 15 个类别，519 行
# 目标任务：给定系统调用 sys_set_runnable。 [描述]: 将胚胎进程设置为可运行 ... [C 代码]: int sys_set_runnable(pid_t pid) {...} [规格说明]: # 生成此

生成的规格说明
```python
def sys_set_runnable(old, pid):
    cond = z3.And(
        z3.And(pid > 0, pid < dt.NPROC),
        old.procs[pid].ppid == old.current,
        old.procs[pid].state ==
            dt.proc_state.PROC_EMBRYO,
    )
    new = old.copy()
    new.procs[pid].state =
        dt.proc_state.PROC_RUNNABLE
    return cond, util.If(cond, new, old)
```

C 语言实现 → 前置条件 后置条件 → Python/Z3 规格说明
```c
int sys_set_runnable(pid_t pid) {
    struct proc *proc;
    if (pid <= 0 || pid >= NPROC) return -EINVAL;
    proc = proc_find(pid);
    if (!proc) return -EINVAL;
    if (proc->ppid != current) return -EACCES;
    if (proc->state != PROC_EMBRYO) return -EINVAL;
    proc->state = PROC_RUNNABLE;
    proc_ready_add(proc);
    return 0;
}
```

前置条件
后置条件
Python/Z3 规格说明
```python
def sys_set_runnable(old, pid):
    cond = z3.And(
        z3.And(pid > 0, pid < dt.NPROC),
        old.procs[pid].ppid == old.current,
        old.procs[pid].state ==
            dt.proc_state.PROC_EMBRYO,
    )
    new = old.copy()
    new.procs[pid].state =
        dt.proc_state.PROC_RUNNABLE
    return cond, util.If(cond, new, old)
```

**Figure 2:** An example task from OSV-Bench for the `sys_set_runnable` system call. The prompt (upper left) includes the programming model, 5-shot examples, and the target task with a functional description and C implementation. BODHI supplements this with a structured translation guide. The model generates a correct specification (upper right) that passes Z3 verification. The C code (lower left) shows the error-checking logic (pre-conditions) and state-update logic (post-conditions). The generated specification (lower right) correctly encodes these as a Z3 formula.