5 ms·

Loops must be bounded, that means, the verifier must be able to see that the loop will eventually terminate based on the condition. The verifier will simulate a

Loops must be bounded, that means, the verifier must be able to see that the loop will eventually terminate based on the condition. The verifier will simulate all iterations of the loop and as such it is limited by the verifier complexity, that is, it'll do analysis of up to 1 million walked insns for the entire program until the verifier rejects it.

mehrdadn 6y ago
Okay thanks! So what I don't get is, what's the point of bounding loops then? If it's already simulating the program up to 1M instructions and rejecting it if simulation doesn't prove termination (bounded model checking?), then can't it still do that when there's no loop bound? Because I kind of expected the algorithm would say "hey this loop is bounded up to 4K, this nested one is up to 3K, therefore I can't prove the total is below 1M, therefore I reject", but from your description it sounds like it actually does some kind of bounded model checking up to 1M instructions instead of taking shortcuts like this? Or did you mean it actually does take shortcuts like this?
- kleendr12 6y ago
  When there's no loop bound it cannot prove termination, see halting problem. Goal is to avoid getting an infinite loop and then freezing the kernel of course.
  - mehrdadn 6y ago
    Right but I guess the point I'm getting at is that termination seems neither necessary nor sufficient to me. A loop (or nested loops...) that goes up to 2^63 may as well be infinite, so on the face of it it's not obvious why boundedness gets you anywhere by itself—you'd need to prove something stronger anyway. Conversely, it's not impossible to have loops that nevertheless (provably) terminate within N instructions. But if you're already bounding the number of instructions, why do you need bounded loops to begin with? Is that a necessary lemma of some sort before the algorithm is capable of proving something stronger? At first glance I don't see why the simulation (BMC?) approach you suggested would require bounded loops, since it would seem it might be capable of proving the termination of some unbounded loops within 1M instructions too.
    - kleendr12 6y ago
      I'm not quite sure I follow your comment. If the program never terminates then it will loop forever and potentially freeze the machine depending from where it is invoked in the kernel. Example of loops that can be detected to terminate: int nested_loops(volatile struct pt_regs* ctx) { int i, j, sum = 0, m; for (j = 0; j < 300; j++) for (i = 0; i < j; i++) { if (j & 1) m = ctx->rax; else m = j; sum += i * m; } return sum; } Or for example another one that is also part of selftests with induction variable i: int while_true(volatile struct pt_regs* ctx) { int i = 0; while (true) { if (ctx->rax & 1) i += 3; else i += 7; if (i > 40) break; } return i; } Overall this is very useful to avoid unrolling loops & keeping the code dense and icache friendly, and to parse (e.g.) IPv6 extension headers and such.
      - mehrdadn 6y ago
        Oh! I thought bounded loops meant every loop has to have a bound (hence while (true) wouldn't work). If it can handle more complicated situations then that answers my question. The second example is identical to a do-while loop though, so it's not clear to me if it can actually handle more complicated situations that don't directly map to for/while/do-while loops. For example, can it handle something like the following, where there's no bound, but the loop necessarily always terminates? (I assumed this loop would be called "unbounded", but maybe I'm confused by the terminology?) int test(unsigned i, unsigned j) { while (true) { i ^= j; j ^= i; i ^= j; if (i <= j) { return 0; } i ^= j; j ^= i; i ^= j; if (j <= i) { return 1; } i ^= j; j ^= i; i ^= j; } return 2; }
        kleendr13 6y ago
        Very interesting question, I just gave that a run with i and j being unknown and seems it's getting rejected by the verifier as it still probes the else path. Note that LLVM will convert the xor patterns to moves: ; __u64 i = PT_REGS_FP(ctx), j = PT_REGS_RC(ctx); 0: (79) r2 = *(u64 *)(r1 +32) ; __u64 i = PT_REGS_FP(ctx), j = PT_REGS_RC(ctx); 1: (79) r1 = *(u64 *)(r1 +80) ; 2: (bf) r3 = r1 3: (bf) r1 = r2 4: (bf) r2 = r3 ; if (i <= j) { return 0; } 5: (2d) if r3 > r1 goto pc-4 from 5 to 2: R1=inv(id=2) R2=inv(id=1) R3=inv(id=1) R10=fp0 ; 2: (bf) r3 = r1 3: (bf) r1 = r2 4: (bf) r2 = r3 ; if (i <= j) { return 0; } 5: (2d) if r3 > r1 goto pc-4 from 5 to 2: R1_w=inv(id=1) R2_w=inv(id=2) R3_w=inv(id=2) R10=fp0 ; 2: (bf) r3 = r1 3: (bf) r1 = r2 4: (bf) r2 = r3 ; if (i <= j) { return 0; } 5: (2d) if r3 > r1 goto pc-4 ; infinite loop detected at insn 2
- tptacek 6y ago
  A shot in the dark but maybe the disconnect here is: BPF statically verifies your program at load time, but a loaded BPF program is executed many, many times after that, with varied inputs. It can't be verified every time it is run, only the first time it's loaded.

mehrdadn 6y ago

Okay thanks! So what I don't get is, what's the point of bounding loops then? If it's already simulating the program up to 1M instructions and rejecting it if simulation doesn't prove termination (bounded model checking?), then can't it still do that when there's no loop bound? Because I kind of expected the algorithm would say "hey this loop is bounded up to 4K, this nested one is up to 3K, therefore I can't prove the total is below 1M, therefore I reject", but from your description it sounds like it actually does some kind of bounded model checking up to 1M instructions instead of taking shortcuts like this? Or did you mean it actually does take shortcuts like this?

kleendr12 6y ago
When there's no loop bound it cannot prove termination, see halting problem. Goal is to avoid getting an infinite loop and then freezing the kernel of course.
- mehrdadn 6y ago
  Right but I guess the point I'm getting at is that termination seems neither necessary nor sufficient to me. A loop (or nested loops...) that goes up to 2^63 may as well be infinite, so on the face of it it's not obvious why boundedness gets you anywhere by itself—you'd need to prove something stronger anyway. Conversely, it's not impossible to have loops that nevertheless (provably) terminate within N instructions. But if you're already bounding the number of instructions, why do you need bounded loops to begin with? Is that a necessary lemma of some sort before the algorithm is capable of proving something stronger? At first glance I don't see why the simulation (BMC?) approach you suggested would require bounded loops, since it would seem it might be capable of proving the termination of some unbounded loops within 1M instructions too.
  - kleendr12 6y ago
    I'm not quite sure I follow your comment. If the program never terminates then it will loop forever and potentially freeze the machine depending from where it is invoked in the kernel. Example of loops that can be detected to terminate: int nested_loops(volatile struct pt_regs* ctx) { int i, j, sum = 0, m; for (j = 0; j < 300; j++) for (i = 0; i < j; i++) { if (j & 1) m = ctx->rax; else m = j; sum += i * m; } return sum; } Or for example another one that is also part of selftests with induction variable i: int while_true(volatile struct pt_regs* ctx) { int i = 0; while (true) { if (ctx->rax & 1) i += 3; else i += 7; if (i > 40) break; } return i; } Overall this is very useful to avoid unrolling loops & keeping the code dense and icache friendly, and to parse (e.g.) IPv6 extension headers and such.
    - mehrdadn 6y ago
      Oh! I thought bounded loops meant every loop has to have a bound (hence while (true) wouldn't work). If it can handle more complicated situations then that answers my question. The second example is identical to a do-while loop though, so it's not clear to me if it can actually handle more complicated situations that don't directly map to for/while/do-while loops. For example, can it handle something like the following, where there's no bound, but the loop necessarily always terminates? (I assumed this loop would be called "unbounded", but maybe I'm confused by the terminology?) int test(unsigned i, unsigned j) { while (true) { i ^= j; j ^= i; i ^= j; if (i <= j) { return 0; } i ^= j; j ^= i; i ^= j; if (j <= i) { return 1; } i ^= j; j ^= i; i ^= j; } return 2; }
      - kleendr13 6y ago
        Very interesting question, I just gave that a run with i and j being unknown and seems it's getting rejected by the verifier as it still probes the else path. Note that LLVM will convert the xor patterns to moves: ; __u64 i = PT_REGS_FP(ctx), j = PT_REGS_RC(ctx); 0: (79) r2 = *(u64 *)(r1 +32) ; __u64 i = PT_REGS_FP(ctx), j = PT_REGS_RC(ctx); 1: (79) r1 = *(u64 *)(r1 +80) ; 2: (bf) r3 = r1 3: (bf) r1 = r2 4: (bf) r2 = r3 ; if (i <= j) { return 0; } 5: (2d) if r3 > r1 goto pc-4 from 5 to 2: R1=inv(id=2) R2=inv(id=1) R3=inv(id=1) R10=fp0 ; 2: (bf) r3 = r1 3: (bf) r1 = r2 4: (bf) r2 = r3 ; if (i <= j) { return 0; } 5: (2d) if r3 > r1 goto pc-4 from 5 to 2: R1_w=inv(id=1) R2_w=inv(id=2) R3_w=inv(id=2) R10=fp0 ; 2: (bf) r3 = r1 3: (bf) r1 = r2 4: (bf) r2 = r3 ; if (i <= j) { return 0; } 5: (2d) if r3 > r1 goto pc-4 ; infinite loop detected at insn 2
tptacek 6y ago
A shot in the dark but maybe the disconnect here is: BPF statically verifies your program at load time, but a loaded BPF program is executed many, many times after that, with varied inputs. It can't be verified every time it is run, only the first time it's loaded.