【eBPF 内核实现深度拆解】验证器核心算法：抽象解释、状态跟踪与路径裁剪

Verifier 日志里有一条 16: (29) r0 &= 0xff，然后是 R0 min value is negative, ...。为什么 r0 &= 0xff 之后 R0 的 min value 不是 0？为什么 verifier 的 smin_value 和 umin_value 有时不一致？不理解 bpf_reg_state 的 tristate 值域跟踪，就只能猜测 verifier 的推理规则，无法系统性地写出被接受的高复杂度程序。

本文深入 verifier 的静态分析引擎：先讲抽象解释（abstract interpretation）的基本原理——为什么 verifier 跟踪的是类型和值域，而非具体值。然后逐层拆解 bpf_reg_state 的类型系统和 tristate（tristate = signed min/max + unsigned min/max）值域表示、bpf_verifier_state 的完整状态结构、do_check() 配合 pop_stack() 的 DFS 搜索策略、states_equal() 的等价判定条件，最后深入 propagate_precision() 的精度追踪机制。读完这篇，你理解 verifier 如何决定两个状态”等价”，以及在什么条件下搜索路径被裁剪。

一、抽象解释：为什么 verifier 不执行具体值

1.1 问题定义

考虑以下 BPF 程序：

int xdp_filter(struct xdp_md *ctx)
{
    void *data = (void *)(long)ctx->data;      // R1 = PTR_TO_PACKET
    void *data_end = (void *)(long)ctx->data_end;

    if (data + 4 > data_end)                   // 边界检查
        return XDP_DROP;

    __u32 key = *(u32 *)data;                  // 读取包的 4 字节
    ...
}

verifier 面临的问题是：在不实际运行程序、也不用具体网络包数据的情况下，证明 *(u32 *)data 的访问不会越界。如果 verifier 像 CPU 一样执行具体值，它需要遍历所有可能的输入（无限的包大小、所有可能的偏移），这在有限时间内是不可能的。

1.2 抽象解释的核心思想

抽象解释（Abstract interpretation）的核心思路是：不跟踪具体值，跟踪抽象值的属性集合。

具体执行：       data = 0xffff888010001000, data_end = 0xffff888010001100
抽象执行：       data ∈ [PTR_TO_PACKET, offset=0, range=[0, 0]]
                data_end ∈ [PTR_TO_PACKET, offset=0, range=[256, 256]]

verifier 为每个 bpf_reg 维护一个抽象状态，而非具体值。这个抽象状态包含：

1. 类型：寄存器是什么类型的指针（stack pointer, packet pointer, map value pointer…）
2. 值域：对于 scalar 值，跟踪有符号和无符号的最小/最大值范围（tristate）
3. 偏移：指针相对于基址的偏移
4. 引用追踪：是否指向一个被持有的引用（如 spinlock、refcount）

1.3 为什么必须是 over-approximation

verifier 的抽象解释必须是保守的 over-approximation——如果抽象状态允许某种行为，那么具体执行也必须允许；如果抽象状态禁止，具体执行也必须禁止。反过来不一定成立：抽象状态可能”多禁止”一些实际上安全的操作（这就是 verifier 的假阳性，false positive）。

以下是一个 over-approximation 导致 false positive 的经典场景：

// 实际永远为 true 的条件（来自更早的常量赋值），但 verifier 不知道
if (some_value < 0)
    return;
// some_value 在抽象状态下现在有 smin=0
// 但同时 umin 可能是 0, smax 可能是 0x7ffffff...
// 接下来：
if (some_value > 0xff)   // verifier 不能证明这分支不可能执行
    ...

verifier 对值的追踪是不完备的——它跟踪范围，不跟踪精确的等值关系。这导致某些安全路径被拒绝（第 04 篇详述）。

二、bpf_reg_state：寄存器抽象状态的类型系统

2.1 数据结构定义

struct bpf_reg_state（include/linux/bpf_verifier.h）定义了单个寄存器的所有抽象状态：

/* Linux 6.6: include/linux/bpf_verifier.h */
struct bpf_reg_state {
    /* 类型追踪 */
    enum bpf_reg_type type;
    
