필사 모드: eBPF Verifier 只告诉你它在哪儿停下 — 复现 235 例拒绝后测出的诊断落差

• 引言 — 错误指向的是停下的地方，bug 在别处
• 什么是诊断落差 — 丢失证明的地方 vs 验证停下的地方
• 数据集是怎么造出来的 — 从 936 例到 235 例
• 发现一 — 19% 的拒绝源码本身没问题
• 发现二 — 12 种根因，其中 10 种是 eBPF 特有的
• 发现三 — 一条错误字符串遮住了 9 种根因
• 现有工具为什么补不上这个落差
• bpfix — 从日志中复原证明的生命周期
• 一个真实案例 — aya issue 1002
• LLM 能修复 verifier 错误吗 — bpfix-bench
• 这些数字该信到什么程度
• 与此同时，verifier 本身也在变
• 那么实务者该做什么
• 结语
• 参考资料

引言 — 错误指向的是停下的地方，bug 在别处

只要认真写过一次 eBPF 程序的人，都体会过这种感觉。你明明对包指针做了边界检查，可是很久之后的一条加载指令却抛出 R5 invalid mem access 'scalar'。错误指向的那一行看不出任何问题。于是你只能这样做 — 把看起来能改的地方都改一遍，重新加载，要是又被弹回来，就再改别的地方。eBPF 开发变成一场反复试错的循环，问题就出在这里。

正如 eBPF 基础完全掌握 一文中梳理过的，verifier 存在的理由很明确。要在内核里跑任意代码，就得有人证明它是安全的，而 verifier 就是代替你完成这个证明的角色。问题在于证明失败时，verifier如何解释这次失败。

2026 年 7 月 2 日发布在 arXiv 上的 Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections(Zheng 等，arXiv:2607.02748)首次认真测量了这种挫败感。作者分别来自 UC Santa Cruz、Virginia Tech、Telecom Paris、University of Washington、University of Connecticut，以及 eunomia-bpf。

论文里的一句话概括了全部内容 — 错误只报告验证在哪里停下，不报告程序在哪里丢失了 verifier 所要求的证明。

什么是诊断落差 — 丢失证明的地方 vs 验证停下的地方

这个区分是全文的核心，所以稍微讲慢一点。

verifier 逐条指令地往下走，为每个值累积一份「这个值可以安全使用」的证明。比如对包指针来说，那份证明就是「这个指针停留在边界之内」。一旦某条指令想在没有这份证明的情况下使用某个值，验证就在那里停下，程序被拒绝。

然而，证明丢失的时刻和证明变得需要的时刻，通常并不是同一个时刻。论文给出的执行示例把这一点讲得很清楚。在某个中间状态下，R5 是 pkt(off=34,r=42)，也就是带有边界信息的包指针。但在指令 37 之前的状态里，同一个 R5 却被表示成标量值 40。而指令 37 正好要解引用 R5。

• 丢失证明的地方：包指针在某处变成了标量(论文中称为 loss point)
• 验证停下的地方：指令 37(错误唯一告诉你的地方)

错误只告诉你后者。而开发者真正该修的是前者。用论文的话说，修复必须恢复丢失的证明，可错误只给需要那份证明的那次操作命了名。于是开发者不得不从执行轨迹里手工反推出「当时需要什么证明、又是在哪里消失的」。

数据集是怎么造出来的 — 从 936 例到 235 例

论文实证部分之所以诚实，是因为它没有隐藏方法论。

作者从四个来源收集了 936 个候选案例 — Stack Overflow 问题、GitHub issue、GitHub 修复提交、内核自测。然后把每个候选案例都在同一套固定工具链上重新构建：内核 6.15.11、clang 18、日志级别 2。(6.15 是 2025 年 5 月发布的主线系列稳定点版本。)

936 例里，在这套构建下真正被拒绝的只有 235 例，这 235 例构成了名为 bpfix-empirical 的数据集。其余案例被剔除的原因也写明了 — 要么在作者的工具链下不会被拒绝，要么需要特定环境，要么已经没有可重建的源码。

