LWN：简化BPF verifier！-技术圈

关注了就能看到更多这么棒的文章哦～

Simplifying the BPF verifier

By Daroc Alden
June 13, 2024
LSFMM+BPF
Gemini-1.5-flash translation
https://lwn.net/Articles/977815/

BPF 检验器 (BPF Verifier) 是一个复杂的程序。很不幸，这导致了相关的贡献者在开发它时更加困难，同时也更容易出现未知的 bug。Yu Shung-Hsi 在 2024 年的 Linux 存储、文件系统、内存管理和 BPF 峰会上提出了两个具体建议，旨在简化检验器，使其更容易维护。Yu 建议改变检验器中跟踪部分已知值的机制，并清理接口，以隐藏值跟踪器（value-tracker）内部表示的细节。

检验器的核心功能之一是值跟踪——推断变量可能持有的值的集合，以确保访问保持在边界内。由于任何值都可能用于计算数组索引或检验器感兴趣的其他内容，因此值跟踪器需要跟踪程序中的每个值。检验器在 bpf_reg_state 结构中存储有关可能值的的信息，该结构跟踪两种相关的信息。第一个是“已知位（known bits）”，它使用掩码来指示哪些 bit 的值是精确知道的：

struct tnum {
    u64 value;
    u64 mask;
}

第二个是值的有效范围，作为带符号和无符号的 32 位和 64 位量进行跟踪：

struct bpf_reg_state {
    ...
    struct tnum var_off;
    s64 smin_value; /* 最小可能 (s64) 值 */
    s64 smax_value; /* 最大可能 (s64) 值 */
    u64 umin_value; /* 最小可能 (u64) 值 */
    u64 umax_value; /* 最大可能 (u64) 值 */
    s32 s32_min_value; /* 最小可能 (s32) 值 */
    s32 s32_max_value; /* 最大可能 (s32) 值 */
    u32 u32_min_value; /* 最小可能 (u32) 值 */
    u32 u32_max_value; /* 最大可能 (u32) 值 */
}

选择要跟踪哪些信息，就代表了准确性和效率之间的权衡。如果计算机拥有过多的内存，检验器可以直接使用通用集合数据结构来跟踪可能值的集合。这种方法的缺点是与存储 bpf_reg_state 所需的字节相比，内存开销会显著增加。更有效方法的缺点是它不能表示所有可能的集合，因此有时代码需要进行保守的过近似（conservative over-approximation），这会像滚雪球一样，导致检验器无法找出理论上本可以找到的边界。例如，检验器当前无法处理不连续范围，例如必须介于 1 到 4 或 8 到 10 之间的值。相反，它会将范围跟踪为仅从 1 到 10。

在实践中，跟踪已知位和可能范围提供了良好的权衡。单独使用其中任何一个都无法捕获检验器关心的重要属性，但它们在一起的大小和复杂度并不太大，可以一起使用。它们可以表示可能的值集，例如“0 到 64 之间的 8 的倍数”，这非常适合跟踪数组访问的对齐和边界。

跟踪更少的边界值

Yu 提出了一项建议，可以在保持相同精度的情况下，显著简化 bpf_reg_state 的实际实现：不再专门跟踪带符号数的范围。现在，无论何时检验器更新一个范围（例如从条件分支推断新的 smin_value ），它都需要执行复杂的同步动作，以确保更改反映在每个范围内。Yu 说，目前，这种同步动作涉及在 20 个不同方向上传播信息。这是因为代码没有跟踪哪些字段已更新，因此在处理代码块后同步边界的过程中就需要把来自五个在跟踪的约束（四个范围和一个 tnum ）中的每一个的信息都共享给其他四个。

Yu 建议，不要以当前的方式跟踪范围，而是使用他在 2023 年 10 月讨论的方法的变体来跟踪范围。本质上，允许最大值小于最小值。以这种方式表示的范围始终从最小值开始，到最大值结束，但它可能会在途中环绕。这意味着范围（最小值：0xFFFFFFFC，最大值：4）表示带符号范围（-4, 4），同时表示/无符号/范围（0xFFFFFFFC, UINT32_MAX）和（0, 4）。现有代码不处理这样的不连续范围，因此 Yu 计划添加一些转换函数，将新的表示方式转换为旧代码使用。

以这种方式存储范围有一些好处。最大的好处是，无需同步带符号和无符号边界的信息——它们会自动同步，完全依靠表示方式本身。这也减少了检验器在已知位表示和范围表示之间需要传播的信息量，将代码减少到只有六个信息流方向（从三个边界中的每一个到另外两个）。Yu 希望这将使处理值跟踪的检验器代码更容易使用，也更容易正式验证。

Yu 计划分几个步骤将这些更改引入上游；最初，将实现转换函数，而主要的检验器代码将基本保持不变。然后，他计划更改数值跟踪代码中最关键的部分，原生使用新的表示方式，然后调整内核气动过程。最后，可以删除最后一处使用以及转换函数。

Yu 简化值跟踪器的第二个建议是为处理 tnum 和范围值引入一个更抽象的接口。这些建议可以独立实现，但它们肯定可以相互补充。Yu 说，现在，在检验器代码上工作需要了解 tnum 和范围的内部细节；但对这些值执行的最常见操作只是取交集或者包含检查。如果将它们提取到它们自己的函数中，那么实际的值跟踪代码的大部分可以大大简化。

然而，这些并不是简化检验器维护的唯一方法。会议以讨论如何改进文档、检验器的哪些方面可以标准化以及这些建议将如何影响正式验证而结束。检验器无疑已经因为它的难以维护而知名了，但似乎内核的 BPF 开发人员有一个计划来开始改变这种状况。

全文完
LWN 文章遵循 CC BY-SA 4.0 许可协议。

欢迎分享、转载及基于现有协议再创作～

长按下面二维码关注，关注 LWN 深度文章以及开源社区的各种新近言论～