5.1 验证器核心逻辑与常见拒绝


5.1 验证器核心逻辑与常见拒绝

本节摘要:验证器对每条路径做抽象解释:寄存器是标量还是指向 Map、栈、上下文的指针,偏移是否仍在对象内,Helper 参数是否符合契约。常见拒绝不是“内核心情不好”,而是未初始化、分支后状态合流失败、循环看不出上界、路径数爆炸。读日志要比改随机 pragma 有效。

先说结论

阅读完本节,你应当能够:

  1. 用“抽象状态沿控制流走”一句话描述验证器
  2. 识别至少五类常见拒绝及其改法
  3. 说明为什么 lookup 后必须判空才能用指针
  4. 在“拆程序”和“展开循环”之间选择成本更低的路

第 2 章把验证器比成海关 X 光机。现在看它实际照什么。它不执行你的业务输入,它假设最坏输入,问最坏情况下会不会越界。

一、它走路的方式

先把字节码建成控制流图。再从入口开始,给每个寄存器一个抽象值:未初始化、标量范围、指向某 Map 值、指向栈上某槽、指向上下文。每执行一条指令,状态更新。遇到条件跳转,状态分叉,两边都要走完。

合流很难。if 两边对同一个寄存器留下不同的“可能是指针也可能是标量”,后面再用,验证器可能直接认输。你觉得“到这里肯定是指针”,它没有看到证明。证明必须出现在字节码里:一次成功的 lookup、一次明确的空指针分支、一次对长度的比较。

循环是另一场战争。它需要看见迭代次数的上界,或者你把循环展开成直线。哈希表“遍历到空为止”在用户态很普通,在这里常常不可证明。于是你改成有界次数,或把聚合挪到写入时。

二、常见拒绝翻译

未初始化读。 寄存器或栈槽没写过就用。C 里未初始化局部变量,编译器未必当错误,验证器当错误。改法:定义时清零。

lookup 后未判空。 Map 查找失败返回空。你必须 if (p) 再读 p->field。验证器靠这个分支把指针从“可能空”变成“非空”。

指针运算超出对象。 你把包指针加了一个验证器看不懂的变量偏移。改法:先比较长度,偏移用立即数或被卡住范围的变量。

Helper 参数类型不对。 该传栈上 key,你传了寄存器里的标量;该传某程序类型的上下文,你传了别的。看 Helper 契约,不要凭用户态直觉。

调用栈与指令数超限。 函数嵌套、展开后指令太多。拆成尾调用或把逻辑送回用户态,见第 7 章。

路径爆炸。 太多分支,状态数打到上限。表现是日志又长又像胡话。改法:减少输入形状、合并分支、拆成多个小程序。

拒绝类型 日志里常出现的意思 优先改法
未初始化 读了未知值 清零;写满结构体
空指针 解引用可能为空 lookup 后分支
越界 偏移或大小不可证 先比长度;用有界下标
Helper 契约 参数类型或大小不对 对照该程序类型的允许列表
无限循环嫌疑 回边无上界 有界循环或展开
路径过多 状态数打满 拆程序、减分支
泄露或类型混淆 指针当标量用 不要把指针值存进随意整数再转回

建筑结构监测仪只允许贴在承重柱的指定点。你把传感器伸进墙里未知空洞,监理会直接停工——不是因为传感器坏了,是因为伸进去的长度无法事先证明安全。验证器就是那位监理。

⚠️ 常见坑:为了过验证把指针 cast 成整数再 cast 回来。这会让类型信息丢失,拒绝变得更怪,有时还会绕过你自己都看不懂的检查,绝不能当技巧。
💡 关键直觉:验证器只相信它跟踪过的类型。你要让它看见“这是 Map 值指针”,而不是在心里知道。

三、工程上怎么跟它合作

从能过的最小程序长出来。 先挂空函数返回 0,再加计数,再加 lookup,再加字段。哪一步炸,哪一步就是问题。对着两千行日志猜,效率极低。

把复杂解析放到用户态。 内核里只留长度检查和拷贝固定头。七层协议状态机是路径爆炸冠军。

读日志从最后一次违规往回看。 前面大量“状态”是面包屑。最后那条指令号对应到源码(有行号映射时),比从头读有效。

接受表达力上限。 有些合法算法就是证明不了。这不是你水平不够,是这套安全模型的价格。换数据结构和有界循环,或换回用户态。

/* 概念性:验证器要求的形状 */ val = bpf_map_lookup_elem(&m, &key); if (!val) return 0; /* 过了这分支,val 才是可解引用的 Map 值指针 */ val->count += 1;

图:抽象状态如何把“心里知道”变成“纸面证明”

图:抽象状态如何把“心里知道”变成“纸面证明”

问题:验证通过是否意味没有 Spectre 一类问题?

不是同一层。验证器管的是 eBPF 安全模型里的内存与终止。CPU 推测执行是另一战场,内核会用推测屏障等手段缓解。不要把“加载成功”理解成侧信道免疫。

问题:为什么同样逻辑在 bcc 能过、在 libbpf 不过?

编译器版本、优化、内联、是否生成 BTF,都会改变字节码形状。不是验证器针对框架有偏见。把中间字节码 dump 出来对比,比争论框架更好。

四、把验证日志读成代码评审意见