    /* 值域追踪（tristate） */
    struct tnum var_off;       /* 已知 bit / 未知 bit 的 tnum 结构 */
    s64 smin_value;            /* 有符号最小值 */
    s64 smax_value;            /* 有符号最大值 */
    u64 umin_value;            /* 无符号最小值 */
    u64 umax_value;            /* 无符号最大值 */
    s32 s32_min_value;         /* 32-bit 有符号最小值 */
    s32 s32_max_value;         /* 32-bit 有符号最大值 */
    u32 u32_min_value;         /* 32-bit 无符号最小值 */
    u32 u32_max_value;         /* 32-bit 无符号最大值 */
    
    /* 父指针：指向此寄存器从哪个父寄存器派生的（用于精度追踪） */
    u32 live;                  /* 寄存器活跃性标记 */
    
    /* 指针类型的额外信息 */
    u32 id;                    /* 唯一 ID（用于指针/引用追踪） */
    u32 ref_obj_id;            /* 引用对象 ID */
    
    /* 类型特定的字段（union） */
    struct {
        /* PTR_TO_MAP_VALUE / PTR_TO_STACK 等 */
        u32 map_uid;           /* map 唯一 ID */
        int off;               /* 相对于基址的偏移 */
        u32 range;             /* 已证明的范围 */
    };
    
    /* 对齐追踪 */
    u8 align;                  /* 已知对齐（2 的幂） */
    ...
};

2.2 寄存器类型分类

enum bpf_reg_type 定义了所有可能的寄存器类型。完整分类表：

类型的转换规则（verifier 在 adjust_ptr_min_max_vals() 和 adjust_scalar_min_max_vals() 中执行）：

• PTR_TO_STACK —（加/减常量）→ PTR_TO_STACK：产生新的指针，指向同一栈区域的合法范围。
• PTR_TO_PACKET —（加/减常量，须在边界检查后）→ PTR_TO_PACKET：产生新的包指针。
• SCALAR_VALUE —（任意计算）→ SCALAR_VALUE：对整数做算术，新值域由原始范围计算得到。
• PTR_TO_MAP_VALUE_OR_NULL —（检查 r == 0）→ PTR_TO_MAP_VALUE 或 SCALAR_VALUE：NULL 检查是唯一允许的转换。

禁止的转换（触发 "R%d pointer arithmetic on %s prohibited" 错误）：

• SCALAR_VALUE + 常量 → 任何指针类型（不能凭空造出指针）。
• PTR_TO_PACKET + 非零标量 → 禁止（只能加常量偏移，除非变量已被边界约束在合法范围内）。
• PTR_TO_MAP_VALUE + 超出 map value 大小的偏移 → 拒绝。

2.3 Tristate 值域：有符号 + 无符号 + bitmask

verifier 为 scalar 值维护三个维度的范围信息：

smin/smax：有符号范围。来自有符号比较（JSGT, JSGE, JSLT, JSLE）。

umin/umax：无符号范围。来自无符号比较（JGT, JGE, JLT, JLE）。

tnum (ternary number)：位级约束。tnum.value 记录已知的 bit，tnum.mask 记录未知的 bit。例如：

r0 &= 0xff:
  var_off.value = 0x00000000
  var_off.mask  = 0xffffff00  (高 24 bit 已知为 0，低 8 bit 未知)
  → umin=0, umax=0xff, smin=0, smax=0xff

tnum 允许 verifier 追踪位模式约束，例如 r0 &= 0x80 之后，verifier 知道第 7 bit 为 1（var_off.value = 0x80, var_off.mask = 0x7f）。这在使用位掩码判断 flag 时非常有用。

关键：signed 和 unsigned 范围独立更新，有时会不一致：

/* 假设 r0 初始化为 [smin=-2, smax=2, umin=0, umax=0xfffffffffffffffe] */
if (r0 > 1) ...  // 无符号比较 JGT 1
/* 在 fallthrough 分支中： */
/* umax = 1 (因为无符号 ≤ 1) */
/* smax = 2 仍然 [保留], smin = -2 [保留] */
/* 这导致 smin < umin —— 逻辑不一致但在 verifier 的建模中是合法的 */
/* 因为 signed 和 unsigned 追踪是独立的 */

