Linux内核eBPF验证器深度剖析：从抽象解释到运行时安全保障

eBPF 技术的核心承诺是：允许用户态程序安全地在内核态执行任意字节码，而不会导致内核崩溃、内存损坏或安全风险。实现这一承诺的关键组件就是 eBPF Verifier —— 一个存在于内核中的静态程序分析器。本文从源码级别完整剖析 eBPF Verifier 的设计哲学与分析框架，深入解读寄存器状态建模、有界验证、路径剪枝、ALU sanitation、类型系统、回调函数验证以及 JIT 编译前的最终安全检查机制，并给出绕过常见验证失败陷阱的工程实践经验。

---

一、为什么内核需要一个静态分析器

1.1 eBPF 的信任模型

eBPF 允许用户将字节码加载到内核中，这些字节码会在网络包到达、系统调用入口、函数探针触发等关键路径上执行。传统内核模块虽然也有这种能力，但任何错误都可能导致整个系统崩溃。eBPF 的设计目标则根本不同：

安全性优先于性能：eBPF Verifier 必须在程序加载时（load-time）静态证明程序的绝对安全性，不存在运行时回退到解释器的安全网。一旦通过验证，程序将以原生速度 JIT 执行。

零信任执行模型：Verifier 假设所有 BPF 字节码都可能是恶意构造的。它必须在最坏情况下（而非平均情况下）证明程序的正确性，包括所有可达的执行路径。

1.2 安全保证清单

eBPF Verifier 必须确保以下安全属性：

┌─────────────────────────────────────────────────────────────┐
│               eBPF Verifier 必须证明的安全属性                    │
├─────────────────────────────────────────────────────────────┤
│  ✦ 无越界内存访问        → 所有指针运算必须经过边界检查             │
│  ✦ 无非法指令            → 必须是合法的BPF指令编码                  │
│  ✦ 无无限循环            → 所有循环必须有界且满足最大指令限制         │
│  ✦ 无未初始化变量读取     → 每个寄存器在使用前必须被初始化           │
│  ✦ 无类型混淆            → 指针类型追踪确保正确的上下文访问          │
│  ✦ 无资源泄漏            → map引用计数、栈帧分配必须平衡             │
│  ✦ 控制流完整性          —→ 无向后跳转（除有界循环外），无不可达代码  │
│  ✦ 无特权提升             —→ helper函数调用受程序类型约束             │
└─────────────────────────────────────────────────────────────┘

1.3 为什么不用解释器或沙箱

直觉上的替代方案是直接解释执行或在软件沙箱中运行。但 eBPF 被设计为在高频关键路径执行（每数据包、每次系统调用），解释执行会有 10-100x 的性能损失。软件沙箱（如 Intel MPX、软件 fault isolation）引入了边界检查开销且依赖特定硬件特性。

eBPF 选择了一种混合策略：加载时一次性支付静态分析开销，运行时零额外安全检查开销（JIT 后为原生指令）。这在性能和安全之间取得了最优平衡。

---

二、Verifier 架构总览：从字节码入口到验证完成

2.1 整体数据流

用户态
┌─────────────────────────────────────────────┐
│  BPF syscall (BPF_PROG_LOAD)                │
│  → 字节码 + license + prog_type + attach_ctx │
└──────────────────┬──────────────────────────┘
                   │ copy_from_user
                   ▼
内核态 eBPF Verifier
┌─────────────────────────────────────────────┐
│  1. 检查insn合法性 (check_insn)              │
│  2. 构建CFG (检测不可达基本块)                 │
│  3. 符号执行 (do_check_main)                  │
│     → 维护 env->cur_state 状态栈              │
│     → 每条指令推进寄存器状态                     │
│     → 分支处 fork 状态，探索所有路径             │
│     → 路径剪枝: 已访问且状态等价则跳过            │
│  4. 调用验证回调 (process_func_* )            │
│  5. 类型系统和返回值验证                        │
│  6. 最终状态回看 (final check)               │
└──────────────────┬──────────────────────────┘
                   ▼
              JIT Compiler
                   ▼
              原生机器码执行

2.2 核心数据结构

Verifier 的核心状态管理围绕以下三个结构体展开：

// include/linux/bpf_verifier.h

