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

Verifier 日志里可能出现 r0 &= 0xff 之后仍报 min value is negative。为什么位掩码后 smin_value 与 umin_value 有时不同步？根因不在「猜规则」，而在 bpf_reg_state 如何把类型、区间（有符号/无符号 min/max）和 tnum（位级三元数）叠成一套抽象域——三者更新路径并不总是交叉约束。

系列分工

• 第 02 篇：bpf_check() 阶段划分、check_cfg()、do_check() 主循环入口、bpf_verifier_env 生命周期——框架与调用链。
• 本篇（第 03 篇）：bpf_reg_state 抽象域、bpf_func_state / bpf_verifier_state 分层、DFS 分支树与 is_state_visited() 裁剪、mark_chain_precision() 精度回溯——算法与数据结构。
• 第 04 篇：18 种常见拒绝模式、最小复现与正确写法——实战排障。

源码与运行环境基准：Linux 6.8.0-90-generic（本机内核）；结构体摘录自 /usr/src/linux-headers-6.8.0-90-generic/include/linux/bpf_verifier.h。下文函数名（do_check()、is_state_visited()、states_equal()、mark_chain_precision() 等）均指 kernel/bpf/verifier.c 中的实现，该文件不在 headers 包内，本篇不贴未核对的伪源码。

一、抽象解释：verifier 跟踪什么

1.1 问题：不能执行具体值

XDP 程序要在不触碰真实报文的前提下，证明 *(u32 *)data 不越界。若像 CPU 一样跟踪具体地址，输入空间无限，静态验证不可判定。Verifier 因此做抽象解释（abstract interpretation）：为每个寄存器维护抽象状态，在抽象域上模拟指令效果。

1.2 学术谱系：从 Cousot 到 Linux 与 PREVAIL

争论焦点（有文献）：PREVAIL（PLDI 2019）认为 Linux 的路径枚举 + 状态裁剪在分支增多时复杂度接近指数，循环支持也弱；Linux 维护者则通过 states_equal() 裁剪、mark_chain_precision() 精度回溯、bpf_loop 有界展开等工程手段把绝大多数生产程序压在可接受时间内。两种路线假设不同——PREVAIL 追求 fixpoint 多项式上界，Linux 接受「裁剪足够 aggressive 时路径仍可控」。截至 6.8，主线仍是后者。

1.3 Over-approximation 与假阳性

抽象解释必须是保守超近似（over-approximation）：抽象域允许的行为 ⊇ 具体执行。因此 verifier 可能拒绝实际安全的程序（假阳性/false positive），第 04 篇从日志措辞反推这类情况。区间域不跟踪等价关系、有符号与无符号区间独立维护（见第二节），是假阳性的常见来源之一。

二、bpf_reg_state：单寄存器抽象域

2.1 数据结构（Linux 6.8 摘录）

路径：include/linux/bpf_verifier.h。头文件注释写明字段顺序与 states_equal() 相关，删减仅保留核心字段：

/* Linux 6.8: include/linux/bpf_verifier.h — struct bpf_reg_state（节选） */
struct bpf_reg_state {
    enum bpf_reg_type type;
    s32 off;
    union {
        int range;                    /* PTR_TO_PACKET */
        struct {
            struct bpf_map *map_ptr;
            u32 map_uid;
        };                            /* map 指针 */
        struct {
            struct btf *btf;
            u32 btf_id;
        };                            /* PTR_TO_BTF_ID */
        struct {
            u32 mem_size;
            u32 dynptr_id;
        };                            /* PTR_TO_MEM | PTR_TO_MEM_OR_NULL */
        /* ... dynptr、iter、raw 等分支见头文件 ... */
        u32 subprogno;                /* PTR_TO_FUNC */
    };
    struct tnum var_off;              /* 标量值或指针可变偏移 */
    s64 smin_value, smax_value;
    u64 umin_value, umax_value;
    s32 s32_min_value, s32_max_value;
    u32 u32_min_value, u32_max_value;
    u32 id;
    u32 ref_obj_id;
    struct bpf_reg_state *parent;     /* 活性/精度回溯链 */
    u32 frameno;
    s32 subreg_def;
    enum bpf_reg_liveness live;
    bool precise;                     /* false 时标量 min/max 可不参与安全判定 */
};