这种独立性源于 verifier 不对有符号/无符号范围做交叉传播（这会成倍增加计算复杂度）。

三、bpf_verifier_state：程序的完整抽象状态

3.1 数据结构

struct bpf_verifier_state 定义了程序在一个执行点的完整抽象状态：

/* Linux 6.6: include/linux/bpf_verifier.h */
struct bpf_verifier_state {
    /* 寄存器状态：R0-R9 */
    struct bpf_reg_state regs[MAX_BPF_REG];  /* MAX_BPF_REG = 11 (R0-R10) */
    
    /* 栈状态：每个 8-byte 槽 */
    struct bpf_stack_state *stack;
    int allocated_stack;  /* 最大已使用的栈槽数 */
    
    /* 引用追踪 */
    u32 acquired_refs;     /* 已获取的引用计数 */
    struct bpf_reference_state *refs[BPF_MAX_REFS];
    
    /* 控制流 */
    u32 insn_idx;          /* 当前指令索引 */
    u32 prev_insn_idx;     /* 前一条指令索引 */
    
    /* 路径追踪 */
    u32 branches;          /* 经历的跳转分支数 */
    u32 depth;             /* 搜索深度 */
    
    /* 循环追踪 */
    u32 loop_depth;        /* 当前循环嵌套深度 */
    struct bpf_loop_inline_state active_loop;
    
    /* 搜索/裁剪 */
    u32 first_insn_idx;    /* 首次到达此状态的指令索引 */
    u32 last_insn_idx;     /* 最后使用的指令索引 */
    
    /* 子程序相关的寄存器状态（用于 caller/callee 合并） */
    struct bpf_func_state *frame[MAX_CALL_FRAMES];  /* 调用帧栈 */
    u32 curframe;          /* 当前帧索引 */
    
    /* 精度标记 */
    u32 jmp_history_cnt;   /* 跳转历史计数 */
    struct bpf_idx_pair *jmp_history;  /* 跳转历史数组 */
};

3.2 栈状态

每个 BPF 程序拥有 512 字节（MAX_BPF_STACK = 512）的栈空间。verifier 将栈划分为 8-byte 槽（共 64 个槽）并为每个槽跟踪状态：

/* Linux 6.6: include/linux/bpf_verifier.h */
struct bpf_stack_state {
    struct bpf_reg_state spilled_ptr;  /* 存储的指针类型/spill 状态 */
    u8 slot_type[BPF_REG_SIZE];        /* 每个 8-byte 槽的类型 */
};

enum bpf_stack_slot_type {
    STACK_INVALID,         /* 未初始化，不能读 */
    STACK_SPILL,           /* 保存的寄存器，包含被 spilling 的 reg_state */
    STACK_MISC,            /* 杂项数据（标量），值为零或不明的 */
    STACK_ZERO,            /* 显式的零值（用于 uninit 栈的初始化） */
};

栈槽访问示例：

// 将 R6 保存到栈
*(u64 *)(r10 - 8) = r6;
// verifier 将栈槽 [r10-8, r10) 标记为 STACK_SPILL，
// spilled_ptr = r6 的完整 bpf_reg_state

// 从栈恢复 R6
r6 = *(u64 *)(r10 - 8);
// 如果槽为 STACK_SPILL，r6 = spilled_ptr
// 如果槽为 STACK_INVALID，拒绝：不允许读未初始化的栈

栈槽的类型约束比寄存器更严格：任何时候只能有 8-byte 槽粒度的类型追踪。如果程序写入 4-byte 后读取 8-byte，verifier 会检测到槽类型不匹配（STACK_MISC + STACK_INVALID 混合）并拒绝。

3.3 状态快照和分支

当 check_cond_jmp_op() 遇到条件跳转时，verifier 创建当前状态的一个完整副本：

