为什么 eBPF verifier 报错难修：诊断鸿沟

当开发者将 eBPF 程序加载到 Linux 内核时，verifier 必须在字节码执行之前证明程序安全。verifier 遍历程序的每一条可能执行路径，逐指令跟踪它对每个寄存器和栈槽的了解。如果发现某条指令无法证明安全，例如通过未验证的指针访问内存、读取超出数据包边界或存在无界循环，它就会拒绝程序并打印报错。

问题在于，verifier 的报错只指出它卡住的那条指令，而不是程序出错的那条指令，两者可能相隔甚远。边界检查可能在二十条指令之前就该做；指针可能在经过某个分支后丢失了类型信息；helper 函数返回的值可能不再被 verifier 跟踪。开发者看到的是最终症状，而非根因。

论文 Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections 系统地研究了这一诊断鸿沟。我们在固定的内核和编译器配置下复现了 235 个真实的 verifier 拒绝案例，然后追问：最后一条 verifier 报错究竟能告诉你多少修复信息？答案出人意料地少。EINVAL 覆盖了 47% 的案例；同一条归一化后的报错字符串最多对应 9 种完全不同的根因。

verifier 的工作原理

要理解 verifier 报错为何难调试，需要先了解它的工作方式。verifier 执行的是抽象解释：它模拟程序执行但并不真正运行，只跟踪每个寄存器和内存位置在每条指令处可能包含的简化模型。

这个模型叫做抽象状态。对于每个寄存器，verifier 可能知道：这是指向数据包的指针，有效范围从偏移 0 到 42。或者：这是一个标量，值在 0 到 255 之间。或者：这是 bpf_map_lookup_elem 返回的指针，程序还没有检查它是否为空。这些事实约束了程序可以安全执行的操作。

verifier 在遍历程序时逐步建立这些事实。当程序执行边界检查（if (ptr + 8 > data_end) return），verifier 记录 ptr 现在已知距离末尾至少有 8 字节。当程序调用返回 map 值的 helper，verifier 记录指针类型和空检查要求。当程序分支时，verifier 探索两条路径并分别跟踪哪些事实成立。

这些累积的事实就是后续指令依赖的证明。只有 verifier 仍能看到访问在边界内的证明，数据包读取才是安全的。只有指针来自 lookup helper 并通过了空检查，map 值写入才是安全的。站内的 eBPF 安全概览 更系统地介绍了 verifier 的安全角色；本文聚焦诊断问题。

关键点：证明可以丢失。持有带边界的包指针的寄存器可能被覆盖。分支可能合并两条路径，一条有证明，一条没有。编译器可能优化掉建立证明的操作，或者重排指令使 verifier 看不到关联。当这种情况发生时，verifier 会在需要证明的指令处拒绝程序，而不是在丢失证明的指令处。

验证停止的位置与证明丢失的位置

论文中的数据包解析例子很典型。程序先计算 UDP header 指针，将其与 data_end 比较，再读取 dest 字段。

if (udph + sizeof(struct udphdr) > data_end)
    return 1;
 
dst_port = __constant_ntohs(((struct udphdr *)udph)->dest);

论文图 1 将三种视角并列呈现：源代码读取 UDP header，原始 verifier log 停在 R5 invalid mem access 'scalar'，证明诊断则指出这次读取所需的条件：解引用发生时，寄存器仍应是 verifier 能识别的包指针。

这段代码看起来已经做了边界检查，但字节码在读取位置已不再保留包指针证明。最后一条报错 R5 invalid mem access 'scalar' 表明 verifier 看到的是标量，而它需要的是包指针。报错没有说明包指针何时变成了标量，也没有区分是源代码少了边界检查、编译器 lowering 抹掉了指针来源，还是开发者应该重新派生一个 verifier 能识别的指针。

这就是诊断鸿沟：报错指出的是症状，而非原因。源代码可能完全正确；问题可能出在编译器如何 lower 它，或者 verifier 如何跨分支跟踪类型。另一种情况是源代码确实有 bug，但位置比报错指向的早二十行。无论哪种情况，仅凭最后这条信息都无法区分。

235 个可复现拒绝案例说明了什么