每个案例都配有问题源码和开发者本人实际采用的修复。这一点很关键 — 「真正的根因是什么」这个答案不是作者猜出来的，而是原始报告里留下的实际修复告诉他们的。

发现一 — 19% 的拒绝源码本身没问题

按「修复落在哪里」对 235 例分类，第一个意外的结果就出现了。

• 191 例(81%)：修复改动了程序源码 — 也就是真正的程序 bug。
• 44 例(19%)：源码本身是对的，却依然被拒绝。修复落在了别的层面 — 编译器 18 例，环境 14 例，verifier 本身 12 例。

论文举的例子很有说服力。一次显然安全的上下文字段读取被拒绝，原因是 -O0 把这次读取降级(lowering)成了标量，导致 verifier 看不到指针的来源(provenance)。修复是一个完全不碰源码的编译器标志。论文 Figure 2 里的代码就是这么简单。

// 正确的源码。-O0 把字段读取降级成了标量
static int add_one(int x) { return x + 1; }
int prog(struct xdp_md *ctx) { return add_one(ctx->rx_queue_index) & 1; }
// verifier: R2 invalid mem access 'scalar'

这一点在实务上相当重要。verifier 拒绝了并不代表你的代码写错了。大约五次里有一次，代码本身是对的，是编译器遮住了证明，或者环境不匹配，又或者 verifier 还不理解这种模式。可惜错误信息并不会区分这两种情况。

发现二 — 12 种根因，其中 10 种是 eBPF 特有的

191 例真正的 bug 可以归为 12 种根因。这里的「根因」指的不是 verifier 检查失败的那一项，而是开发者在源码层面犯的错误。

论文指出，这 12 种里有 10 种是 eBPF 特有的。证明包的边界，或者把 dynptr 与它的生命周期正确配对，都不是普通 C 编程知识能带来的能力。所以要修复它们，需要的不是一般的编程功力，而是领域知识。缺少空值检查算是个例外，是唯一相对通用的一类。

这也从数量上解释了为什么 eBPF 的学习曲线这么陡 — 大多数问题都不是「把 C 写好」就能解决的那种。

发现三 — 一条错误字符串遮住了 9 种根因

最扎心的数字出现在这里。

第一，errno 几乎不给任何信息。全部拒绝里有 47% 只返回一个 EINVAL。也就是说，将近一半都被归到了一个只表示「出了点问题」的错误码里。

第二，错误字符串本身也太粗糙。作者把每条错误字符串里的寄存器编号和偏移量掩盖掉，做归一化后，把 235 例归了类。167 条互不相同的字符串，收敛成 82 个模板。而这 82 个模板里，有 15 个分别对应着不止一种根因。

最严重的是下表第一行。

单单 invalid mem access 'scalar' 一条，就在 28 个案例中遮住了 9 种不同的根因。指望看这条消息就能缩小根因范围，在统计上是没有根据的。照搬论文的 Takeaway 一句话来说 — 终端错误粗糙到无法指导修复。

现有工具为什么补不上这个落差

你可能会问，难道没有现成的工具吗?论文提到了两个。

PrettyVerifier(Rizza 等，2025 IEEE CSR)用正则表达式把终端错误映射到源码行和提示。BPF Verifier Visualizer(bpfvv)是一个把逐指令状态交互式渲染出来的前端。bpfvv 仓库自己也把它描述成一个原始的调试器 UI — 解读的是日志，而不是运行时状态。

论文给出的评价是这样的 — 两者都能帮开发者读懂错误，但都没有指出证明是在哪里丢失的。

而对于为什么这件事很难，论文的解释也很犀利。像 Rust 这样语言的错误解释工具，能沿着检查器已经建好的结构走 — AST、类型约束。但 eBPF verifier 不会暴露这样的产物。留下来的只有日志。

bpfix — 从日志中复原证明的生命周期

于是作者做了 bpfix。核心洞见是这样的 — 在日志级别 2 下，verifier 会为每条指令打印出完整的抽象状态。也就是说，丢失的证明其实已经活在日志里了，只是没人去读它而已。