/* kernel/bpf/verifier.c - 状态 fork 简化流程 */
static int push_stack(struct bpf_verifier_env *env, int insn_idx, int prev_insn_idx)
{
    struct bpf_verifier_state *cur = env->cur_state;
    struct bpf_verifier_state *new;

    /* 分配新状态并深拷贝 */
    new = copy_verifier_state(cur);
    new->insn_idx = insn_idx;           /* 目标指令 */
    new->prev_insn_idx = prev_insn_idx;

    /* 加入 DFS 栈 */
    push_stack_state(env, new);
    return 0;
}

深拷贝的开销是 verifier 性能的主要瓶颈。在一次复杂的 XDP 程序验证中，copy_verifier_state() 可能被调用数千次。内核通过 states_equal() 的 pruning 来避免无限制的状态增长。

四、DFS 状态空间搜索：do_check() 与 pop_stack()

说明：内核 verifier 中没有独立的 explore_state() 函数。下文伪代码描述的逻辑实际分布在 do_check() 主循环与 pop_stack() / push_stack() 之间——用 explore_state() 命名仅为便于理解 DFS 语义。

4.1 DFS 搜索算法

verifier 使用 DFS（深度优先搜索）遍历程序的状态空间：

/* kernel/bpf/verifier.c — 逻辑等价于 do_check() + pop_stack() 的简化 */
static int explore_state(struct bpf_verifier_env *env, int insn_idx)
{
    while (true) {
        /* 在当前状态中执行指令 */
        err = do_check_insn(env, insn_idx);
        if (err)
            return err;

        /* 检查是否到达已探索状态（pruning） */
        if (states_equal(env, env->cur_state, explored)) {
            /* 当前状态被已探索状态覆盖，回溯 */
            if (!pop_stack(env, &insn_idx)) {
                /* 没有更多状态待探索 */
                break;
            }
            continue;
        }

        /* 到达叶子节点（EXIT 指令） */
        if (is_exit_insn(insn)) {
            /* 记录已探索状态 */
            save_explored_state(env, env->cur_state);
            if (!pop_stack(env, &insn_idx))
                break;
            continue;
        }

        /* 继续到下一条指令 */
        insn_idx = next_insn(env, insn_idx);
    }
    return 0;
}

DFS 栈的维护是通过 push_stack() 和 pop_stack() 管理的。当遇到条件跳转时，当前路径在 fallthrough 方向继续，分支路径被推入栈。当当前路径完成（到达 EXIT 或遇到已探索状态），verifier 弹出栈顶的状态，继续探索分支路径。

4.2 复杂度限制

verifier 对状态空间搜索有两个硬性限制：

这两个限制确保 verifier 在有限时间内返回结果。对于复杂程序（大量循环、多层嵌套条件），可能需要拆分或使用尾调用来规避（第 04 篇的 pattern 8）。

4.3 循环的特殊处理

循环是 verifier 面临的最困难的结构。对于每个循环迭代，寄存器的值域可能变化（例如循环计数器递增）。如果不加限制，verifier 会无限展开循环直到值域饱和或超出 BPF_COMPLEXITY_LIMIT_INSNS。

verifier 的处理策略：

对于 detected 循环：
  1. 记录每条指令的 loop_depth（check_cfg() 阶段确定）
  2. 在每次循环回边时检查 states_equal()
  3. 如果新状态被旧状态覆盖（值域是子集），停止循环展开
  4. 如果值域超出旧状态（例如 smin 更小），继续展开
  5. 达到复杂度上限时拒绝程序

这就是为什么循环必须在有限迭代内使值域收敛。例如：

for (int i = 0; i < 100; i++) {
    // i 从 [0,0] 到 [0,99]
    // 第 100 次迭代时被 i >= 100 的分支状态覆盖，停止展开
}

如果循环的上界不明显（例如基于 map 值的循环），verifier 无法确定迭代次数，会报告可能的无限循环并拒绝程序。

五、states_equal()：等价判定与路径裁剪

5.1 核心判定条件