struct bpf_verifier_env {
    struct bpf_prog *prog;           // 正在验证的 BPF 程序
    struct bpf_verifier_state *cur_state;  // 当前执行路径状态栈顶
    struct bpf_verifier_state *head_state; // 状态链表头（BFS/DFS探索栈）
    struct bpf_func_state *func_stack;     // 函数调用的栈帧栈

    u32 insn_idx;                    // 当前指令索引
    u32 insn_processed;              // 已处理指令总数
    u32 prev_insn_idx;               // 上一条已处理指令

    // 路径探索状态管理
    struct bpf_verifier_state **explored_states;
    int allocated_stack;             // 状态栈深度

    // 类型和上下文追踪
    struct bpf_call_arg_meta *access_buffer; // 调用参数元信息
    // ... 调试和统计信息
};

struct bpf_verifier_state {
    struct bpf_reg_state regs[BPF_REG_MAX]; // 所有寄存器的抽象状态
    struct bpf_verifier_state *parent;      // 父状态（路径分叉点）
    struct bpf_verifier_state *branch;      // 兄弟分支
    struct bpf_verifier_state *next;        // 状态队列中的下一个
    u32 speculative_path : 1;              // 是否为投机路径
    u32 seen_since_last_sweep : 1;         // 活动状态标记
};

struct bpf_reg_state {
    enum bpf_reg_type type;    // SCALAR_VALUE / PTR_TO_MAP / PTR_TO_MEM / ...
    struct tnum tnum;          // 追踪数值范围和精度（抽象解释核心）
    s64 smin_value;            // 有符号最小值
    s64 smax_value;            // 有符号最大值
    u64 umin_value;            // 无符号最小值
    u64 umax_value;            // 无符号最大值

    // 指针类型专用
    struct bpf_map *map_ptr;   // PTR_TO_MAP 时指向的 map
    u32 map_uid;             // map 的唯一标识，防止 map 被释放后悬挂引用
    struct bpf_map_value *ValueType; // map 值类型

    enum bpf_type_flag type_flag; // PTR_MAYBE_NULL / PTR_TRUSTED 等
};

2.3 分析框架：抽象解释（Abstract Interpretation）

Verifier 的理论基础是抽象解释（Abstract Interpretation，Cousot & Cousot 1977）。它不追踪变量的精确值，而是追踪其抽象属性：

数值追踪 — TNum（Truncated Number）：64位值的三值表示 (mask, value)，其中 value 表示已知位的值，mask 表示哪些位已知（0=已知，1=未知）。

例如：value=0x10, mask=0xFFFF...FFFE 表示第0位未知，第4位为1，其余位为0，即可能值为 {0x10, 0x11}。

// TNum 定义（kernel/bpf/tnum.h）
struct tnum {
    u64 value;
    u64 mask;
};

// TNum 运算示例
tnum_add(a, b): 
    // 结果的 value = (a.value + b.value) & ~(a.mask | b.mask)
    // 结果的 mask  = a.mask | b.mask + 进位传播

这种表示在数值范围追踪的同时追踪未知位模式，兼顾了精度和性能——足以判断指针运算是否有越界风险。

---

三、指令级验证：符号执行引擎

3.1 寄存器语义模型

eBPF 有 11 个寄存器（R0-R10），Verifier 对每个寄存器维护完整的状态：

寄存器	用途	类型追踪
R0	函数返回值 / 程序退出值	每次调用后更新
R1-R5	函数参数 / helper 参数	map_lookup 后变为 PTR_TO_MAP_VALUE
R6-R9	调用者保存寄存器（callee-saved）	函数调用前后保持
R10	只读栈帧指针 (PTR_TO_STACK)	不可变指针，栈访问基准

3.2 ALU 指令验证

对每条 ALU 指令（如 BPF_ADD、BPF_XOR），Verifier 执行以下验证：

// kernel/bpf/verifier.c 中的简化逻辑

static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
{
    struct bpf_reg_state *dst = &env->cur_state->regs[insn->dst_reg];
    struct bpf_reg_state *src = &env->cur_state->regs[insn->src_reg];

    // 1. 检查源寄存器是否已初始化
    err = check_reg_arg(env, insn->dst_reg, SRC_OP);
    err = check_reg_arg(env, insn->src_reg, SRC_OP);

    // 2. 如果源是未标量值（指针），拒绝算术运算
    if (type_is_ptr(dst->type)) {
        verbose(env, "pointer arithmetic prohibited\n");
        return -EACCES;
    }

    // 3. 使用 TNum 抽象域追踪运算结果
    if (src->type == SCALAR_VALUE) {
        dst->tnum = tnum_add(dst->tnum, src->tnum);
        dst->umin_value = dst->umin_value + src->umin_value;
        dst->umax_value = dst->umax_value + src->umax_value;
    }

    // 4. 32位子寄存器追踪
    coerce_reg_to_size(dst, 4);  // BPF_ALU (32-bit)

    return 0;
}