bpfix 用 Rust 写成，约 2.3 万行，唯一必需的输入是现成的 verifier 日志。源码或对象元数据是可选的，提供了会让指令到源码的映射更准确。流水线分三个阶段。

1. 日志解析 — 把终端错误和逐指令的抽象状态提取成一条归一化的证据流。
2. 证明复原 — 把终端错误映射到某个证明族(proof family)上，比如指针来源、包的边界、标量范围之类，并追踪该证明的证据何时成立、何时被维持、又在何时消失。
3. 生成诊断 — 挑选出相关的代码片段(span)，并给出重新建立证明所需的指引。

输出是一份 Rust 风格的纯文本诊断，由稳定的错误标识符、所需的证明、相关的片段与证据、可观测情况下的 loss point，以及一条 help: 指引组成。「可观测情况下」这个限定语是作者自己加上的 — 并不是每次都能捕捉到。

另一个实用的功能是责任层的区分。bpfix 把一次拒绝标记为 source_bug(源码层)或 lowering_artifact(编译器层) — 这正好直接对应前面看到的「19% 源码没问题」的情况。不过论文明确把这称为尽力而为的归因(best-effort attribution)。

论文的 Figure 5 精确地展示了这一点。两次拒绝的终端消息完全相同，都是 invalid mem access 'scalar'，但一个是源码 bug(Stack Overflow 56965789 — 在没有包基址的情况下把整数偏移强转成指针)，另一个是编译器 lowering 产物(Stack Overflow 53136145 — 分支合并遮住了包指针的类型)。修复该落在哪一层完全不同，可 verifier 给出的消息却一模一样。

一个真实案例 — aya issue 1002

来看论文给出的一个具体例子。程序把映射对象 &globals 的地址强转成 __u64 *，直接读写它。

// 被拒绝的程序
__u64 *raw_map = (__u64 *)&globals;  // 映射对象指针
__u64 v = *raw_map;
*raw_map = v + 1;                    // 在此处被拒绝

// verifier: only read from bpf_array is supported

verifier 的消息没有错。它只是陈述了症状 — 它看到了一次经由映射对象的写操作。至于为什么不允许、该怎么做，它没有说。

bpfix 给出的诊断是这样的 — 映射指针正被当作普通内存来访问(source_bug)；所需要的证明是，在读写映射内容之前，先通过合适的映射辅助函数(map helper)导出一个映射值指针；接下来该做的是先查找元素，再通过那个指针写入。

而开发者实际采用的修复，正好完全遵循了这个诊断。

// 开发者实际的修复
__u32 key = 0;
__u64 *v = bpf_map_lookup_elem(&globals, &key);
if (!v) return 0;
*v += 1;

LLM 能修复 verifier 错误吗 — bpfix-bench

论文的最后一条主线，是如今大家真正关心的问题。反正错误日志迟早要丢给 LLM 处理，那它到底行不行?

作者搭建了一个叫 bpfix-bench 的基准测试，一共 75 道源码级修复题，其中 40 道是围绕特定的 verifier 证明构造的，另外 35 道则是从 Cilium、xdp-tools、bpftrace 等开源项目里精简出来的。

评分方式很诚实。每道题都配有一套独立于 bpfix、可执行的测试套件。要让一次修复被判定为成功，必须(1)真正通过内核 verifier 加载，(2)通过功能测试，(3)通过源码语义检查。也就是说，光靠「看起来说得通的文本」拿不到分，靠破坏逻辑来绕开 verifier 这种常见小聪明，也会被源码语义检查抓住。

测试用的模型是 Qwen3.6 27B(主模型)、GLM 5.2(托管)、Qwen2.5 3B 三种，温度均为 0。加入 3B 模型是为了看看这个提升在小模型上是否依然成立。结果如下(均为 75 题满分，作者自测)。

从这张表能读出两件事。

第一，只给原始 verifier 日志时，目前的模型修得并不好。单次成功率在 0% 到 37% 之间。用论文的说法，从 3B 到 27B 这三个模型来看，verifier 拒绝对再有能力的模型也仍然是个难题。

