Linux Kernel/BPF verifier / 控制流图检查

用显式栈遍历 BPF 控制流

Linux BPF 验证器的 check_cfg 使用显式指令栈执行非递归 DFS，检查跳转目标、可达性及控制流结构。

v6.12图处理与编译核验 2026-10-08

工程问题#

待验证程序的跳转会形成有向图；遍历必须区分尚未探索和已完成的指令，同时避免深调用链消耗内核 C 调用栈。

实际实现#

insn_stack 数组保存当前探索路径，cur_stack 指向栈顶之后。push_insn 将未发现目标压栈；当前指令的边探索完成后，标记 EXPLORED 并弹栈。

处理流程#

分配指令状态数组与显式栈。
将入口指令标为已发现并压栈。
访问栈顶指令，继续探索未访问后继。
后继处理完毕后弹栈，并检查未遍历指令。

源码片段#

固定版本 · 原文摘录

kernel/bpf/verifier.cv6.12 · L16515–L16534

查看原文件

16515walk_cfg:16516	while (env->cfg.cur_stack > 0) {16517		int t = insn_stack[env->cfg.cur_stack - 1];1651816519		ret = visit_insn(t, env);16520		switch (ret) {16521		case DONE_EXPLORING:16522			insn_state[t] = EXPLORED;16523			env->cfg.cur_stack--;16524			break;16525		case KEEP_EXPLORING:16526			break;16527		default:16528			if (ret > 0) {16529				verbose(env, "visit_insn internal bug\n");16530				ret = -EFAULT;16531			}16532			goto err_free;16533		}16534	}

check_cfg

用 cur_stack - 1 读取栈顶；visit_insn 若发现新分支则继续深入，返回 DONE_EXPLORING 时标记完成并递减栈指针。这是源码明确声明的非递归深度优先遍历，错误跳转也在该遍历中向上传递。

CGPL-2.0-only（文件头 SPDX）

连续片段展示取栈顶与完成后的弹栈；压栈发生在 visit_insn 调用链中的 push_insn。片段外还有异常回调入口及不可达指令检查。

收益与取舍#

工程分析

带来的收益

显式管理遍历深度，不依赖递归调用栈。
访问状态用于区分树边、回边和已完成分支。

付出的代价

按指令数量分配辅助数组，额外占用内存。
结构检查不能独立证明内存访问安全或循环终止。

可比较的选择

递归 DFS写法更接近图遍历定义，但深路径会消耗内核调用栈。

版本与适用范围#

这里是验证器工作栈，不是 BPF 程序的运行时栈。v6.12 的回边处理受 bpf_capable 等规则影响，不能描述为全面禁止循环。

参考来源#

源码、官方文档与原始论文

Linux v6.12：非递归控制流 DFS

kernel/bpf/verifier.c · check_cfg

源码v6.12

Linux v6.12：压栈与回边处理

kernel/bpf/verifier.c · push_insn