eBPF Verifier 深度剖析——安全沙箱的验证之路
当一段用户态代码需要以内核特权级运行在 Linux 内核中时，如何保证它既不会崩溃内核、也不会泄露敏感信息、更不会陷入死循环？eBPF Verifier —— 这个位于 kernel 中的静态验证器，承担了"在内核中安全执行不受信任代码"的最后防线。本文基于 Linux 6.8+ 内核源码（kernel/bpf/verifier.c，约 16000 行 C 代码），深入拆解 verifier 的核心验证机制。
一、Verifier 的总体架构与设计哲学
1.1 为何需要 Verifier
eBPF 程序加载到内核后运行在特权模式，拥有对内核内存的受限访问能力。如果没有 verifier，恶意或有缺陷的 eBPF 程序可能造成：
- 内核崩溃（空指针解引用、越界访问）
- 信息泄露（读取未初始化内核内存并外泄）
- 死循环/超长执行路径（导致内核 hang 住或 soft lockup）
- 特权提升（篡改关键内核数据结构）
Verifier 的目标是在加载时静态验证程序安全性，确保满足三大安全不变量：
- 无越界内存访问：所有指针运算的结果必须落在已映射的合法范围内
- 无信息泄露：所有外发到用户态的数据必须已被显式初始化
- 有限执行：程序必须在有限步骤内终止，不允许无限循环
1.2 Verifier 的执行时机
用户态调用 bpf(BPF_PROG_LOAD, ...)
→ bpf_check() // kernel/bpf/verifier.c 入口
→ check_cfg() // 控制流图(CFG)验证
→ do_check() // 逐指令模拟执行
→ check_map_access() // map 访问验证
→ check_return_value() // 返回值范围校验
→ check_max_stack_depth() // 栈深度验证
→ 若全部通过 → jit_compile() → 注入内核
Verifier 在程序加载时执行一次，通过后程序才允许编译为机器码注入内核。这意味着验证开销是一次性的，运行时零开销。
1.3 三个核心数据结构
// 指令级状态跟踪（每个基本 Block 一个）
struct bpf_verifier_env {
struct bpf_prog *prog; // 被验证的 eBPF 程序
struct bpf_verifier_state *cur_state; // 当前验证状态
struct bpf_verifier_state *head_state; // 入口状态
struct bpf_state_list_entry *exploration_state; // 搜索队列
u32 insn_idx; // 当前指令偏移
u32 insn_processed; // 已处理指令总数
u64 init_insn_processed; // 初始处理数
// 验证配置
bool allow_ptr_leaks;
bool allow_uninit_ctx_access;
bool bypass_spec_v1;
// ...
};
// 基本块级的验证状态快照
struct bpf_verifier_state {
struct bpf_func_state *frame[MAX_CALL_FRAMES]; // 调用栈帧
struct bpf_verifier_state *parent; // 父状态（用于 DFS 回溯）
struct bpf_verifier_state *branches; // 分支探索状态
u32 jmp_history_cnt;
// ...
};
// 函数调用栈帧状态
struct bpf_func_state {
struct bpf_reg_state regs[BPF_REG_MAX]; // 寄存器状态数组
enum bpf_stack_slot_type slot_type[MAX_BPF_STACK]; // 栈槽类型
u8 *stack[MAX_BPF_STACK / STACK_SPAN_DEPTH]; // 栈帧区域
// ...
};
二、控制流图验证——可终止性的第一道验证
2.1 构建 CFG
Verifier 先将 eBPF 程序的控制流图（CFG）构建出来，检查以下条件：
- 无不可达代码（dead code detection）：所有指令都能从入口到达
- 无越界跳转：跳转目标必须在程序范围内
- 无向后跳转（Linux 5.3 前完全禁止，后允许受限循环）
- 指令数上限：单程序最大指令数由
sysctl net.core.bpf_jit_kernenv配置，默认 100 万条（特权模式）或 4096 条（非特权模式）
2.2 循环检测与展开
// 循环检测的核心思想：状态合并 + 指令计数
// kernel/bpf/verifier.c
static int check_cfg(struct bpf_verifier_env *env)
{
// 1. 构建控制流图
// 2. DFS 遍历所有可达节点
// 3. 识别回边（back edge）
// 4. 对循环展开有界模拟（不执行无限次）
// 5. 验证每个回边对应一个合法的循环退出条件
}
Linux 5.3+ 允许受控循环，但每个循环的迭代次数理论上必须是可静态上界的，或者包含显式的退出条件（如 if (--count == 0) break）。Verifier 通过状态等价判定来避免对循环进行完全展开：如果循环某次迭代进入某基本块时，寄存器/栈的状态与之前某次进入时"覆盖"之前的状态（即当前值是之前值的安全超集），则可以终止展开。
2.3 DFS 搜索的状态空间管理
Verifier 使用深度优先搜索(DFS)遍历所有可能的执行路径。对分支指令，它先将一边完全探索完毕，再回溯探索另一边。关键数据结构是状态快照栈：
入口 → Block_A → if cond
├─ true路径 → Block_B → ... → exit
└─ false路径 → Block_C → ... → exit
当 DFS 探索到 exit 时，回溯到最近一个未探索的分支点，继续探索另一分支。
visited 状态缓存：Verifier 为每个基本块维护 visited 状态快照。当再次进入同一个基本块时，若当前状态被已有状态"覆盖"（即当前所有寄存器的精度不高于已有状态），则可跳过该路径。这是 verifier 能够处理大型程序而不指数级爆炸的关键优化。
三、逐指令模拟执行——安全性的核心战场
3.1 寄存器状态模型
Verifier 为每个 eBPF 寄存器维护一个精确实数（Precise Register State），包含：
struct bpf_reg_state {
enum bpf_reg_type type; // SCALAR_VALUE / PTR_TO_* / STACK / ...
// 标量值范围跟踪
struct tnum tnum; // 追踪数值（位掩码+值）
s64 smin_value; // 符号最小值
s64 smax_value; // 符号最大值
u64 umin_value; // 无符号最小值
u64 umax_value; // 无符号最大值
// 指针类型信息
enum bpf_type_id id; // 类型 ID（用于跨指令关联）
struct bpf_map *map_ptr; // 仅当 type == PTR_TO_MAP_VALUE
// 子寄存器精度信息
u8 precise : 1; // 是否需要精确比较
// ...更多字段
};
关键字段说明：
- tnum：追踪数值（Tracked Number），由(value, mask)组成。若 mask 中位为 0 表示该位值未知。例如
tnum(0xFFFF, 0x0F0F)表示低 8 位已知、中间位已知、高位未知。 - smin_value/smax_value：64 位有符号取值范围。Verifier 对每条算术/比较指令更新这两个值。
- type：寄存器当前持有的类型（标量、指针、栈槽引用等），这是所有安全检查的基础。
3.2 指令模拟的虚拟机实现
Verifier 用 do_check() 函数逐条模拟 eBPF 指令的执行：
static int do_check(struct bpf_verifier_env *env)
{
struct bpf_insn *insn = env->prog->insnsi;
int insn_cnt = env->prog->len;
for (int i = 0; i < insn_cnt; i++) {
// 1. 根据 opcode 分类处理
switch (BPF_CLASS(insn[i].code)) {
case BPF_ALU: // 算术运算：更新 smin/smax 和 tnum
case BPF_JMP: // 跳转指令：分支 DFS、验证条件可静态判定
case BPF_LD: // 加载指令（包括 map 访问辅助函数）
case BPF_ST: // 存储指令：更新栈类型
}
// 2. 检查访问安全（每次内存访问前）
if (is_access) {
check_mem_access(env, reg, offset, size);
check_stack_access(env, reg_idx);
}
// 3. 验证次数上限
if (++env->insn_processed > BPF_COMPLEXITY_LIMIT) {
verbose(env, "exceeded complexity limit\n");
return -EACCES;
}
}
}
3.3 值传播与精度分析
Verifier 对算术运算的值范围进行截断分析（Truncation Analysis）：
示例： smin smax tnum(value, mask)
──────────────────────────────────────────────────────
r0 = 0 0 0 (0x00000000, 0x00000000)
r0 |= 0xFF 0 255 (0x000000FF, 0x00000000)
r0 <<= 32 ? ? (0x00000000, 0xFFFFFFFF)
→ shift 后 smin/smax 未知（可能为负，也可能很大）
边界情况：u32 和 u64 的截断传播需要精确处理
当 r0 = (smin=-2147483648, smax=2147483647) 时，强制截断到 u32 范围 → (0, 4294967295)
Verifier 维护符号/无符号视角的双重范围——同一段位模式在不同上下文中有不同的值域，且每次比较（如 r0 < 100）会根据结果分支分别窄化。
四、内存安全检查——守护内核的边界
4.1 指针有效性验证
每次内存访问前，Verifier 调用 check_mem_access() 验证访问安全：
static int check_mem_access(struct bpf_verifier_env *env,
int regno, int off, int size,
bool zero_size_allowed,
enum bpf_access_type t)
{
struct bpf_reg_state *reg = &env->regs[regno];
switch (reg->type) {
case PTR_TO_STACK:
// 必须落在 [BPF_REG_SIZE, MAX_BPF_STACK) 范围内
// 且对应槽位类型必须匹配
if (off < -EBPF_STACK_SIZE || off + size > 0)
goto err;
if (env->stack[off].slot_type != type)
goto err;
break;
case PTR_TO_MAP_VALUE:
// 必须在 map 值大小范围内
if (off < 0 || off + size > map->value_size)
goto err;
break;
case PTR_TO_PACKET:
// 在 packet 范围内，但有额外限制
// 必须是用 packet_pointer 指令获取的
break;
case PTR_TO_CTX:
// 只能访问上下文结构中允许的字段
// 由 bpf_prog->expected_attach_type 和
// bpf_ctx_access_info 定义允许的偏移/大小
break;
}
}
4.2 栈帧空间管理
eBPF 程序有严格的栈空间限制：每个函数帧最多 512 字节。Verifier 用 bpf_stack_slot_type 数组追踪每个字节槽（栈按字节粒度追踪）的状态：
enum bpf_stack_slot_type {
STACK_INVALID = 0, // 未初始化（禁止读取）
STACK_SPILL, // 被寄存器溢出
STACK_MISC, // 通用写入数据
STACK_ZERO, // 零初始化
};
栈操作的核心规则：
分配栈空间 (r10 -= N)：在指针存在之前，必须标记所有槽位为 STACK_INVALID
写入 (BPW/BPH/BPDWORD [r10+off], value)：更新对应槽位类型为 STACK_MISC 或 STACK_SPILL
读取 (BPF_LDX 从 r10+off)：检查槽位类型 != STACK_INVALID，否则报错 "read from uninitialized stack"
退出函数前：栈指针必须恢复到入口值（即不能泄露栈帧中的指针引用）
4.3 指针运算安全
Verifier 对指针运算的检查极其严格，核心规则：
// 允许的指针运算：
// 1. 常量偏移访问（如 ctx + offset, map_value + offset）
// 2. 寄存器偏移访问——仅限特定辅助函数中
// 不允许的操作：
// - 指针之间的加减
// - 指针乘以/除以某值
// - 指针与指针异或（无法判断安全性）
// - map_value 指针作为尾调用的参数（map 内存归还后可能失效）
对寄存器偏移的可变范围检查（variable offset check）， verifier 会验证：
r1 = map_value (umin=0, umax=4096)
r2 = variable (smin=0, smax=1023)
r3 = r1 + r2 → 结果范围 [0, 5119]，但 map->value_size=4096
→ verifier 检查 umax < value_size → 5119 < 4096 → FAIL
→ 修改为 r3 = r1 + r2 & 0xFFF：umax=4095 < value_size → PASS
实际检查使用 tnum 进行精确位级验证，而非简单的范围比较，因此能够识别如 & mask 这样的安全措施。
五、尾调用与函数调用的验证
5.1 尾调用 (BPF_JMP | BPF_CALL)
尾调用（Tail Call）是 eBPF 中跨程序链式执行的关键机制，基于 bpf_tail_call() 辅助函数实现。Verifier 对尾调用有特殊的验证逻辑：
安全约束：
- 签名匹配：Tail Call 的目标程序必须在同一 map（
BPF_MAP_TYPE_PROG_ARRAY）中索引，且目标程序必须已经过验证并加载入内核 - 上下文兼容：目标程序期待的上下文类型必须与调用方的上下文类型兼容（例如都是
struct __sk_buff） - 栈释放：调用方函数的所有栈帧和寄存器在跳转时不被保留——目标程序从零状态开始执行
- 尾调用链深度限制：默认最多 33 次尾调用（用户可调整
sysctl net.core.bpf_jit_kernenv中的bpf_tail_call_depth），防止无限递归
Verifier 如何跟踪尾调用链：
// kernel/bpf/verifier.c
static int check_max_stack_depth(struct bpf_verifier_env *env)
{
// 尾调用不会增加栈深度（每帧都是独立的 512 字节帧）
// 但 tail_call_depth 需要累计跟踪
depth = env->subprog_depth; // 子程序深度
tail_call_depth = env->tail_call_depth; // 尾调用链深度
// 两者之和不能超过限制
if (depth > BPF_CALL_DEPTH_LIMIT) {
verbose(env, "the depth of the call chain is too large\n");
return -E2BIG;
}
// 尾调用后的程序仍然会继续验证（从目标_func入口）
// 因此两条路径的栈帧使用相互独立
}
5.2 函数调用 (BPF_JMP | BPF_CALL, BPF_FUNC_*)
对于非尾调用的函数调用，Verifier 需要验证：
- 参数类型匹配：调用 BPF_FUNC_* 时，每个辅助函数的参数类型必须匹配
- 常量参数验证：某些辅助函数要求参数为常量（如
bpf_map_lookup_elem的 flags 参数） - 返回值类型：辅助函数的返回值类型必须正确使用（不可对 SCALAR 类型做指针运算）
- 调用后寄存器污染：调用辅助函数会重置 r1-r5 寄存器（称为 caller-saved），Verifier 会自动标记它们为 SCALAR_VALUE（未知值）
六、类型系统与状态跟踪
6.1 指针类型层次
Verifier 的寄存器类型系统是一个精细的层次结构：
SCALAR_VALUE（标量值，无指针含义）
↓
PTR_TO_系列（指针类型）
├── PTR_TO_PACKET (指向 packet 数据的指针)
├── PTR_TO_MAP_KEY (指向 map 键的指针)
├── PTR_TO_MAP_VALUE (指向 map 值的指针)
├── PTR_TO_MEM (通用内存指针)
├── PTR_TO_BUF (指向 buffer 的指针)
├── PTR_TO_STACK (指向栈帧中数据)
├── PTR_TO_CTX (指向 eBPF 上下文结构)
├── PTR_TO_SOCKET (指向内核 socket 对象)
├── PTR_TO_TCP_SOCK (指向 TCP socket)
├── PTR_TO_BTF_ID (指向 BTF 类型对象)
│ PTR_TO_BTF_ID_OR_NULL (可能为空)
└── PTR_TO_FLOW_KEYS (指向 flow keys)
SPILL_REGISTER（栈中溢出的寄存器，关联到具体寄存器编号）
6.2 空指针验证
// 返回值可能为 NULL 时，类型标记为 *_OR_NULL
reg->type = PTR_TO_MAP_VALUE_OR_NULL;
// 使用前必须检查
if (reg->type == PTR_TO_MAP_VALUE_OR_NULL) {
// 插入显式检查：if (reg == 0) { return; }
// 检查后分支内类型窄化为 PTR_TO_MAP_VALUE
if (tnum_equals_const(reg->var_off, 0)) {
// 已知 NULL，标记为不可解引用
} else if (tnum_within(reg->var_off, range)) {
// 已知非 NULL，窄化类型
__mark_reg_not_null(reg);
}
}
6.3 跨基本块的值追踪
跨基本块的值追踪是 verifier 中最复杂的算法之一。核心机制：
寄存器版本号（Register Versioning）：
每次修改寄存器时，版本号递增。Verifier 比较两个状态是否"相同"时，不仅比较值，还比较快照号：
struct bpf_reg_state {
// ...
int32_t id; // 分配 ID（跨指令唯一）
enum bpf_ref_obj_id ref_obj_id; // 引用对象的 ID
u32 mem_size; // 引用的内存大小
struct {
u32 precise : 1; // 是否需要精确比较
u32 ref_obj_id_set : 1; // 引用对象 ID 是否有效
// ...
} flag;
};
状态快照与合并：
当两个执行路径汇合到一个基本块时，Verifier 需要合并两个分支进入时的前入状态：
路径 A 进入：r1 = SCALAR(min=0, max=100), r2 = PTR_TO_STACK(off=-16)
路径 B 进入：r1 = SCALAR(min=0, max=200), r2 = PTR_TO_STACK(off=-16)
合并后： r1 = SCALAR(min=0, max=200), r2 = PTR_TO_STACK(off=-16)
↑ 取并集，精度降低
当合并导致精度降低时，Verifier 会标记 precise = 1，要求后续所有条件分支在此状态上进行精确比较——这是防止精度丢失导致安全检查失效的关键保障。
七、调试技巧与常见报错
7.1 使用 Verifier Log
加载失败时，内核会在 bpf_log_buf 中输出详细的验证日志：
// 用户态使用
char buf[65536] = {};
union bpf_attr attr = {
.prog_type = BPF_PROG_TYPE_XDP,
.insns = (uintptr_t)insns,
.insn_cnt = insn_cnt,
.license = (uintptr_t)"GPL",
.log_buf = (uintptr_t)buf,
.log_size = sizeof(buf),
.log_level = 2, // 1=错误 2=错误+详细状态跟踪
.kern_version = LINUX_VERSION_CODE,
};
bpf(BPF_PROG_LOAD, &attr, sizeof(attr));
// 失败时 buf 中包含详细的 verifier 轨迹
Log Level 2 下，Verifier 输出每条指令执行后的寄存器状态，以及每条安全检查的判断过程。
7.2 常见报错与解决方案
错误1："invalid stack off=-16 size=8"
原因：栈偏移访问超出当前栈帧已分配的空间
解决：确保对该槽位执行了写操作，或增加栈分配
错误2："R1 read from uninitialized stack"
原因：读取了未初始化的栈槽
解决：在读取前先写入至少一次
错误3："unreleased reference to map"
原因：程序退出时未释放 map 引用（如获取的 socket 未调用 bpf_sk_release）
解决：在所有退出路径上确保释放引用
错误4："subprog doesn't exist"
原因：尾调用目标索引对应的 subprog 未找到
解决：检查 BPF_MAP_TYPE_PROG_ARRAY 中对应索引的程序是否已加载
错误5："the depth of the call chain is too large"
原因：尾调用链或调用链深度超限
解决：减少尾调用次数（默认 33），或重构程序减少调用深度
错误6："BPF program is too large (insn_processed 1000001)"
原因：单程序超过复杂度上限
解决：使用尾调用拆分程序
错误7："invalid bpf_context access off=8 size=4"
原因：访问了上下文中不允许访问的字段
解决：检查 bpf_prog_type 对应的 allowed_access 列表
错误8："R7 has unknown scalar value"
原因：辅助函数要求常量参数，而传入的是运行时值
解决：确保参数值在编译时已知（不可使用变量）
错误9："math between pointer and pointer prohibited"
原因：两个指针相加，无法确定安全性
解决：检查指针运算逻辑，移除指针间运算
错误10："variable ctx access is not allowed"
原因：使用变量偏移访问 packet/socket/ctx，导致无法静态验证边界
解决：改用循环 + 常量偏移，或限制 offset 范围（如 offset &= mask）
7.3 实用调试策略
策略1：渐进式编写
从最简单的 eBPF 程序开始，逐步增加功能，每次验证通过后在日志中观察 verifier 推断出的寄存器状态
策略2：模拟执行观察
使用 log_level=2 配合 BPF_PROG_LOAD 附带的日志，观察 verifier 逐条指令的状态变化
策略3：参考已有程序
bpf/samples/ 目录中的程序通过合并的测试用例，查看详细 verifier 行为
策略4：使用 bpf object pinned map 调试
对于运行时行为，使用 bpf_object__pin_maps() 保留 map，通过 bpftool 查看 map 内容：
bpftool map dump pinned /sys/fs/bpf/my_map
策略5：perf 工具辅助
使用 perf_event_open + BPF_MAP_TYPE_PERF_OUTPUT_MAP 进行事件追踪
八、Verifier 对复杂程序的支持演进
8.1 BPF-to-BPF 函数调用
Linux 4.16 引入 BPF-to-BPF 调用后，Verifier 增加了子程序（subprog）验证逻辑。每个子程序独立验证入口条件，然后被调用者"内联"地记录其对寄存器状态的影响。这避免了在每次调用时重复展开子程序体。
8.2 BTF（BPF Type Format）
Linux 5.2 引入 BTF 信息在内核和用户态之间传递。Verifier 利用 BTF：
- 自动类型检查：BTF 定义的函数签名被 verifier 用来验证参数和返回值类型
- CO-RE（Compile Once - Run Everywhere）：通过 BTF 和 CORE relocations，Verifier 能在加载时根据运行内核的 struct layout 自动修正偏移
- kfunc 调用：Verifier 通过 BTF 验证 kfunc（内核函数）的参数类型
8.3 BPF TOKEN（Linux 6.x）
BPF token 机制允许非特权用户创建受限的 eBPF 程序。Verifier 利用 token 的 capability 标志（bpf_token_cap_*）决定放宽哪些检查：
struct bpf_token {
u64 caps;
// BPF_TRAP: 允许 bpf_modify_return
// BPF_TOKEN_BMAP: 允许不使用 map
// BPF_TOKEN_BTF: 允许使用 BTF 加载 kfunc
};
8.4 允许受限循环
Linux 5.3 起引入受控循环支持。核心机制是循环条件上界验证：
for (int i = 0; i < N; i++) { ... } // Verifier 要求 N 可静态上界
// 或"内循环不超过 N 次"的上界已知
实际验证中，Loop-Unrolling + 状态等价判断的组合使得 verifier 能够在有限资源下保证循环必然终止。
九、总结与前瞻
eBPF Verifier 是一个精巧但庞大的系统，其核心思想是"用近似精确的静态分析替代运行时的动态检查"。它通过控制流分析 + 值范围追踪 + 栈类型粒度跟踪 + 指针生命周期验证四重机制，在程序加载时构建了一张完整的安全契约。
展望未来发展方向：
- 精确指针追踪：当前 verifier 对指针解引用链的追踪仍在演进（如通过
PTR_TO_BTF_ID追踪具体对象生命周期） - 循环上界推导：借助约束求解的力量自动推导不可静态证明的循环上界
- 跨程序边界验证：尾调用链 + BPF-to-BPF 调用的组合场景仍存在未覆盖的边界条件
- Verifier 性能：对百万指令级程序，verifier 耗时已超过可接受范围，内核社区正在探索增量验证、并行验证等优化
截至 Linux 6.8，Verifier 已支持 30+ 种程序类型、超过 200 个辅助函数、复杂的指针追踪和循环验证。理解 Verifier 的工作原理，不仅是编写合规 eBPF 程序的必要条件，更是深入理解 Linux 内核安全设计的绝佳窗口。
参考链接： - kernel/bpf/verifier.c - Linux 源码 - BPF 设计与实现 - Quincey Kozior 博客 - Brendan Gregg - BPF 性能跟踪全书 - Official eBPF Docs - Verifier
发表评论 取消回复