I've often found myself perplexed at the general BPF verifier approach.

Why is there so much time & effort spent trying to reconstruct (i.e. *guess*) high level[1] stuff like for loops rather than have the semantics available on the original code available to the verifier - perhaps represented in the bytecode? Having a couple of codes that represent standard loops, or even more general iterators seems like a no brainer to my uninformed mind.

Why is having this whole (increasingly complex and hairy) verification process *in kernel* so important? Some means o for an administrator to sign a BPF as "safe" again seems utterly sensible to me. Keep all the complexity out of kernel space, and the verification can be done once instead of every time the program is loaded. If an admin wants to miss the point by signing unsafe BPF programs, let them keep the pieces!

The verifier could even evolve separately from the kernel - a new, updated verifier could certify programs to run on a kernel that predates the latest improvements & bug fixes, for example. The admin could set policy requiring a certain version of the verifier separately from the kernel version, perhaps.

If *signing* isn't acceptable, perhaps there's some way for a more sophisticated user-space verifier to add something like a zero knowledge proof. The verifier could potentially *check* the safety claim more quickly/safely than it can be produced. An external verifier wouldn't need to be restricted by kernel resources etc. It could be aided by access to the source code, it could add invariant hints to the bytecode, simplifying the proof, making it tractible to a stripped down in-kernel verifier.

I see so many possibilities that the current approach seems to run screaming away from!

Presumably there are some really persuasive reasons why nothing I've thought of is sane, but nothing comes to mind for me...

[1] ...for sufficiently trivial definitions of "high level"