2025-09-28 –, Auditorium B032 (80)
The BPF verifier has troubles when verifying loops. This talk will cover:
- historical evolution of loops handling by verifier;
- problems with current state of things (too crude widening,
no bounds for induction variables); - describe DFA based liveness analysis that landed last week;
- describe further steps adding DFA-based value range analysis to
the verifier (a very hand-waving part).
We are interested in the feedback of the GNU toolchain community, especially when it comes to range analysis.
I work on Linux Kernel BPF verifier since 2022, mostly on its core logic.
Before that I worked on high level to high level language transpilers for more than 10 years.