eBPF 验证器：把内核扩展变成可判定问题
The eBPF Verifier: Turning Kernel Extensions into a Decidable Problem
Linux 把曾经只能写在内核模块里的观测、网络与安全逻辑，部分开放成 eBPF 程序：一段受限制的字节码，在内核里 JIT 后挂钩点运行。没有验证器，这就只是又一种内核模块。有了验证器，它试图先当一个静态分析器：在加载前证明程序会停、不会任意乱指内存、辅助函数调用合法。2020 年代的开放问题是：这个分析器够不够精确、够不够完备、以及「可判定」的边界如何随内核演进移动。
本页只讨论机制与研究问题。不讨论如何绕过验证器，不提供利用步骤。
破除误解：通过验证不等于内核无漏洞
验证器证明的是相对一份内核抽象语义的性质：寄存器值域、栈槽、映射（map）访问、指针类型。它不证明挂钩点的并发、不证明辅助函数实现、不证明 JIT 后端、不证明硬件。加载成功的程序仍运行在有漏洞的内核里。把 eBPF 说成 seL4，类型错了。
第二个误解是 eBPF 等于「用户态随便改内核」。加载需要能力与签名策略；许多发行版把类型和挂钩点收得很紧。可编程数据路径改变的是经批准的扩展面，不是取消权限模型。
第三个误解是验证器已经「解决」了程序终止。它用有界循环、状态剪枝和路径计数来避免无限分析。真实程序为了通过，常常把算法改写成验证器能看懂的形状。这是接口对程序结构的反向压力，不是终止性问题的数学结局。
现场：抽象解释在加载路径上
加载时，验证器对 BPF 指令做抽象解释：跟踪每条路径上寄存器是标量还是指针、数值区间、对齐、空指针可能。访问包数据必须先做长度检查，检查必须被分析器看见。对 map 的查找返回的指针带类型，解引用被限制在该类型里。调用辅助函数要匹配原型。
状态爆炸是日常。路径一多，验证器放弃或拒绝。程序作者于是写「验证器友好」的控制流：展开循环、减少间接、把复杂逻辑搬回用户态。CO-RE（Compile Once – Run Everywhere）用 BTF 把内核结构偏移变成可重定位的重写，降低「每个内核版本编一次」的成本，同时给验证器更多类型信息。
生产里 Cilium、bpftrace、生产剖析器把 eBPF 做成默认观测面。研究论文在 2020 年代反复测量：拒绝率、误拒（本来安全却过不了）、以及验证器 bug 导致的误放行。最后一类是安全事件；前两类是可编程性税。开放问题在精度与性能之间：更重的分析让更多合法程序通过，也让加载变慢、攻击面变成分析器本身。
开放问题：完备性、并发、规范漂移
验证器不是对一份冻结规格的模型检测。内核每周都在加辅助函数与程序类型。规范漂移意味着：去年的「可判定子集」今年不同。形式化工作试图抽出可证明的核心，与正在长的 C 实现之间永远有缝。这与 CompCert 的冻结语言非常不同。
并发是另一道缝。程序在网卡软中断或追踪点上跑，与内核其余部分共享数据结构。验证器看到的是单线程字节码。数据竞争、ABA、错误的 RCU 用法不在当前合同中心。把 eBPF 当并发原语用的人，必须自己遵守内核惯例。
用户空间验证器、形式化重写、用证明助手生成可加载字节码，是活跃研究。目标不是让所有 C 程序进内核，是让被批准的扩展有一份比「C 里来回打补丁」更硬的合同。进展按程序类型计，不按「内核已安全」计。
JIT 把通过验证的字节码变成机器码。开放问题包括：验证器语义与 JIT 语义是否一致、Spectre 一类微架构通道是否要把某些程序类型关进更钝的沙箱、以及辅助函数的实现能否被单独审计。2020 年代的内核安全讨论里，eBPF 同时是观测的救星和扩展面的新成员。诚实的研究表述是：它把一部分扩展从「任意内核模块」收成「可分析的子集」，子集的边界每周都在谈判。
生产约束也很具体。验证器的时间限制会让合法但路径多的程序加载失败，于是作者把逻辑拆进多个程序或搬回用户态。复杂性没有消失，只是被推到挂钩点之外。对云厂商，谁能加载何种程序类型，已经变成产品策略：观测默认开、数据包改写默认关，或反过来。验证精度与治理是同一枚硬币的两面。
程序类型把挂钩点写成不同的合同。跟踪点上的程序多半只读、短命；数据包路径上的程序必须在预算内决定转发、丢弃或改写，并证明每次访问包数据都先经过长度检查。映射类型再把共享状态收成带类型的键值：哈希、数组、环形缓冲，各有验证器能看见的访问规则。辅助函数是内核自愿暴露的系统调用子集，原型必须匹配。这三层——程序类型、映射、辅助函数——构成可判定问题的签名。签名一变，去年能加载的字节码今年可能被拒。这不是运维噪音，这是「可判定子集」随主线移动的定义。
抽象解释跟踪的不是具体值，是寄存器的种类与区间。标量可以做算术，指针必须带着类型、对齐与可解引用的范围。分支把状态拆成两条路径，汇合时做并。并得太粗，安全的程序会被拒；并得太细，路径数把加载时间打满。有界循环把终止从数学问题收成分析预算：循环次数必须对分析器可见。作者于是把算法改写成展开、查表或搬回用户态。可编程性税以「为了通过验证而改写的程序结构」来计，不以「内核是否允许 eBPF」的布尔值来计。
BTF 与 CO-RE 把内核结构布局从编译期常数改成加载期重写。验证器因此看见更多类型，而不是看见一份冻在某个内核版本上的偏移表。形式化研究试图抽出这份抽象解释的核心，与正在增长的 C 实现对照。缝永远在：新辅助函数、新程序类型、以及 JIT 后端是否与解释语义一致。Spectre 一类微架构通道把某些程序类型推进更钝的沙箱，那是硬件合同，不是字节码合同。本页不讨论如何探测这些通道；只登记分层：验证器证明的是相对内核抽象语义的性质，不是相对流水线的性质。把两层混写成「eBPF 已安全」，类型就错了。
加载权限与签名策略决定谁能把哪一类程序送进验证器。发行版可以把观测打开、把数据包改写关上，而不改分析器算法。研究论文测量误拒与误放行，是在测分析器；生产事故若来自错误的能力授予，是在测治理。两条曲线必须分开画。开放问题因此有两个终点：一份更能跟上主线的规格，以及一套不把「允许 eBPF」写成空话的许可制度。精度提高而不收紧许可，只是把扩展面变宽；许可收紧而分析器仍误放行，只是把事故推迟到下一次加载。
观测用例（追踪、剖析、流量统计）与强制用例（防火墙、强制访问）对误放行的代价不对称。前者错了多半是数字难看，后者错了是策略被绕过。因此生产系统常把强制逻辑拆成：验证器能看懂的短程序，加上用户态策略编译器。复杂性没有消失，它被放在编译器必须生成「验证器友好」字节码这一层。研究若只改进分析精度、不讨论这层编译约定，会低估真实合同：可编程内核扩展，首先是一门面向分析器的编程语言。精度与治理必须同场出现，缺一则只是把事故换个房间发生。
跨域连接
- 证明：验证器是在线的、不完全的证明检查：失败不意味着程序一定危险，通过不意味着相对硬件为真。开放问题是如何把这份检查接到可发表的规格上，使内核演进时证明义务跟着补丁走。形式化验证前沿文给出离线、高保证的对照；eBPF 给出在线、低延迟、必须跟主线内核一起活的对照。
- 范畴论：程序类型与挂钩点像对象，验证器像只接受某些态射的检查。CO-RE 重写像自然变换：同一程序在不同内核对象上重新对准。类型一乱，变换不合法，加载失败。范畴语言在这里只提醒：可移植性是结构之间的映射，不是把字节码复制到另一台机器。
- 组合学：路径状态是组合对象。剪枝启发式决定哪些组合被合并。合并过猛，精度下降，误拒上升；合并过弱，分析超时。验证器工程是在组合爆炸上找能跑完的等价类，不是在写新的 BPF 指令。
- 国家能力：谁能加载何种 BPF，是机器内部的许可制度。发行版与云厂商把能力收进策略，等于在可编程内核上重建行政法。能力过宽，扩展面变成攻击面；过窄，观测只能回到内核模块。治理问题与验证精度问题绑在一起：分析器越不可靠，许可就必须越保守。策略文档若只写「允许 eBPF」而不写程序类型与签名，等于把行政法写成一句空话，强制力无处落点。
参考文献
- Starovoitov, A., Borkmann, D. 等. Linux 内核文档 bpf/verifier 与相关提交（随主线版本变化，引用时核对 tag）。
- Fleming, M. "A Thorough Introduction to eBPF." Linux Weekly News, 2017. （机制导读，延伸而非唯一佐证）
- Gershuni, E. et al. "Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions." PLDI, 2019.
- Nelson, L. et al. 关于 BPF 验证器可靠性与形式化的后续论文（OSDI/SOSP/PLDI 2020s，读时核对该程序类型是否仍被主线支持）。
- Cilium 项目关于 eBPF 数据路径的公开设计文档（生产约束，对照内核语义）。