Bounded loops in BPF for the 5.3 kernel

Posted Aug 1, 2019 15:29 UTC (Thu) by Karellen (subscriber, #67644)
In reply to: Bounded loops in BPF for the 5.3 kernel by johill
Parent article: Bounded loops in BPF for the 5.3 kernel

Just because a verifier for Turing-complete languages cannot reliably classify *all* arbitrary programs into either "safe" or "unsafe", that does not mean they don't exist or are useless. Verifiers can correctly classify large numbers of useful programs as safe. They can also correctly classify large numbers of unsafe programs as such. Any program that a verifier cannot classify, due to being insufficiently powerful, or due to the Halting problem, can simply be declared as "not verified safe" and rejected.

Note that this means that some useful, safe programs could be rejected. That is unfortunate, but not an argument that verifiers are impossible, or even useless.

Bounded loops in BPF for the 5.3 kernel

Posted Aug 1, 2019 17:27 UTC (Thu) by excors (subscriber, #95769) [Link] (10 responses)

I think there's some ambiguity on what the BPF language is (in the theoretical computer science sense of "language"). Is it all the programs that can be syntactically expressed with BPF bytecode? Or is it all the programs that can be expressed *and* that the verifier accepts? I think johill was using the latter, but the phrase "verifier for Turing-complete languages" seems to imply the former.

The pre-verification language may be Turing-complete (if it had unbounded loops or equivalent). The post-verification language cannot be, assuming the verifier only accepts programs that it can prove will halt (and rejects ones where it can't decide), because there will always exist a computation that halts but that cannot be implemented in a program that the verifier will accept. The post-verification language may still be useful in practice (as you say), but it's not Turing-complete.

In practice, Turing-completeness seems a pretty useless concept and a big distraction. Turing machines only care about the boundary between infinite and non-infinite, so a computation that requires more time than exists in the universe is just as good as one that completes almost immediately. A practical software engineer cares about a boundary measured in seconds or milliseconds, and a program that takes years is just as bad as one that never halts, so they need a totally different set of tools to analyse that problem.

Bounded loops in BPF for the 5.3 kernel

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

Yeah, I was indeed thinking of "the programs that will be accepted by the kernel verifier" - because that's actually what the article discusses (changes/improvements in the verifier).

The language itself is fairly obviously Turing complete (not that I've written down an emulator), but of course that is a theoretical concept anyway, as you say.

And in any case, going back to the OP's comment, BPF is almost certainly already reading email somewhere, in the form of DPI :-)

Bounded loops in BPF for the 5.3 kernel

Posted Aug 1, 2019 19:48 UTC (Thu) by Karellen (subscriber, #67644) [Link] (8 responses)

Just because the verifier only outputs programs which are guaranteed to halt, does that mean that the language used to express them is necessarily Turing-incomplete?

Bounded loops in BPF for the 5.3 kernel

Posted Aug 2, 2019 13:39 UTC (Fri) by mathstuf (subscriber, #69389) [Link] (3 responses)

Seems like a philisophical question to me. Is this C code? Or is it invalid because a reasonable C implementation could just say "no" rather than outputting any object code for it?

int* p = NULL;
int i = *p;

Bounded loops in BPF for the 5.3 kernel

Posted Aug 5, 2019 16:40 UTC (Mon) by shane (subscriber, #3335) [Link] (2 responses)

Hm... turning your code into a C program:

#include <stddef.h>

int
main ()
{
    int* p = NULL;
    int i = *p;
    return i;
}

We discover that clang doesn't warn or complain in any way:

$ clang --version
clang version 8.0.0-3 (tags/RELEASE_800/final)
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin
$ clang -Weverything foo.c
$ ./a.out
Segmentation fault (core dumped)

Likewise by default GCC doesn't:

$ gcc --version
gcc (Ubuntu 8.3.0-6ubuntu1) 8.3.0
Copyright (C) 2018 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

$ gcc -Wextra -Wall -Wpedantic foo.c
$ ./a.out
Segmentation fault (core dumped)

We can use a feature disabled by default:

$ gcc -Werror=null-dereference -O foo.c 
foo.c: In function ‘main’:
foo.c:7:9: error: null pointer dereference [-Werror=null-dereference]
     int i = *p;
         ^
cc1: some warnings being treated as errors

Enabling this warning apparently breaks the GCC self-bootstrapping build (as well as things like building the Linux kernel). The ticket which added the warning is here:

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=16351

Bounded loops in BPF for the 5.3 kernel

Posted Aug 5, 2019 17:09 UTC (Mon) by excors (subscriber, #95769) [Link] (1 responses)

I guess that's because it's only undefined behaviour if you actually execute main(), and the compiler doesn't know if you're going to execute main(), so it can't reject the code at compile time. And in practice this pattern probably occurs frequently in dead code, so programmers would get annoyed if it generated a warning.

GCC still knows that function must never be executed, so it replaces it with the "ud2" instruction (at least with gcc -O2).

Bounded loops in BPF for the 5.3 kernel

Posted Aug 6, 2019 9:27 UTC (Tue) by farnz (subscriber, #17727) [Link]

As an aside, examining the code in Matt Godbolt's Compiler Explorer shows that gcc 9.1 leaves an unnecessary MOV before UD2, while clang goes straight to RET. MSVC compiles to clear RAX, load EAX from *RAX, and return 0, while ICC generates code to set up SSE2 the way it wants it, loads AL from *NULL, and then calls an "abort" subroutine.

Bounded loops in BPF for the 5.3 kernel

Posted Aug 6, 2019 11:39 UTC (Tue) by massimiliano (subscriber, #3048) [Link] (2 responses)

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

Bounded loops in BPF for the 5.3 kernel

Posted Aug 7, 2019 15:48 UTC (Wed) by fuhchee (guest, #40059) [Link]

Yes, exactly - construing the language as the sequence of bpf bytecodes that are accepted as inputs.