第二，把日志换成 bpfix 诊断后有所改善。论文摘要里给出的提升幅度是 11 到 21 个百分点。按单次成功率看，Qwen3.6 提升最大，达到 21.4 个百分点，Qwen2.5 3B 提升 10.7 个百分点，GLM 5.2 提升 13.4 个百分点。不过要注意 — 这一点得对着表格自己核实 — GLM 5.2 在重试模式下的提升幅度小得多，只有 6.6 个百分点，摘要给出的区间是按单次成功率来读才对。

作者还把失败发生在哪个阶段做了拆解，这一点反而更有说服力。在 Qwen3.6 27B 上，verifier 加载失败从 19 例降到 10 例，源码语义失败从 22 例降到 16 例。GLM 5.2 也是同样的方向(10 → 5，25 → 22)。两边的编译失败数都维持在低位。

小模型的情况值得单独看一下。Qwen2.5 3B 用原始日志时，75 道题一道都没修好。单次尝试的候选修复里有 62 个在 verifier 加载阶段就失败了，还有 3 个提示词直接超出上下文窗口，连程序都没能返回。换成更短的 bpfix 诊断后，模型调用失败消失了，加载失败也降到 39 例，但编译失败反而从 7 例升到了 14 例。作者自己的解读很坦诚 — bpfix 给了小模型足够的 verifier 相关信息，让它能尝试更有意义的修复，但普通的代码生成错误依然存在。

这些数字该信到什么程度

从这里开始，是论文自己说明的局限，再加上我读的时候附加的保留意见。首先要说清楚，本文的大多数数字都是作者自测得到的 — bpfix 和这套基准测试都出自同一个团队。

选择效应相当明显。936 个候选案例里，只有 235 个留了下来。留下来是因为它们在作者的固定工具链上复现了，而被剔除的 701 个里，相当一部分是环境依赖的，或者已经没有源码可以重建。而且数据来源一开始就是 Stack Overflow 和 GitHub issue — 让人困惑到愿意专门发帖提问的那些拒绝会被过度代表。样本可能天然就偏向「诊断不足」这个结论。当然，里面也混入了内核自测和修复提交，所以并非纯粹的偏差，而且也有一个站得住脚的反驳：实务中真正拦住人的，恰恰就是这些让人困惑的拒绝。

工具链被固定在了单一版本上 — 内核 6.15.11、clang 18。verifier 每个版本都在变，尤其是错误信息和剪枝(pruning)行为一直在被打磨。不应该假设在 6.15 上测出的 47%，放到最新内核上依然成立。

模型的选择也有限 — Qwen3.6 27B、GLM 5.2、Qwen2.5 3B，评测里没有前沿级模型。所以准确的说法不是「LLM 修不好 verifier 错误」，而是「这三个模型用原始日志修好了 0% 到 37%」。

而且即便用了 bpfix，天花板依然不高。最好的成绩是单次 50.7%，加上重试也只到 69.3%。「诊断越好、修复越好」这个方向在三个模型上都一致成立，但离「现在可以直接交给 LLM 处理」还有相当距离。

工具的成熟度也得考虑进去。bpfix 仓库以 MIT 协议开源，v0.1.0 于 2026 年 7 月 11 日发布，是个刚满五天的 0.1.0。README 自己就明确写着，它既不是内核补丁，也不是 verifier 的替代品，更不是自动源码修复工具，而是一个诊断说明工具。在把它接入生产流水线之前，抱着这个程度的预期才是对的。

与此同时，verifier 本身也在变

如果说这篇论文的思路是「把日志读得更好」，那么对面还有另一条路子 — 「一开始就让 verifier 少拒绝一点」。

LWN 的 BPF loop verification with scalar evolution(Daroc Alden，2026 年 6 月 9 日)报道过的 Eduard Zingerman 的工作就是一个例子。这是在 2026 年 LSFMM+BPF 峰会上展示的一项进行中的工作，目标正如 Zingerman 本人所说，是让 verifier 能单次遍历就处理典型的 for/while 循环，而不必真的把循环跑一遍。