3.3 内存访问验证：两条铁律

Verifier 对内存访问（BPF_LDX_MEM、BPF_STX_MEM等）实施严格的验证规则：

规则一：指针必须有明确的类型。 只有 PTR_TO_MEM、PTR_TO_STACK、PTR_TO_MAP_VALUE 等几种类型可以解引用。

规则二：偏移必须在声明的边界内。 例如，对于 struct tcphdr *th 来自上下文（ctx），Verifier 追踪 th 的有效大小为 sizeof(struct tcphdr)，任何超出此范围的偏移都会被拒绝。

访问模式示例:
  合法: r2 = *(r1 + 0)       // r1 = PTR_TO_MAP_VALUE, offset 0, 大小 = 8字节 ✓
  合法: r2 = *(r1 + 6)       // 如果 map 的元素大小 ≥ 14 字节 ✓
  非法: r2 = *(r1 + 100)     // 超出 map 元素边界 ✗
  非法: r2 = *(r6 + 0)       // r6 = PTR_TO_CTX, 需追踪 ctx 的 valid data range ✗

---

四、有界验证：确保终止性

4.1 核心挑战

Verifier 必须证明 BPF 程序不会无限循环——因为 BPF 程序运行在抢占被禁用的上下文中，无限循环将导致整个系统挂起。

Verifier 通过以下机制保证终止性：

┌─────────────────────────────────────────────────┐
│            有界验证三大机制                         │
├──────────┬──────────────────────────────────────┤
│ 机制      │ 说明                                  │
├──────────┼──────────────────────────────────────┤
│ 有界循环  │ 循环体必须满足：                        │
│          │  → 迭代次数有上界（常量或已知范围）         │
│          │  → 不包含 helper 调用                   │
│          │  → 循环体大小不能超过 8条BPF指令(保守限制)  │
├──────────┼──────────────────────────────────────┤
│ 指令计数  │ 每条路径的总指令数 ≤ 100万条 (24.5内核+)   │
│          │ 每次迭代处理成本 ≈ 1条(对循环体线性缩放)    │
├──────────┼──────────────────────────────────────┤
│ 探索状态  │ env->insn_processed 超过上限直接拒绝      │
│ 总量上限  │ 防止路径爆炸导致加载时间过长               │
└──────────┴──────────────────────────────────────┘

4.2 向后跳转检测

Verifier 将基本块组织为 CFG（控制流图），任何向后跳转（目标地址 < 当前地址）都被视为潜在循环入口。对于每个向后跳转，Verifier 尝试证明该循环必然终止：

// 简化：kernel/bpf/verifier.c

static int check_max_loop_count(struct bpf_verifier_env *env)
{
    // 1. 回溯到循环起始，计算循环体边界
    // 2. 如果循环计数无法静态确定 → 需要 bound
    // 3. 如果 bound 不可证 → 拒绝
    // 4. 对于有界循环，在验证阶段"展开"循环体若干次
    //    确保展开后的路径仍然安全
}

实际限制（Linux 6.x）： - 单次探索路径最多 100万条 BPF 指令处理 - 循环展开后单路径视为线性序列 - 程序中所有路径累计处理 ≤ env->explored_states 限制

---

五、类型系统和特殊指针追踪

5.1 寄存器类型层次

Verifier 维护一个复杂的类型层级，用于精确建模寄存器在不同时刻的含义：

类型层次（简化）:

SCALAR_VALUE          ← 任何数值指针算术的结果
PTR_TO_CTX            ← bpf_context 指针（XDP/tracepoint/sock等上下文）
PTR_TO_MAP            ← bpf_map 指针（通过 bpf_map_lookup 获得）
PTR_TO_MAP_VALUE      ← map 内的值指针
PTR_TO_MEM             ← 普通内核内存地址
PTR_TO_STACK           ← R10 栈帧指针
PTR_TO_SOCKET / SOCK_OPS 相关
PTR_TO_BTF_ID          ← 内核 BTF 类型指向的引用
PTR_TO_BUF             ← 缓冲区指针（如 skb->data）
PTR_TO_TCP_SOCK        ← 强类型追踪的协议对象
PTR_TO_TP_BUFFER       ← tracepoint 专用的缓冲区
MAYBE_NULL(type)        ← 可空标志修饰
PTR_TRUSTED            ← 完全信任指针（不可算术运算、可解引用）