不存在于头文件的字段（旧文误写，此处纠正）：u8 align、map_uid 与 off 平级、range 作为通用字段等——真实布局见上方 union。

tnum 定义在 include/linux/tnum.h：value 为已知位，mask 为未知位（注释称 tracked/tristate numbers）。CGO 2022 论文形式化了该域上加减乘的 soundness。

2.2 类型与转换（概要）

enum bpf_reg_type 在 include/uapi/linux/bpf.h 定义。Verifier 在 check_alu_op()、adjust_ptr_min_max_vals() 等路径上维护类型不变量。核心约束举例：

• 标量不能经算术「变成」指针；
• PTR_TO_MAP_VALUE_OR_NULL 判空前不得解引用；
• 包指针 PTR_TO_PACKET 的 range 字段记录已证明的可访问字节数（日志里常写作 r=）。

完整类型表与转换规则见第 04 篇模式索引；本篇只强调：类型与值域在 bpf_reg_state 同一结构里绑定，states_equal() 两者都查。

2.3 三套值域：smin/smax、umin/umax、tnum

三者独立更新，verifier 不做 smin/umin 的全局交叉传播（否则状态空间膨胀）。因此可能出现 umin=0 而 smin<0 的抽象状态——在抽象解释语义下合法，但会导致有符号分支上保守拒绝。位运算后若需有符号推理，通常要配合显式范围收窄（第 04 篇相关模式）。

三、分层状态：bpf_func_state 与 bpf_verifier_state

3.1 关键纠正：regs[] 在哪

regs[MAX_BPF_REG] 在 struct bpf_func_state，不在 struct bpf_verifier_state。 访问当前帧寄存器的内联 helper：

/* Linux 6.8: include/linux/bpf_verifier.h */
static inline struct bpf_reg_state *cur_regs(struct bpf_verifier_env *env)
{
    return cur_func(env)->regs;
}

3.2 bpf_func_state（函数/调用帧）

/* Linux 6.8: include/linux/bpf_verifier.h — struct bpf_func_state（节选） */
struct bpf_func_state {
    struct bpf_reg_state regs[MAX_BPF_REG];
    int callsite;
    u32 frameno, subprogno;
    u32 async_entry_cnt;
    struct bpf_retval_range callback_ret_range;
    bool in_callback_fn;
    bool in_async_callback_fn;
    bool in_exception_callback_fn;
    u32 callback_depth;
    int acquired_refs;
    struct bpf_reference_state *refs;
    struct bpf_stack_state *stack;
    int allocated_stack;
};

栈按 8 字节槽跟踪：

struct bpf_stack_state {
    struct bpf_reg_state spilled_ptr;
    u8 slot_type[BPF_REG_SIZE];
};

enum bpf_stack_slot_type {
    STACK_INVALID, STACK_SPILL, STACK_MISC, STACK_ZERO,
    STACK_DYNPTR, STACK_ITER,
};

MAX_BPF_STACK = 512（include/linux/filter.h），共 64 槽。Spill 时整槽复制 bpf_reg_state；读未初始化槽（STACK_INVALID）拒绝。

3.3 bpf_verifier_state（控制流搜索节点）

/* Linux 6.8: include/linux/bpf_verifier.h — struct bpf_verifier_state（节选） */
#define MAX_CALL_FRAMES 8

struct bpf_verifier_state {
    struct bpf_func_state *frame[MAX_CALL_FRAMES];
    struct bpf_verifier_state *parent;
    u32 branches;
    u32 insn_idx;
    u32 curframe;
    struct bpf_active_lock active_lock;
    bool speculative;
    bool active_rcu_lock;
    bool used_as_loop_entry;
    u32 first_insn_idx, last_insn_idx;
    struct bpf_verifier_state *loop_entry;
    struct bpf_jmp_history_entry *jmp_history;
    u32 jmp_history_cnt;
    u32 dfs_depth;
    u32 callback_unroll_depth;
};