目前的 verifier 遇到循环时，会逐次迭代评估直到抵达终止条件，这个过程中可能会误触指令数上限 — 一个更好的实现原本不该触发的限制。标量演化(scalar evolution)正是想通过计算循环内变量可能取值的范围来避免这一点。

不过这还只是一个原型，尚未合并。它还处理不了溢出到栈上再恢复的寄存器，也无法统一分析所有循环变量。Zingerman 表示，计划在补上栈操作、带符号整数运算、更复杂循环的支持之后，再考虑提交进内核。至于加载时间，他本人说还没有做过严谨的测量。(Starovoitov 提到，过去类似的 verifier 改动一开始也曾引发担忧，但最终都让加载时间变快、内存占用变少。)

这两条路线是同一个问题的两面 — 一条在减少拒绝，另一条在拒绝发生时让它可以被理解。而后者永远不会消失。不管 verifier 变得多聪明，拒绝总会存在，存在的拒绝就需要被解释。

那么实务者该做什么

即便不引入任何工具，这篇论文也有一些东西是可以直接拿来用的。

把日志级别 2 设成默认值。bpfix 之所以能够存在，根本原因就是「所需要的信息其实已经在日志里了」。在级别 2 下，verifier 会为每条指令打印抽象状态。要是没打开它，你其实是在把诊断所需的原材料直接丢掉。

不要相信终端错误那一行。那只是验证停下的地方，bug 在证明消失的地方。真正该做的是沿着日志往回走，找到出问题的寄存器最后一次拥有正确类型的时刻 — 比如 pkt(off=..,r=..) 变成 scalar 的那个点。

不要一见拒绝就先怪自己。五个里有一个源码本身完全正常。如果你正好在用 -O0 或者某种特殊的优化级别构建，那么怀疑编译器 lowering 是有统计依据的。

不要把靠错误字符串搜出来的答案原样照搬。invalid mem access 'scalar' 背后藏着 9 种根因。Stack Overflow 上挂在同一条消息下的答案，恰好适用于你这个案例的概率，比你想的要低。

要交给 LLM 处理的话，不要只丢日志。这篇论文说明的是，诊断质量决定了修复的成功率。人先自己把上下文缩小一步 — 需要什么证明、在哪里丢失的 — 结果就会不一样。

结语

这篇论文的价值不在于告诉了我们新事实，而在于它把 eBPF 开发者早已用身体感受到的东西变成了数字。大家都知道 verifier 的错误没什么帮助，但没人知道 47% 是 EINVAL，也没人知道一条错误字符串背后能藏着 9 种根因。

而诊断为什么会难到这个地步，其根本原因是结构性的，这一点也很有意思。Rust 编译器能沿着自己构建出来的类型约束走一遍，从而解释一个错误。eBPF verifier 不会留下这样的产物，留下的只有日志。bpfix 做的事情，归根结底是一种把日志逆向工程还原成产物的操作。这是个巧妙的解法，但如果 verifier 一开始就把证明结构暴露出来，这项工作本就没有必要存在。长远来看，真正能弥合这道落差的路径，大概率还是在内核这一侧。

眼下，bpfix 还是个刚满五天的 0.1.0，提升幅度是作者自测的结果，而且只在一套工具链上测过。所以这篇文章的结论不是「快去用 bpfix」，而是这一句 — verifier 停下的地方和你 bug 所在的地方，是两个不同的地方。哪怕只是明确知道这一点再去读日志，下一次面对 invalid mem access 'scalar' 时花掉的时间，大概也会少一些。

参考资料

• Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections (Zheng 等，arXiv:2607.02748，2026 年 7 月 2 日)
• eunomia-bpf/bpfix — 论文的工具实现(MIT，v0.1.0 / 2026 年 7 月 11 日)
• BPF loop verification with scalar evolution (Daroc Alden，LWN，2026 年 6 月 9 日)
• libbpf/bpfvv — BPF Verifier Visualizer
• eBPF verifier — 内核官方文档
• eBPF 基础完全掌握 — 程序、映射与 Verifier 的世界(相关文章)