states_equal() 是 verifier 路径裁剪的核心。它的判定逻辑是：如果当前状态的寄存器约束是已探索状态的超集（即更宽松），则当前状态可以被裁剪。

更精确地，两个状态 cur 和 old 被判定为等价（cur 被 old 覆盖）当：

1. 对于每个寄存器 R0–R10：
   • cur->regs[i].type == old->regs[i].type
   • cur->regs[i].smin >= old->regs[i].smin（cur 的有符号范围更窄）
   • cur->regs[i].smax <= old->regs[i].smax
   • cur->regs[i].umin >= old->regs[i].umin（cur 的无符号范围更窄）
   • cur->regs[i].umax <= old->regs[i].umax
   • regs_precision_match() 条件成立
2. 对于每个栈槽：
   • 槽类型相同（STACK_SPILL / STACK_MISC / STACK_ZERO）
   • 对于 STACK_SPILL，内嵌的 bpf_reg_state 满足上述寄存器等价条件
3. cur 的引用计数状态是 old 的子集。

关键洞察：如果 cur 的每个寄存器的类型与 old 相同且值域是 old 的子集，那么任何从 cur 可达的状态也从 old 可达。因此，不需要继续验证 cur 路径——old 路径已经覆盖了所有安全/不安全的可能性。

5.2 Pruning 的实际效果

考虑以下程序：

int result = 0;
if (packet_type == TYPE_A) {
    result = process_a(data);   // 路径 A
}
if (packet_type == TYPE_B) {
    result = process_b(data);   // 路径 B
}
// 合并点：在两种路径之后
return result;

执行过程： 1. verifier 先验证路径 A（packet_type == TYPE_A），到达合并点的状态 S_A。 2. verifier 回溯，验证路径 B（packet_type != TYPE_A && packet_type == TYPE_B），到达合并点时检查 states_equal(S_B, S_A)。 3. 如果 S_B 的寄存器约束被 S_A 覆盖（或反过来），pruning 发生——不需要继续验证相同的后缀路径。

但如果 process_a() 和 process_b() 对 result 产生了不同的值域（例如 result_a ∈ [0,10] vs result_b ∈ [0,100]），则 S_B 不会被 S_A 覆盖——verifier 必须继续验证两条路径的后缀。

六、精度追踪：propagate_precision() / __mark_chain_precision()

6.1 问题：过快裁剪导致的假阴性

假设验证过程中，states_equal(S_cur, S_old) 返回 false 因为 S_cur 的 R0 是 scalar，S_old 的 R0 也是 scalar，但 S_cur 的 smin 更小。这阻止了 pruning。但假如 R0 实际上从未用于控制流（例如它只是一个返回值）呢？

verifier 不应该因为”一个无关寄存器”的范围差异而拒绝 pruning。这就是 precision tracking 解决的问题。

6.2 精度追踪的工作原理

精度追踪（precision tracking）由 propagate_precision() 和 __mark_chain_precision() 两个核心函数实现。

基本流程：

1. 当 states_equal() 因为寄存器/栈槽差异而返回 false 时，verifier 检查差异的组件是否在当前或未来的路径中真的被使用。
2. 如果差异只存在于不会影响安全性的寄存器上（例如 callee-saved 但从未读取的 R8），verifier 可以标记该寄存器为不精确（imprecise），从而允许 pruning。
3. __mark_chain_precision() 执行回溯分析：从当前指令逆向追踪，找到哪些寄存器和栈槽需要精确跟踪，哪些可以放宽。
4. 如果差异涉及”精确所需”的寄存器，verifier 不能 pruning，必须继续探索。

精度标记函数：

/* kernel/bpf/verifier.c - __mark_chain_precision() 简化 */
static int __mark_chain_precision(struct bpf_verifier_env *env, int regno)
{
    /* 逆向遍历跳转历史，找到需要精确标记的指令 */
    for (i = state->jmp_history_cnt - 1; i >= 0; i--) {
        insn_idx = state->jmp_history[i].idx;
        prev_idx = state->jmp_history[i].prev_idx;

        /* 检查 insn_idx 处的指令是否"使用了"regno */
        /* 如果是，标记 prev_idx 处的对应寄存器需要精确 */
        if (insn_uses_reg(env->insn_aux_data[insn_idx], regno)) {
            err = mark_precise(env, prev_idx, regno);
            if (err)
                return err;
        }
    }
}