为了用真实数据研究这一问题，我们收集了开发者实际遇到的 verifier 拒绝案例。最初从 Stack Overflow 问题、GitHub issue、GitHub 修复提交和 Linux kernel selftest 收集了 936 个候选报告。使用 Linux 6.15.11、clang 18 和 verifier log level 2 重新构建并加载每个候选，最终 235 个在这套固定配置下仍能触发 verifier 拒绝。其余案例有的依赖特定环境，有的在选定工具链下不再复现，还有一些缺少重新构建所需的源代码。

这一筛选过程限定了数据能够回答的问题：它提供的是一组可复现样本，并非对所有开发者遇到的 verifier 失败的估计。每个保留案例都包含出错的源代码和报告中的开发者修复，二者共同为根因及修复所在层次提供标注依据。

191 个案例通过修改程序源代码得到修复，占样本的 81%；另外 44 个案例的源代码符合原本意图，修复分别落在编译器 18 个、环境 14 个、verifier 12 个。以上下文字段读取为例，-O0 可能在 lowering 过程中让 verifier 可见的指针类型退化成标量，调整编译选项即可恢复，C 代码的逻辑保持不变。仅凭被拒绝的指令，很难判断应该从哪一层着手。

我们进一步把 191 个源代码 bug 分成 12 类根因，其中 10 类来自 eBPF 特有的约束，包括边界、指针来源、对象生命周期和 helper 调用协议；这些概念在普通 C 编程中并不存在。

不同类别需要不同修复：收紧标量范围、保证每条路径都有数据包边界、检查 map 查询结果、按正确顺序释放引用，恢复的 verifier 事实各不相同。看到 invalid mem access 'scalar' 的开发者，仅凭这条消息无法判断修复应该是边界检查、空检查、类型转换还是编译器选项。

为了测量最后一条报错本身的区分能力，我们将其中的寄存器编号和 offset 归一化。235 个拒绝产生了 167 个不同字符串，归一化后得到 82 个消息模板，其中 15 个模板各自覆盖多类根因。最常见的四类模板已经说明同一句报错可能对应多少种问题。

更粗粒度的 EINVAL 出现在全部可复现拒绝的 47% 中。

verifier log 实际上包含的信息远比最后一条报错多：在 log level 2 下，它会打印每条指令后的抽象状态。问题是开发者必须手动追踪这些状态才能找出证明丢失的位置。日志最后一行省略了将被拒绝操作连回根因和修复层次所需的历史。

从拒绝位置追到修复信息

有用的诊断应该回答最后一条报错没有回答的问题：verifier 在被拒绝的指令处需要什么证明？程序在哪里丢失了它？

论文引入了一个名为 bpfix 的研究原型来尝试这种重建。它读取 verifier 的 log level 2 输出（逐指令抽象状态），从被拒绝的操作向后追踪。它识别需要什么证明（数据包边界、指针来源、空检查等），该证明何时首次出现在状态中，何时消失。如果有调试元数据，它会将这些转换映射回源代码行。

论文中的一个 map 值案例说明了区别。开发者直接将 BPF map 对象的地址转换为指针并尝试写入：

__u64 *v = (__u64 *)&globals;
*v += 1;

verifier 以 only read from bpf_array is supported 拒绝了写操作。报错指出了被拒绝的操作，但没有点明根本问题：不能直接通过 map 对象指针写入。verifier 期望的是 map 值指针，必须通过 bpf_map_lookup_elem 这样的 helper 获取。正确的修复遵循这套协议：

__u32 key = 0;
__u64 *v = bpf_map_lookup_elem(&globals, &key);
if (!v)
    return 0;
*v += 1;

修复用三个步骤建立所需证明：查找 map 元素、检查返回指针是否为空、通过该指针写入值。能够指出所需证明（来自 helper 的 map 值指针）和丢失点（直接转换）的诊断，比最后一条报错提供了更多信息。

这种方法还能区分报错相同但需要不同修复的案例。一个程序从整数 offset 构造数据包地址；它从未建立包指针来源，需要修改源代码。另一个程序正确派生并检查了指针，但编译器优化在读取前把值合并成标量；修复是编译器选项，不是源代码修改。两者都产生 invalid mem access 'scalar'，但属于不同的修复层次。

