>
The BPF verifier is, fundamentally, a form of static analysis. It determines whether BPF programs submitted to the kernel satisfy a number of properties, such as not entering an infinite loop, not using memory with undefined contents, not accessing memory out of bounds, only calling extant kernel functions, only calling functions with the correct argument types, and others. As Alan Turing famously proved, correctly determining these properties for all programs is impossible — there will always be programs that do not enter an infinite loop, but which the verifier cannot prove do not enter an infinite loop. Despite this, the verifier manages to prove the relevant properties for a large amount of real-world code.[ Halting problem: https://en.wikipedia.org/wiki/Halting_problem ]
> Some basic properties, such as whether the program is well-formed, too large, or contains unreachable code, can be correctly determined just by analyzing the program directly. The verifier has a simple first pass that rejects programs with these problems. But the bulk of the verifier's work is concerned with determining more difficult properties that rely on the run-time state of the program [dynamic analysis].