精度追踪的过程可能导致额外的验证轮次（pass）。第一轮验证标记了需要精确的寄存器，第二轮验证只对”需要精确”的寄存器做严格比较，允许”不需要精确”的寄存器有更宽松的约束。

6.3 精度等级

精度追踪将寄存器分为两个等级：

精度追踪是 verifier 实现”在精确性和效率之间权衡”的核心机制。没有它，即使是中等复杂度的 BPF 程序（30+ 条分支指令）也可能因状态爆炸而无法在时限内验证完成。

七、完整追踪示例

以下是一个简化的 BPF 程序的验证过程追踪：

SEC("xdp")
int simple_xdp(struct xdp_md *ctx)
{
    void *data = (void *)(long)ctx->data;          // 指令 0: R1 = PTR_TO_PACKET
    void *data_end = (void *)(long)ctx->data_end;   // R2 = PTR_TO_PACKET_END

    if (data + 4 > data_end)                         // 指令 1-2: 边界检查
        return XDP_DROP;                             // 指令 3-4: 路径 A: EXIT

    __u32 port;
    port = *(__u32 *)data;                           // 指令 5: LDX_W R3, [R1]

    if (port == 0x5000)                              // 指令 6: JEQ R3, 0x5000
        return XDP_PASS;                             // 指令 7-8: 路径 B: EXIT (R0=2)
    else
        return XDP_DROP;                             // 指令 9-10: 路径 C: EXIT (R0=1)
}

验证过程：

状态 S0 (入口，指令 0):
  R1=ptr_to_packet() R10=fp
  ↓ push_stack(路径A_branch → 指令 3)
  
状态 S1 (fallthrough after if, 指令 5):
  R1=ptr_to_packet(off=4, range=...)  R2=ptr_to_packet_end
  ↓ check_mem_access: data+4 在 data_end 范围内 → OK
  ↓ LDX_W R3 ← [R1], R3=scalar(umin=0, umax=0xffff)
  
状态 S2 (指令 6):
  R3=scalar(umin=0, umax=0xffff)
  ↓ check_cond_jmp_op: fork 状态 S2B (JEQ true) 和 S2C (JEQ false)
  
状态 S2B (分支方向, 指令 7):
  R3=scalar(umin=0x5000, umax=0x5000)  // 条件断言：port == 0x5000
  → EXIT with R0=2 → 记录已探索状态 S_exit_port_match
  
状态 S2C (fallthrough方向, 指令 9):
  R3=scalar(umin=0, umax=0xffff)  // 条件断言：port != 0x5000
  → EXIT with R0=1 → 记录已探索状态 S_exit_port_nomatch
  
pop_stack: 回溯到 S0 的 pushed 状态 (路径 A)
  
状态 S3 (路径 A, 指令 3):
  R1=ptr_to_packet(无有效范围), R2=ptr_to_packet_end
  data + 4 > data_end 条件成立
  → EXIT with R0=1 → 记录已探索状态 S_exit_oob

所有路径探索完毕，验证成功 ✓

在这个追踪中，关键步骤是： 1. 边界检查后的状态更新：R1 从一个 “unchecked PTR_TO_PACKET” 变成 “checked PTR_TO_PACKET with range”。 2. 条件跳转的 fork：一条路径中 port == 0x5000 被断言，另一条路径中 port != 0x5000 被断言。 3. 没有 pruning 机会（因为每个 EXIT 前的状态都不同）。

八、Mermaid：verifier 状态追踪流程图