branches 字段注释（同文件 373–416 行）说明 DFS 树如何计数待探索分支，以及 is_state_visited() 如何据此检测循环——这是理解裁剪与循环判定的第一手说明。

explored_states 哈希表挂在 bpf_verifier_env 上（struct bpf_verifier_state_list 链表节点），不在 bpf_verifier_state 内。

3.4 状态快照与分支

条件跳转时 verifier 复制当前 bpf_verifier_state（含各 frame 深拷贝），一条路径 fallthrough 继续，另一条 push_stack() 延后探索。深拷贝成本是验证耗时的主要来源之一；裁剪与精度标记旨在压低 peak_states（见 bpf_verifier_env.peak_states）。

四、DFS 搜索与复杂度预算

4.1 算法轮廓

第 02 篇已描述 do_check() 主循环。本篇补充语义：

1. 从入口 bpf_func_state 初始化 R1=PTR_TO_CTX、R10=PTR_TO_STACK、其余 NOT_INIT（02 篇亦有述）。
2. 顺序模拟指令，更新 cur_regs() 与当前帧栈。
3. 条件跳转：fork 状态、更新分支断言（如 JEQ taken 分支将 R1 收窄为常数）。
4. 到达汇合点或 bpf_exit：调用 is_state_visited()；若当前抽象状态被历史状态覆盖，则裁剪。
5. 栈空且所有分支 branches==0：验证成功。

内核中没有名为 explore_state() 的函数；DFS 语义分布在 do_check()、push_stack()、pop_stack() 之间。

4.2 复杂度限制（可核对常量）

实测日志末尾可见统计行，例如 processed 13 insns (limit 1000000) ... peak_states 1（见第七节）。

4.3 循环

循环回边触发 is_state_visited()：若新状态抽象域不宽于已访问状态，停止展开；若变宽则继续直到饱和或触达复杂度上限。上界明显的 for (i = 0; i < N; i++) 可在有限步收敛；上界依赖运行时数据（如 map 值）时常被拒绝。

五、states_equal() 与路径裁剪

5.1 覆盖关系

is_state_visited() 在汇合点查询 explored_states。核心判定由 states_equal()（及栈/spill 比较、regs_precision_match()）完成，语义是：

若当前状态 \(s\) 的每个寄存器/栈槽约束不比已存状态 \(t\) 更宽（类型相同，标量区间是子集，指针 range 更小等），则 \(s\) 可达行为 ⊆ \(t\) 已分析行为，可安全裁剪。

形式化：对标量，\([\text{smin}_s,\text{smax}_s] \subseteq [\text{smin}_t,\text{smax}_t]\) 且 umin/umax 同理。注意「更窄区间 ⇒ 更强约束 ⇒ 可被覆盖」——与直觉上「状态相等」不同，这是偏序下的 subsume，不是字节级相同。

5.2 活性标记

enum bpf_reg_liveness（REG_LIVE_READ、REG_LIVE_WRITTEN 等）与 parent 链配合：mark_reg_read() 向上传播「此寄存器影响安全性」；写标记阻断传播。这决定 states_equal() 是否必须比较某个寄存器的 min/max。

5.3 裁剪示例（概念）

两条分支在汇合点若 R0 分别为 \([0,10]\) 与 \([0,100]\)，则互不覆盖，汇合点后缀需分别验证；若均为 PTR_TO_PACKET 且 range 已证明足够，则常可裁剪其一。

六、精度追踪：precise 与 mark_chain_precision()

6.1 动机

若仅因不影响内存安全的 callee-saved 寄存器区间差异就阻止裁剪，会导致 peak_states 无谓升高。bpf_reg_state.precise 标记：为 false 时，标量 min/max/tnum 可不参与安全等价判定（头文件 226–227 行注释）。