验证日志看起来像寄存器转储,其实可以当评审意见读。最后一条违规指出“哪条指令、哪种状态不合法”。往前翻,看该寄存器的类型从哪条指令开始变成未知。未知往往来自一次 Helper 返回、一次你没判空的指针、一次把指针当标量加完又当指针用。把这三段标回源码,修改通常只涉及一个分支。

路径爆炸的日志则是另一种声音:它在说输入形状太多。包解析里每个可选头都是形状。减形状的方法是限制“我们声称支持的最浅子集”,而不是让验证器陪你走完协议的全部排列。能声明“最多两个扩展头”,就不要在注释里写“完整支持 IPv6”。

与编译优化的互动很烦。同一份 C,O2 可能把分支合并成验证器更难看懂的形式,也可能消掉你需要的判空。若某次优化后突然拒绝,比较未优化字节码,而不是先改逻辑。必要时对热函数关激进内联。这是构建问题,不是安全模型故意针对你。

把常见拒绝做成内部卡片:未初始化、未判空、越界、Helper 契约、循环、路径过多。新人提交加载失败时先自己对卡片,再找人看。卡片比口头“验证器就是很烦”更能积累组织知识。验证器的脾气稳定,变的是我们是否学会用它的语言说话。

不要在生产节点上对着验证日志现场改。日志里可能带有内核内部细节,循环试错会把节点当编译器。把对象和日志带回 CI 的对应内核,修到绿再发。这和第 8 章的“节点不编译”是同一条纪律在验证期的投影。

现场笔记:为了过验证把指针来回转换

有人把 Map 值指针转成整数存起来,过会儿再转回指针,本地偶然能过,换编译器优化后变成更怪的拒绝,有一次甚至让审查者看不懂意图。后来明确禁止这类写法。类型信息断了,验证器要么拒绝,要么你自己也不知道它在证明什么。证明必须可读,才配进生产。

路径爆炸出现在一份想完整解析某种封装协议的程序上。每加一个可选头,状态数翻倍。最后声明只支持最浅两层,更深的走慢路径。产品经理不喜欢“不完整”,但完整的不可加载程序对用户是零。能加载的子集,比不能加载的全集有用。

把拒绝卡片贴进代码评审。新人加载失败先对卡片再找人。一周后重复问题明显下降。验证器脾气稳定,组织学习曲线不稳。卡片是把稳定的脾气翻译成人话。人话可以传承,寄存器转储传承不了。

延伸讨论:可读的证明才配进生产

指针来回转换让类型信息断裂,审查者看不懂你在证明什么。禁止。路径爆炸时声明最浅子集,能加载的子集比不能加载的全集有用。优化级别改变字节码形状,突然拒绝时先对比未优化产物,再改逻辑。把拒绝卡片用于评审,新人先对卡片。验证器脾气稳,组织学习不稳,卡片是翻译器。生产节点不对着日志现场改,带回 CI 对应内核。节点当编译器用,会把现场改脏,也会把内核内部细节打进不该去的日志系统。脏现场让第 8 章的对照实验失效。失效之后你无法证明是验证问题还是业务问题。不能证明的修复,不是修复,是另一次加载。另一次加载可能碰巧通过,碰巧不能当方法。方法是最小程序生长:空函数、计数、lookup、字段,一步一证。

对照清单

  1. 从日志最后一条违规往回找类型从哪变成未知,修改通常只涉及一个分支。
  2. lookup 后判空、比长度、有界循环,证明必须出现在字节码里不是心里。
  3. 路径爆炸时减输入形状,声明最浅子集,能加载的子集比不能加载的全集有用。
  4. 禁止把指针和整数来回转换,类型断了审查者也不知道你在证明什么。
  5. 优化级别会改变形状,突然拒绝先对比未优化字节码再改逻辑。
  6. 生产不对着验证日志循环试 pragma,带回 CI 对应内核修到绿。
  7. 最小程序生长是最高效过验证策略,对着两千行日志猜效率极低。
  8. 有些合法算法就是证明不了,换结构或回用户态,不要堆到不可维护。
  9. 同一逻辑在不同框架下字节码不同,不是验证器针对框架有偏见。
  10. 验证通过不是 Spectre 免疫,也不是计数正确,两件事另审。
  11. 拒绝卡片给新人用,组织学习曲线靠卡片而不是靠口头很烦。
  12. 寄存器职责单一,几乎像在写强类型汇编,混用会在合流处被拒绝。

要点速记

  • 验证器做抽象解释:跟踪类型与范围,不是跑单元测试。
  • 证明必须写在代码里:判空、比长度、有界循环。
  • 路径爆炸是真实上限:拆程序比堆 pragma 更可持续。
  • 不要用整数来回转换指针来“骗过”类型系统。
  • 最小程序生长法是最高效的过验证策略。
  • 有些合法算法证明不了:这是模型价格,换结构或换回用户态。

下一节看第二道约束:即便可证明安全,内存、指令和时间仍然记账,防止合法程序拖垮内核。


作者与出处
原作者: 灏天文库
来源:灏天文库
整理: 灏天文库整理
由灏天文库平台收录,内容或由平台用户上传,仅供学习交流
发布者: 作者: 灏天文库 转发
评论区 (0)
U