5.2 可空指针追踪（Null-Check Liveness）

Verifier 追踪每个指针的可空状态，在解引用前必须经过 null check：

// BPF 代码示例:
r1 = bpf_map_lookup_elem(&my_map, &key)  // r1 = PTR_TO_MAP_VALUE | PTR_MAYBE_NULL
if r1 == 0 goto exit                     // ← 这一步设置 r1 = PTR_TO_MAP_VALUE
r2 = *(r1 + 0)                           // ← 此时 Verifier 知道 r1 不为空

实现机制：分支分叉时，Verifier 在 if r1 == 0 的两个分支中分别追踪： - then 分支（r1 == 0）: r1.type = SCALAR_VALUE（用于跳转匹配） - else 分支（r1 != 0）: r1.type = PTR_TO_MAP_VALUE（可空标志移除）

这种跨分支的状态追踪被称为 liveness 追踪（liveness analysis）——Verifier 精确知道哪些寄存器在哪些路径点"活着"（即将被使用）。

5.3 指针泄漏防护

Verifier 阻止任何将内核指针泄露到用户态或 map 中的方式：

禁止的行为:
  → 将 PTR_TO_MAP 或 PTR_TO_MEM 以 SSA 形式泄漏到 map 中
  → 使用指针直接进行跨 subroutine 的算术运算
  → 在没有边界检查的情况下将栈指针存储到 map

允许的行为:
  → 值拷贝: r2 = r1（如果 r1 是 SCALAR_VALUE 类型）
  → 指针 + 常量: r2 = r1 + 8（需要确保不越界）
  → 指针 - 常量: r2 = r1 - 8
禁止：
  → 指针 + 指针
  → 指针 ^ 指针
  → 指针 % 非常量

---

六、Helper 函数验证：接口契约执行

6.1 调用前契约检查

每个 BPF helper 函数都有严格的调用约定，Verifier 在调用点强制执行：

// kernel/bpf/verifier.c

static int check_helper_call(struct bpf_verifier_env *env, int func_id, 
                             int insn_idx)
{
    const struct bpf_func_proto *fn = &helper_proto[func_id];

    // 1. 检查程序类型是否有权调用此 helper
    if (!bpf_helper_prog_type_valid(env, func_id))
        return -EINVAL;

    // 2. 验证参数数量和类型
    for (i = 0; i < 5; i++) {
        err = check_func_arg(env, i, fn->arg_type[i], ...);
    }

    // 3. 验证上下文相关性（如 bpf_sock_addr 对 sockaddr 的写入不超过实际大小）
    if (fn->check_arg)
        fn->check_arg(env, fn);

    // 4. 根据返回类型设置 R0
    mark_reg_unknown(env, &env->cur_state->regs[BPF_REG_0]);
    env->cur_state->regs[BPF_REG_0].type = fn->ret_type;
}

6.2 返回值处理示例

bpf_map_lookup_elem 的 proto:
  arg1: PTR_TO_MAP           // map 指针
  arg2: CONST_SIZE_OR_ZERO   // key 指针  
  arg3: PTR_TO_STACK         // key 在栈中的位置
  ret:  PTR_TO_MAP_VALUE_OR_NULL  // 查找结果

Verifier 处理:
  → 如果 ret == MAYBE_NULL: 后续解引用前必须检查 NULL
  → 如果找到: 返回的指针指向 map value 内部，valid size = value_size
  → map 被释放时: 所有 PTR_TO_MAP_VALUE 类型的寄存器标记为无效（map uid 追踪）

---

七、ALU Sanitation：防御时序和投机执行攻击

7.1 问题背景

当 BPF 程序可以访问 kernel 地址指针时（某些程序类型的特权行为），攻击者可能利用 ALU 操作构造出有效的内核指针，绕过后续检查。更重要的是，在推测执行架构（Spectre类攻击）上，寄存器值可能存在于推测执行流水线中，被作为未经验证的指针间接访问。

7.2 BPF Constant Blinding（ALU Sanitizer）