LLM 能修复 verifier 报错吗？

论文测试了更好的诊断上下文能否改善自动修复效果。如果诊断鸿沟确实重要，模型在收到缺失的证明信息时应该表现更好，而不是只收到原始 verifier log。

我们构建了 bpfix-bench，一个包含 75 个源代码级修复任务的基准。其中 40 个围绕特定 verifier 证明构造，修复后的程序必须重新建立该证明；35 个从 Cilium、xdp-tools 和 bpftime 等开源项目中最小化得到。

每个任务都附带独立于诊断工具的可执行测试套件。候选修复必须完成编译、通过内核 verifier 加载、通过功能测试和源语义检查。最后一项要求很重要：它能识别通过删除问题代码路径或改变程序行为来消除报错的补丁。成功意味着恢复一个 verifier 能接受的程序，同时保持它原本应该做的事。

实验比较两种提示条件：模型收到原始 verifier log，或收到更短的诊断信息（指出所需证明和相关源代码区间）。在温度为 0 的设置下测试三种模型：Qwen3.6 27B、GLM 5.2 和 Qwen2.5 3B（作为低容量对照）。一次生成模式直接评判首个候选；重试模式反馈一次失败信息后允许第二次尝试。

结果显示，当模型收到证明定位上下文而非原始日志时，表现一致提升。Qwen3.6 27B 的一次生成成功率从 29% 升至 51%；GLM 5.2 从 37% 升至 51%；Qwen2.5 3B 从 0% 升至 11%。允许重试后提升仍然保持：Qwen3.6 从 40% 升至 59%，GLM 从 63% 升至 69%。

研究还记录了每个一次生成候选最先失败的阶段，便于进一步拆解汇总数字。

分阶段细分显示提升来自哪里。Qwen3.6 的 verifier 加载失败从 19 降到 10，源语义失败从 22 降到 16。这正是与恢复证明并保持行为相关的阶段，诊断补充的正是这些信息。

3B 模型呈现不同模式。verifier 加载失败从 62 降到 39，原先超出上下文窗口的提示现在能正常处理。但编译失败从 7 增至 14；模型到达了更多的修复尝试，但基本代码生成仍然力不从心。

这些结果的适用范围有限：三种模型、75 个任务、温度为 0、最多一次重试。即使最好的结果（允许重试后 52/75）仍有许多任务未解决。但跨模型的一致提升支持一个具体结论：知道丢失了哪个证明，比只知道验证停止的位置，更有利于修复。

实践中调试 verifier 报错

论文的发现给调试 verifier 拒绝提供了一种不同的方法。与其问“这一行哪里错了”，不如先问被拒绝的操作需要什么。

许多 verifier 拒绝都是因为某条指令需要一个 verifier 没有的证明。数据包读取需要包指针来源和有效边界。map 值写入需要来自 lookup helper 并做过空检查的指针。dynptr slice 需要存活的 dynptr 对象。识别所需证明是第一步。

下一步是沿抽象状态向后追踪，看这个证明何时出现、何时消失或从未出现。verifier log 在 level 2 包含这些信息（它打印每条指令后的状态），但需要手动阅读。寻找寄存器从有类型的指针变成标量的位置，边界在分支合并后消失的位置，或者必需的检查从未出现的位置。

实用的阅读顺序：

1. 识别被拒绝的操作：它是哪种访问？数据包读取、map 写入、helper 调用？
2. 说出所需证明：数据包边界、指针来源、空检查、标量范围？
3. 向后追踪：寄存器何时有这个证明？何时丢失？是否曾经有过？
4. 判断修复层次：问题在源代码（缺少检查）、编译器（优化隐藏了证明）、环境（内核版本错误）还是 verifier（精度限制）？

有时这种追踪会越过源代码。如果抽象状态显示证明已建立然后在编译过程中被丢弃，修复可能是编译器选项。如果源代码从未建立证明，则需要代码修改。最后一条报错是起点；证明历史告诉你在哪里修复。

参考文献

• Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections
• bpfix GitHub 仓库
• Linux kernel eBPF verifier 文档
• BPF Verifier Visualizer
• An Empirical Study on the Challenges of eBPF Application Development
• bpftime userspace eBPF runtime