6.2 机制

1. states_equal() 因某寄存器差异返回 false；
2. propagate_precision() / mark_chain_precision() 沿 jmp_history 反向查看该寄存器是否在控制流/内存访问中实质使用；
3. 未影响安全性的寄存器设 precise=false，允许后续裁剪；
4. 必要时 env->pass_cnt 增加，触发额外验证轮次。

这是 Linux 在「路径枚举」框架内逼近 PREVAIL 式「忽略无关维度」的工程折中。

七、实测 verifier 日志解读

7.1 实验环境与方法

测试程序（XDP）：

/* 用户态 C — 非内核源码；由 BCC 编译为 BPF_PROG_TYPE_XDP */
int xdp_pass(struct xdp_md *ctx) {
    void *data = (void *)(long)ctx->data;
    void *data_end = (void *)(long)ctx->data_end;
    if (data + 4 > data_end)
        return XDP_DROP;
    __u32 port = *(__u32 *)data;
    if (port == 0x5000)
        return XDP_PASS;
    return XDP_DROP;
}

7.2 验证通过：寄存器状态逐指令跟踪

以下输出来自本机真实加载（经删减空行；完整统计行保留）：

0: R1=ctx() R10=fp0
0: (b7) r0 = 1                        ; R0_w=1
1: (61) r2 = *(u32 *)(r1 +4)          ; R1=ctx() R2_w=pkt_end()
2: (61) r1 = *(u32 *)(r1 +0)          ; R1_w=pkt(r=0)
3: (bf) r3 = r1                       ; R1_w=pkt(r=0) R3_w=pkt(r=0)
4: (07) r3 += 4                       ; R3_w=pkt(off=4,r=0)
5: (2d) if r3 > r2 goto pc+4          ; R2_w=pkt_end() R3_w=pkt(off=4,r=4)
6: (61) r1 = *(u32 *)(r1 +0)          ; R1_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
7: (b7) r0 = 2                        ; R0_w=2
8: (15) if r1 == 0x5000 goto pc+1     ; R1_w=scalar(...)
9: (b7) r0 = 1                        ; R0=1
10: (95) exit

from 8 to 10: safe
from 5 to 10: safe
processed 13 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1

解读要点：

1. 指令 2–5：从 ctx 加载 data/data_end，比较 data+4 与 data_end。Fallthrough 路径上指令 5 处 R3_w=pkt(off=4,r=4)——r=4 表示已证明 4 字节包内访问合法。
2. 指令 6：Load 后 R1 变为 scalar，tnum 显示 32 位未知（读包前 4 字节）。
3. 指令 8 分支：from 8 to 10: safe 表示 JEQ 的 fallthrough 路径可达 exit；taken 路径在省略行中返回 R0=2。
4. 指令 5 taken 路径（goto pc+4）：越界分支直接 XDP_DROP，日志中 from 5 to 10: safe 涵盖该路径可达 exit 的判定。
5. 统计：仅 1 个 peak state，说明此小程序未触发状态爆炸。

7.3 验证失败：缺少边界检查

对照组去掉 data_end 检查：

0: R1=ctx() R10=fp0
0: (61) r1 = *(u32 *)(r1 +0)          ; R1_w=pkt(r=0)
1: (61) r1 = *(u32 *)(r1 +0)
invalid access to packet, off=0 size=4, R1(id=0,off=0,r=0)
R1 offset is outside of the packet
processed 2 insns (limit 1000000) max_states_per_insn 0 total_states 0 peak_states 0 mark_read 0

r=0 表示未证明任何包内字节可访问——与第 04 篇「边界检查后 range 才非零」的模式一致。读日志应自底向上：先锁定错误行，再向上追溯 R1 的类型与 range 何时丢失。

八、Verifier 主循环（流程图）