对于使用常数进行 ALU 操作且结果是指针类型的情况，Verifier 注入 BPF_KPROBE_ON 宏生成临时指令序列，在执行时加一层随机掩码后运算，然后验证结果仍在范围内：

原始指令: r1 = r0 + 0x100    // 危险：攻击者通过 r0 控制地址

sanitize 后（运行时）:
  tmp = load_special_mask()   // 加载随机掩码
  r1 = r0 XOR tmp            // 用随机化打破地址可预测性
  r1 = r1 XOR tmp            // 恢复真实值  
  r1 = r1 + 0x100            // 在验证保障的范围内运算
  验证 r1 仍在有效范围内       // 安全检查

7.3 Spectre v4 / Speculative Store Bypass

对于可能与推测执行交互的指针加载，Verifier 还会附加 speculative 路径分析，确保：

• 每个条件分支的 then/else 两个方向的 LOAD 路径都被验证
• 即使推测路径执行了未验证条件的指令，也不能导致越界访问

---

八、路径剪枝与状态合并

8.1 状态精确度控制

Verifier 在探索每条路径时维护完整的寄存器状态集合。为避免路径爆炸（指数级增长），Verifier 实现了状态合并（state pruning）机制：

// kernel/bpf/verifier.c: 状态等价性判断

static bool state_equiv(struct bpf_reg_state *old, struct bpf_reg_state *new)
{
    if (old->type != new->type)
        return false;

    // 对于 SCALAR 类型，如果新状态的值域 ⊆ 旧状态的值域
    // 且 TNum 的已知位是超集 → 新状态已被"覆盖"
    if (old->type == SCALAR_VALUE) {
        if (old->smin_value <= new->smin_value &&
            old->smax_value >= new->smax_value &&
            (old->tnum.mask & new->tnum.mask) == old->tnum.mask)
            return true;
    }

    return false;
}

当遇到已访问过的程序点且当前状态被已有状态"支配"（dominate）时，剪枝这条路径——这保证了 Verifier 的复杂度在可管理范围内。

8.2 回溯深度限制

┌──────────────────────────────────────────────┐
│         Verifier 资源限制（Linux 6.7+)          │
├────────────────────┬─────────────────────────┤
│ 单路径最大指令探索  │ 1,000,000 条（约 200万处理量）│
│ 总探索状态数        │ 64k+（受内存限制）          │
│ 最大栈深度          │ BPF_MAX_CALL_LIMIT = 24      │
│ 循环展开次数        │ 受总指令数限制               │
│ 验证超时            │ 典型场景下 < 1秒              │
└────────────────────┴─────────────────────────┘

---

九、常见验证失败与排错实战

9.1 "Permission denied" — 指针运算越界

场景：

struct xdp_md *ctx = (struct xdp_md *)ctx;
void *data = (void *)(long)ctx->data;
void *data_end = (void *)(long)ctx->data_end;

if (data + sizeof(struct ethhdr) > data_end)  // ✅ OK
    return XDP_DROP;

struct tcphdr *tcp = data + sizeof(struct ethhdr) + sizeof(struct iphdr);
// ❌ 错误！多个 Verifier 未知偏移相加

修复： Verifier 要求每次加法的偏移是已知的并且在允许范围内：

struct tcphdr *tcp = data + 34;  // ETH(14) + IP(20)
if (tcp + 1 > data_end)           // 每次只做一次边界检查
    return XDP_DROP;

9.2 "R0 !read_ok" — 未读取返回的 map value

场景：

r0 = bpf_map_lookup_elem(&map, &key);
// 没有检查 r0 == NULL
bpf_printk("found"); // ❌ Verifier: R0 可能为 NULL

修复： 始终在使用前进行 NULL 检查：

r0 = bpf_map_lookup_elem(&map, &key);
if (!r0) return 0;     // ✅ 必须先检查
bpf_printk("found");

9.3 "Back-edge from insn X to Y" — 无限循环

场景：

for (int i = 0; i < 10; i++) {  // ❌ 当变量不可静态确界时
    // 循环体
}

修复： 使用 #pragma unroll 或 for (int i = 0; i < 10; __u32) 确保循环计数有明确上界。或者使用 bpf_loop() helper（Linux 5.17+）。

---

十、验证后流程：JIT 与安全保证链

10.1 验证成功的最终处理

当 Verifier 完整探索所有路径且未发现问题时，进入加载后流程：