flowchart TD
    START["入口状态初始化<br/>R1=PTR_TO_CTX<br/>R10=PTR_TO_STACK<br/>其他 R=NOT_INIT"]
    
    FETCH["取当前状态<br/>state = env->cur_state"]
    
    NEXT_INS["获取下一条指令<br/>insn = &insns[state->insn_idx]"]
    
    CHECK_LIMIT{"insn_processed<br/>&lt; 1,000,000?"}
    
    CLASSIFY{"指令类别<br/>BPF_CLASS(insn->code)"}
    
    ALU["check_alu_op()<br/>更新 dst_reg 的值域<br/>smin/smax/umin/umax/tnum"]
    MEM["check_mem_access()<br/>验证指针类型<br/>对齐、范围检查"]
    JMP["check_cond_jmp_op()<br/>fork 分支状态<br/>push 分支状态到栈"]
    CALL["check_helper_call()<br/>验证参数类型<br/>设置 R0 返回类型<br/>标记 R1-R5=NOT_INIT"]
    
    UPDATE["更新状态<br/>env->insn_processed++"]
    
    IS_EXIT{"到达 EXIT?"}
    
    PRUNE{"states_equal()<br/>当前状态 vs<br/>explored_states?"}
    
    SAVE["保存 explored state<br/>到哈希表"]
    
    POP{"pop_stack()<br/>有更多状态?"}
    
    PRECISE{"需要精度追踪?<br/>propagate_precision()"}
    
    MARK["__mark_chain_precision()<br/>逆向标记精确寄存器<br/>额外验证轮次"]
    
    ACCEPT["验证通过 ✓<br/>返回 0"]
    REJECT["验证失败 ✗<br/>返回错误码 + 日志"]
    TOO_LARGE["拒绝: 程序过大<br/>-E2BIG"]
    DONE["完成"]
    
    START --> FETCH --> NEXT_INS --> CHECK_LIMIT
    CHECK_LIMIT -->|是| CLASSIFY
    CHECK_LIMIT -->|超出| TOO_LARGE
    CLASSIFY --> ALU
    CLASSIFY --> MEM
    CLASSIFY --> JMP
    CLASSIFY --> CALL
    ALU --> UPDATE
    MEM --> UPDATE
    JMP --> UPDATE
    CALL --> UPDATE
    
    UPDATE --> IS_EXIT
    IS_EXIT -->|是| PRUNE
    IS_EXIT -->|否| NEXT_INS
    
    PRUNE -->|状态被覆盖| POP
    PRUNE -->|状态不匹配| PRECISE
    PRECISE -->|需要| MARK
    MARK --> NEXT_INS
    PRECISE -->|不需要| SAVE
    SAVE --> POP
    POP -->|是| NEXT_INS
    POP -->|否| ACCEPT

九、小结

verifier 的静态分析引擎通过三个核心机制保证程序和内核的安全：

1. 抽象解释：不执行具体值，而是跟踪类型（bpf_reg_type）和值域（smin/smax/umin/umax/tnum）。这避免了穷举所有可能的输入——代价是 over-approximation 导致的 false positive。

2. DFS 状态探索 + 等价裁剪：do_check() 配合 pop_stack() 按深度优先遍历程序的状态空间，states_equal() 判定两个状态的”覆盖”关系。如果当前状态的约束被已探索状态完全包含，路径被裁剪——这避免了组合爆炸。

3. 精度追踪：__mark_chain_precision() 识别哪些寄存器的精确范围真正影响安全性，允许”不精确的”寄存器有更宽松的约束。这使得 pruning 在更多场景中生效——但代价是可能需要进行额外的验证轮次。

这三个机制共同定义了 verifier 的安全边界和性能边界。下一篇文章将从这个理论出发，落地到实战中——解释常见拒绝模式的根因和正确的编程约束。

参考

内核源码（A 级，Linux 6.6）

• kernel/bpf/verifier.c — do_check()、pop_stack()、push_stack()、states_equal()、propagate_precision()、__mark_chain_precision()
• include/linux/bpf_verifier.h — struct bpf_reg_state、struct bpf_verifier_state
• kernel/bpf/syscall.c — bpf_prog_load() 入口

上一篇：验证器框架：从 BPF_PROG_LOAD 到 do_check()（第 02 篇）

下一篇：与验证器共舞：常见拒绝模式与编程约束（第 04 篇）