The BPF verifier works, on a theoretical level, by considering every possible path that a BPF program could take. As a practical matter, however, it needs to do that in a reasonable amount of time. At the 2025 Linux Plumbers Conference, Mahé Tardy and Paul Chaignon gave a detailed explanation (slides; video) of the main mechanism that it uses to accomplish that: state pruning. They focused on two optimizations that help reduce the number of paths the verifier needs to check, and discussed some of the complications the optimizations introduced to the verifier's code.
从理论上讲,BPF 验证器(verifier)的工作方式是考虑一个 BPF 程序可能执行的所有路径。但在实际中,它必须在合理的时间内完成这项工作。在 2025 年的 Linux Plumbers Conference 上,Mahé Tardy 和 Paul Chaignon 对其实现这一目标的核心机制——状态剪枝(state pruning)——进行了详细讲解(配有幻灯片和视频)。他们重点介绍了两种用于减少验证器需要检查的路径数量的优化方法,并讨论了这些优化给验证器代码带来的一些复杂性。
Tardy began by giving an example of the simplest kind of branching control flow: a program with a single if statement in it. This program has two potential execution paths. Adding another (non-nested) if statement makes it four, then eight, and by the time one reaches a realistic program, the number of possible paths is completely intractable. Sometimes, however, a conditional branch doesn't actually result in any changes that the verifier cares about:
Tardy 首先给出了一个最简单的分支控制流示例:一个只包含单个 if 语句的程序。这个程序有两条潜在的执行路径。再增加一个(非嵌套的)if 语句,就会变成四条路径,再加一个就变成八条;当程序接近真实规模时,可能路径的数量将完全不可处理。不过,有时条件分支并不会导致验证器真正关心的任何变化:
1int index = 3; 2if (condition) { 3 // Some code that doesn't change the value of index 4 ... 5} 6// The validity of index doesn't depend on whether the branch was taken 7int foo = array[index]; 8
The core question that state pruning asks, Tardy said, is: "Can we skip some of the other paths?" To determine that, the verifier uses special "pruning points" in a program's execution where it knows that it might be able to cut out redundant paths. Pruning points are inserted at the sources and targets of conditional jumps, places where unconditional jumps rejoin a different series of instructions, and functi
《Verifier-state pruning in BPF》 是转载文章,点击查看原文。