验证完成 → 检查所有特殊指令（如 bpf_printk → 映射到 bpf_trace_printk）
        → 修正指令（如将 sd NULL 插入指针追踪标记）
        → 附加 info 记录到内核（bpf_prog_load info）
        → 进入 JIT 编译（bpf_prog_select_runtime）
        → JIT 编译为原生代码并挂载

10.2 运行时安全边界

验证通过后，BPF 程序运行时还保留两道安全边界：

禁用抢占 preemption disabled：大多数 BPF 程序执行时禁用抢占，防止程序执行时间过短。部分类型（如 XDP）还需要硬件配合。

指令边界检查（如有需要）：对于某些旧硬件，Verifer 会插入额外的边界检查。但现代 64位 x86/ARM64 上，验证后的程序完全以原生速度运行。

10.3 BPF CO-RE 与验证的关系

BPF CO-RE（Compile Once — Run Everywhere）机制允许可重定位的 BPF 程序在不同内核间移植。Verifier 在处理 CO-RE 重定位时确保：

• 所有通过 BTF 信息访问的内核字段偏移都是静态已知且已验证
• 重定位记录的一致性（map 引用、extern 符号等）
• 内核版本兼容性标记（BPF_CORE_READ 等）

这种机制大幅提升了 BPF 应用程序的可移植性，同时 Verifier 保证重定位后的访问安全性。

---

十一、性能与未来方向

11.1 Verifier 性能基准

对典型的 BPF 程序（数十到数千条指令），Verifer 的验证复杂度为 O(n × k)，其中 n 是指令数，k 是同位置的等价状态数。由于状态剪枝，k 通常很小：

程序规模          典型验证时间    状态数
  100 条指令      < 1 ms         < 10
  1000 条指令     1-10 ms        10-200
  10000 条指令    10-200 ms      200-2000
  100000 条指令   200ms-2s       2000-64000

11.2 Linux 6.x+ 方向

• BPF Open Maps (shared maps)：跨 BPF 程序共享 map，Verifier 追踪跨程序 map 引用
• BPF Token：无特权容器化 BPF，Verifier 在 token 作用域内授权 helper 调用
• 增强的 register state tracking：更精确的 SCALAR 值域追踪减少误报
• 可展开循环（bounded loops）：Linux 6.x 逐步放宽循环展开约束

11.3 Formal Verification 前沿

学术界正在将 eBPF Verifier 与形式化验证结合（例如 PCR 项目使用 Coq 验证参考 Verifier 的正确性），但目前内核中的 Verifier 仍然是经验驱动的工程实现——它的安全属性由数百万行测试用例保证，而非形式化证明。

---

十二、总结

eBPF Verifier 是一套在内核中实现的抽象解释引擎，它融合了寄存器状态建模、TNum 数值追踪、有界路径探索、类型系统和 ALU sanitation 多项技术。它巧妙地平衡了安全性（严格证明所有可达路径不存在安全风险）和性能（验证后直接 JIT 为原生指令，运行时零开销）。

理解 Verifier 不仅对编写正确的 BPF 程序至关重要，也为理解编译器/静态分析系统的设计提供了真实案例。其设计哲学——"支付高昂的分析开销以换取运行时零额外安全开销"——对构建安全关键系统具有普适意义。

┌─────────────────────────────────────────────────────────┐
│               eBPF Verifier 核心贡献                       │
├─────────────────────────────────────────────────────────┤
│  ✦ 首次在内核态实现了有界验证的零信任安全模型               │
│  ✦ 可以在加载时拒绝100%的恶意/错误程序                     │
│  ✦ 验证后的程序以原生指令速度运行，零运行时开销               │
│  ✦ 支撑了Cilium、Falco、Tetragon等新一代云原生基础设施       │
│  ✦ 设计思路: 静态分析 + 类型追踪 + 路径探索 + 状态剪枝       │
│  ✦ 学术价值: 工业级抽象解释和符号执行的标杆实现              │
└─────────────────────────────────────────────────────────┘

---

延伸阅读与参考： - kernel source: kernel/bpf/verifier.c（~20000+ 行 C 代码） - BPF Design Q&A: kernel.org/doc/html/latest/bpf/bpf_design_QAQ.html - BPF Verifier Errata: kernel source tools/testing/selftests/bpf/verifier/ - "Understanding the eBPF Verifier": qmonnet.github.io/whirl-offload/2021/04/17/ebpf-verifier-understanding/