Bounded loops in BPF for the 5.3 kernel

Posted Aug 6, 2019 11:39 UTC (Tue) by massimiliano (subscriber, #3048)
In reply to: Bounded loops in BPF for the 5.3 kernel by Karellen
Parent article: Bounded loops in BPF for the 5.3 kernel

The way I see it, the semantics of the BPF is that a program needs to be verified, and then executed. The verification step is an integral part of the execution, because if affects the final result of the high level invocation of a BPF program (the invocation might fail because the verification fails).

My take is that the verifier, being implemented in a Turing complete language (C), is subject to the halting problem and in principle could never terminate.

It is like if every BPF program had an initial implicit "verify" instruction opcode. A BPF program without verification step is Turing complete (thanks to its loops), and one with the verification step... maybe is not Turing complete by itself (it number of states is bounded so in the end it is a a finite state machine), but it is still subject to the halting problems because of the verifier!

Of course, as said in other comments, nothing of this matters in practice. But it is one way of understanding how BPF programs are not violating the "halting problem" principle: it's just that kernel developers are trusting the verifier to always terminate :-)

Bounded loops in BPF for the 5.3 kernel

Posted Aug 7, 2019 7:39 UTC (Wed) by laarmen (subscriber, #63948) [Link] (1 responses)

What the halting problem basically says is that there are some programs for which one cannot tell if they will halt or not. Doesn't mean all programs, nor even most programs, just "some". I'm not aware of any proof that the verifier is one of those programs (nor of a proof that it halts, for that matter), and a quick Google search doesn't turn out any promising link.

Anyone aware of such work ?

Bounded loops in BPF for the 5.3 kernel

Posted Aug 8, 2019 19:27 UTC (Thu) by johill (subscriber, #25196) [Link]

The verifier always halts, simply because it gives up after a while. It only processes a maximum of 1e6 instructions (BPF_COMPLEXITY_LIMIT_INSNS) before giving up:

                if (++env->insn_processed > BPF_COMPLEXITY_LIMIT_INSNS) {
                        verbose(env,
                                "BPF program is too large. Processed %d insn\n",
                                env->insn_processed);
                        return -E2BIG;
                }