Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

eBPF Summit Day 1 Recap

cilium.io

Post reply on HN
Print view View original

11–20 of 26 posts

Re: eBPF Summit Day 1 Recap

#11

Post by mehrdadn »

tptacek wrote: post #4
ArtWomb wrote: post #2

This caught my eye: Lou Xun (CCP Games) - Traffic Control the Rabbit with Rust using RedBPF. An xdp context transparently available to rust ;) https://github.com/aquarhead/protect-the-rabbit https://github.com/redsift/redbpf

Redbpf is a very cool project. But note that the Rust you get to work with is extremely limited: you don't get loops or native function calls (redbpf inlines them in the LLVM IR), and so essentially no library support. There are some BPF programs you can express in C (anything that relies on a bounded loop, for instance to walk a packet a byte at a time) that I don't think you can in redbpf right now. (Bounded loops…

Generic BPF question: do they actually impose a limit based on the loop bound? (If so, what is the limit on the loop bound?)

Re: eBPF Summit Day 1 Recap

#12

Post by kleendr12 »

mehrdadn wrote: post #11
tptacek wrote: post #4

Earlier quoted context omitted.

Redbpf is a very cool project. But note that the Rust you get to work with is extremely limited: you don't get loops or native function calls (redbpf inlines them in the LLVM IR), and so essentially no library support. There are some BPF programs you can express in C (anything that relies on a bounded loop, for instance to walk a packet a byte at a time) that I don't think you can in redbpf right now. (Bounded loops…

Generic BPF question: do they actually impose a limit based on the loop bound? (If so, what is the limit on the loop bound?)

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.

Re: eBPF Summit Day 1 Recap

#13

Post by mehrdadn »

kleendr12 wrote: post #12
mehrdadn wrote: post #11

Earlier quoted context omitted.

Generic BPF question: do they actually impose a limit based on the loop bound? (If so, what is the limit on the loop bound?)

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.

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?

Re: eBPF Summit Day 1 Recap

#14

Post by kleendr12 »

mehrdadn wrote: post #13
kleendr12 wrote: post #12

Earlier quoted context omitted.

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.

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 t…

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.

Re: eBPF Summit Day 1 Recap

#15

Post by mehrdadn »

kleendr12 wrote: post #14
mehrdadn wrote: post #13

Earlier quoted context omitted.

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 t…

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.

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.

Re: eBPF Summit Day 1 Recap

#16

Post by kleendr12 »

mehrdadn wrote: post #15
kleendr12 wrote: post #14

Earlier quoted context omitted.

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.

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.…

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 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.

Re: eBPF Summit Day 1 Recap

#17

Post by mehrdadn »

kleendr12 wrote: post #16
mehrdadn wrote: post #15

Earlier quoted context omitted.

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.…

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 rax; else m = j; sum += i * m; } return sum; } Or for example another one that is also part of sel…

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

Re: eBPF Summit Day 1 Recap

#18

Post by kleendr13 »

mehrdadn wrote: post #17
kleendr12 wrote: post #16

Earlier quoted context omitted.

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 rax; else m = j; sum += i * m; } return sum; } Or for example another one that is also part of sel…

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 followi…

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  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  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  r1 goto pc-4
  ;
  infinite loop detected at insn 2

Re: eBPF Summit Day 1 Recap

#19

Post by mehrdadn »

kleendr13 wrote: post #18
mehrdadn wrote: post #17

Earlier quoted context omitted.

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 followi…

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 =…

Ah I see, thanks for running it! Yeah so it's not this particular loop that's interesting (there's probably always going to be some simple-looking loop a solver can't prove—and I'm sure we could come up with simpler examples), but rather, the interesting question is whether it can figure out anything that doesn't map directly to bounded for/while/do-while loops. It's interesting because:

1. If the answer is no, then what is the precise reason? Is there a legitimate reason for it? After all, a bounded loop that loops for too long is just as bad as one that never terminates, so clearly they need a way to upper-bound the instruction count for any loop—at which point, why is the bound even relevant? The only reason I can think of is that they do simplistic analysis (e.g. multiplying the bounds on nested loops to naively approximate an overall bound), but your examples suggest they have more sophisticated (SMT/BMC?) solvers, and it's not obvious to me why a modern solver would fail on all unbounded loops.

2. If the answer is yes, then it would seem they actually do allow unbounded loops after all?

The other possibility is they're using the word "bounded" differently (e.g. maybe as a synonym for "terminating"), in which case it would be true that they would need bounded loops by definition.

Re: eBPF Summit Day 1 Recap

#20

Post by tptacek »

mehrdadn wrote: post #19
kleendr13 wrote: post #18

Earlier quoted context omitted.

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 =…

Ah I see, thanks for running it! Yeah so it's not this particular loop that's interesting (there's probably always going to be some simple-looking loop a solver can't prove—and I'm sure we could come up with simpler examples), but rather, the interesting question is whether it can figure out anything that doesn't map directly to bounded for/while/do-while loops. It's interesting because: 1. If the answer is no, then…

The verifier is extremely fussy. Different forms of the exact same loop (as far as the programmer is concerned) will get different results, and my experience is that I spend time rewriting the same loop in different ways just to get programs to pass. A bona-fide non-unrolled loop in a BPF program right now is a special thing that takes extra time to implement, and you're probably not going to use them casually.

The answer to whether BPF effectively allows unbounded loops is "no". The verifier essentially emulates the instructions in your loop, iteration by iteration, and gives itself a fixed budget to do so. If it can't prove the loop invariably exits in that budget, it rejects the program. Allowing an unbounded loop would be an important security vulnerability, and is kind of the whole original point of the verifier.

Probably, this is just a terminology issue; what the verifier in fact cares about is indeed whether the program terminates.

Post reply on HN