Bounded loops in BPF for the 5.3 kernel

Posted Aug 7, 2019 7:39 UTC (Wed) by laarmen (subscriber, #63948)
In reply to: Bounded loops in BPF for the 5.3 kernel by massimiliano
Parent article: Bounded loops in BPF for the 5.3 kernel

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;
                }