Bounded loops in BPF programs

Posted Dec 4, 2018 11:50 UTC (Tue) by ibukanov (subscriber, #3942)
Parent article: Bounded loops in BPF programs

One can always replace a bounded loop by repeating the code up to max allowed number of iterations. So I suppose BPF can be extended with simple bytecodes for a loop that repeats the code, say, 100, times. If one wants to stop it earlier, one just use jumps. But proving that it cannot be subverted can be tricky.

Bounded loops in BPF programs

Posted Dec 4, 2018 14:19 UTC (Tue) by dskoll (subscriber, #1630) [Link] (4 responses)

A few nested loops and once again you can execute billions of iterations...

Bounded loops in BPF programs

Posted Dec 4, 2018 22:46 UTC (Tue) by ibukanov (subscriber, #3942) [Link] (1 responses)

There is no need to support nested loops. Any such loop can be re-written as single loop.

Bounded loops in BPF programs

Posted Dec 5, 2018 2:24 UTC (Wed) by dskoll (subscriber, #1630) [Link]

That would work if BPF programs couldn't call subroutines, or if the verifier chased subroutines down to make sure anything called within a loop didn't contain its own loop. Sounds pretty tricky and tedious. I don't envy those doing this work.

Bounded loops in BPF programs

Posted Dec 5, 2018 14:25 UTC (Wed) by mina86 (guest, #68442) [Link] (1 responses)

This seems to be the actual issue. For practical purposes, BPF program which terminates after an hour is just as unsafe as one which never terminates. Perhaps instead of trying to prove things about the program, it’d be better to simply limit how many instructions a program can execute and terminate it if it takes too long.

Bounded loops in BPF programs

Posted Dec 5, 2018 20:10 UTC (Wed) by matthias (subscriber, #94967) [Link]

This might be a valid catch all solution for situations where the proof aproach does not work. However, the verifier approach has many advantages. If the code can be proven to never execute more than the allowed number of instructions, there is no need to count instructions and place conditional jumps all over the code that will abort once the counter reaches zero. Apart from the performance boost, this also gives certainty that the code is never aborted due to taking too much time. If I rely on BPF programs that do not fail, I would anyway need a tool that can proof that the code does not use too many instructions. Then why not integrating this into the verifier?