LLVM improvements for BPF verification [LWN.net]

LLVM improvements for BPF verification

Posted May 31, 2024 12:20 UTC (Fri) by SLi (subscriber, #53131)
Parent article: LLVM improvements for BPF verification

A lot in this feels like it has parallels in how VHDL and Verilog constructs need to be translated into actual hardware like logic gates. Those languages are powerful enough to express constructs that are inherently unsynthesizable, like unbounded loops, similar to C for BPF. The trend there seems to be towards inputting higher level languages and inferring bounds.

Would one sensible way to express this problem be this: We can design a low-level language that can only express safe (in the BPF sense) programs and that can be reasonably mechanically and efficiently be translated into bytecode that the verifier accepts. This language needs to have some higher level constructs such as loops with specified bounds, so in this sense it's perhaps best thought of as a target-specific intermediate language instead of a backend language, which I assume in most compilers are strongly associated with something highly resembling lists of machine instructions.

The problem from general compiler point of view is that this language is rather distinct from the IRs that the compiler otherwise works with. It is inherently designed to not only carry but _require_ safety information; and it is inherently incomplete, in that there are valid programs that it cannot express (though obviously any C-to-BPF compiler needs to deal with this impendance somewhere in the pipeline).

It sounds to me like the current approach either does not use such a language at all (perhaps more likely?), or that that language is constructed from fairly far lowered LLVM IR or even from the generated BPF instructions.

It may well be that introducing such a language into a generic compiler framework is largely impossible. But such a language as a "target" would be what I would think of if I was working on a compiler for a such a system. Granted, I would very much prefer to work on a frontend for a language that actually cannot express non-verifiable programs (i.e. not C). If such a language was generated from LLVM IR, there's also the tricky question of "when". LLVM optimization passes work on the LLVM IR. Doing the lowering too early makes it impossible to run those optimization passes. Doing it as late as reasonably possible will probably make it trickier to do because of difficult things the optimization passes have done. And even then it seems likely that optimizing the bytecode generated "mechanically" from this intermediate language would still benefit from many optimization passes that only operate on LLVM IR.

to post comments

LLVM improvements for BPF verification

Posted May 31, 2024 16:04 UTC (Fri) by Wol (subscriber, #4433) [Link] (1 responses)

In that case, couldn't you just run a subset of LLVM optimisers? Ones that are either "verifier safe" such as unrolling loops, or make the verification process easier.

You could probably actually write a lot of the verification code in an LLVM optimiser, just that it's designed to optimise for verification, not to optimise code speed/size.

Cheers,
Wol

LLVM improvements for BPF verification

Posted May 31, 2024 16:20 UTC (Fri) by SLi (subscriber, #53131) [Link]

I suspect that the story about "verification safe" passes may be trickier. That approach would work if the process started from something verification safe. But if you start from arbitrary code with no safety guarantees, I'd expect to run into cases where the same optimization pass, given two inputs A and B where A is verifiable and B is not, would flip it so that it makes B verifiable and A not.

But just to be clear, I claim to understand something about compilers and software verification in general; I'm not particularly familiar with this specific case.