Bounded loops in BPF for the 5.3 kernel

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

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.