BPF Verifier State Pruning: Timeline
This article is part of a series of notes that Mahé Tardy and I wrote to prepare a presentation introducing the BPF verifier state pruning for Linux Plumbers 2025 in Tokyo. You can also find the slides and the video recording of the presentation.
State pruning is what helps the BPF verifier in Linux scale to larger programs. It mitigates the path explosion problem by pruning paths that are equivalent to already-verified paths. State pruning evolved alongside the verifier for the past decade. As we illustrated in our talk, it started as a simple optimization and grew into a more complex and efficient component of the verifier.
This timeline tracks the main changes state pruning went through.
Each commit is prefixed with a symbol to indicate the overall impact the change had on the complexity (the “cost” of verification).
For example, ↓ means the commit decreased complexity and therefore helped the verifier scale.
Commits suffixed with a * have been backported to at least one LTS kernel.
As we publish more articles with Mahé, I’ll include more link to Read more on important changes.
- f0318d Track offseted map value pointers while on the stack.
- dc503a Track register liveness.
- 4f7b3e* Extend dead-branch detection to all types of numeric conditions.
- 9f4686 Least-recently used mechanism to limit number of saved states at pruning points.
- f7cf25* Track constant scalar registers as they are spilled to the stack.
- 258972 Support bounded loops, introduce heuristic to decide when to save the verifier state on a pruning point.
- b5dc01 Introduce precise tracking of scalar values.
- a3ce68 Fix precision propagation in case of pruned paths.
- 675417 Fix precise tracking in case of subprogs.
- cc52d9 Require precise tracking of map lookup key for tail calls.
- 51c39b Support function-by-function verification.
- 354e8f* Track all bounded scalar registers as they are spilled to the stack.
- a3b666* Fix precision propagation in case of ALU operations.
- be2ef8* Do not completely disable precise tracking whenever subprogs are used.
- f63181* Improve accuracy of precision propagation.
- bffdea* Decouple jump history from pruning points.
- 7a830b* Improve accuracy of precision propagation by actively forgetting precise marks.
- 2793a8* For
iter_nextloops, require exact state match in state pruning and introduce widening of registers. - 42d31d Improve
BPF_JEQandBPF_JNEdead-branch detection by using signed ranges. - ab5cfa* Add a pruning point on calls to synchronous callback functions, fix callback function verification to verify all iterations.
Read more - cafe2c* Extend use of register widening to synchronous callback functions.
- 0acd03* Require precise tracking of R0 on callback function return.
- eabe51 Require precise tracking of R0 when checking return code is within expected range.
- 41f6f6 Precise tracking on spill to the stack even if using non-R10 register.
- 18a433 Don't trigger precise tracking whenever writing zero register to aligned stack slots.
- 4bf79f Improving precise tracking at conditional jumps in case of linked registers.
- 14c855 Data-flow analysis for register liveness, before the actual program analysis.