flowchart TD
    START["Init entry state<br/>R1=PTR_TO_CTX R10=PTR_TO_STACK"]
    FETCH["cur_state = env->cur_state<br/>cur_regs = frame[curframe]->regs"]
    NEXT["insn = insns[state->insn_idx]"]
    LIMIT{"insn_processed<br/>&lt; 1M?"}
    CLASS{"BPF_CLASS(insn)"}
    ALU["check_alu_op()"]
    MEM["check_mem_access()"]
    JMP["check_cond_jmp_op()<br/>fork + push_stack()"]
    CALL["check_helper_call()"]
    UPD["insn_processed++"]
    EXIT{"bpf_exit?"}
    VISIT{"is_state_visited()<br/>subsumed?"}
    POP{"pop_stack()?"}
    PREC["mark_chain_precision()<br/>extra pass if needed"]
    OK["return 0"]
    ERR["return -errno + log"]
    BIG["-E2BIG too large"]

    START --> FETCH --> NEXT --> LIMIT
    LIMIT -->|yes| CLASS
    LIMIT -->|no| BIG
    CLASS --> ALU & MEM & JMP & CALL
    ALU & MEM & JMP & CALL --> UPD --> EXIT
    EXIT -->|no| NEXT
    EXIT -->|yes| VISIT
    VISIT -->|yes| POP
    VISIT -->|no| PREC
    PREC --> POP
    POP -->|yes| NEXT
    POP -->|no| OK

九、小结与开放问题

Verifier 静态引擎的三根支柱：

1. 抽象域：bpf_reg_state 上的类型 + 双区间 + tnum（Cousot 框架在 Linux 上的特化；tnum 见 CGO 2022）。
2. DFS + 子序裁剪：bpf_verifier_state.branches 管理探索树；is_state_visited() / states_equal() 在偏序下 subsumption。
3. 精度回溯：precise 与 mark_chain_precision() 避免无关寄存器阻止裁剪。

开放问题

1. 路径枚举 vs 抽象 fixpoint 会否收敛到同一设计？ PREVAIL（PLDI 2019）与 Linux 6.8 主线仍分道扬镳；随着 bpf_loop、open-coded iterator、kfunc 增加，Linux 裁剪启发式能否继续扩展而不重写为 fixpoint——尚无社区共识，需跟踪 verifier.c 重构讨论与 Windows/Linux 验证器行为 diff。
2. Verifier 自身正确性：Vishwanathan et al.（CGO 2022）只形式化了 tnum 算子；states_equal()、指针别名、ref_obj_id 释放规则的全局 soundness 仍靠测试与 Agni 等后续工作（Rutgers 团队）逐步覆盖——生产 verifier 的「可证安全」与「实际安全」之间仍有工程间隙。

下一篇：与验证器共舞：常见拒绝模式与编程约束（第 04 篇）——从本篇的抽象域与裁剪语义出发，对照真实拒绝日志给出可操作的写法。

参考资料

规范与头文件（A 级，Linux 6.8.0-90-generic）

• include/linux/bpf_verifier.h — struct bpf_reg_state、bpf_func_state、bpf_verifier_state、enum bpf_reg_liveness
• include/linux/tnum.h — struct tnum 语义与算术
• include/linux/bpf.h — BPF_COMPLEXITY_LIMIT_INSNS
• include/linux/filter.h — MAX_BPF_STACK

内核实现（A 级，路径指 Linux 6.8 主线）

• kernel/bpf/verifier.c — do_check()、push_stack() / pop_stack()、is_state_visited()、states_equal()、propagate_precision()、mark_chain_precision()
• kernel/bpf/syscall.c — bpf_prog_load() → bpf_check()

论文

• Patrick Cousot & Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977.
• Elazar Gershuni et al. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions. PLDI 2019.（PREVAIL；路径枚举 vs zones fixpoint）
• Harishankar Vishwanathan et al. Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers. CGO 2022.

实验（A 级，本机）

• 环境：Linux 6.8.0-90-generic，BCC 0.29.1，bpftool v7.4，root 加载
• 方法：BPF(text=..., debug=0x12) 获取 log_level=2 寄存器状态跟踪（第七节原文）

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

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