5 ms·

eBPF Summit Day 1 Recap

128 points by genbit 6y ago

ArtWomb 6y ago
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/aquarhead/protect-the-rabbit https://github.com/redsift/redbpf https://github.com/redsift/redbpf
- ShaniceWilliams 6y ago
  interesting!
- tptacek 6y ago
  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 are really fussy anyways and you probably won't use them in most programs, so writing in a single language rather than Rust and C might easily be enough of a win).
  - mehrdadn 6y ago
    Generic BPF question: do they actually impose a limit based on the loop bound? (If so, what is the limit on the loop bound?)
    - kleendr12 6y ago
      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.
- danobi 6y ago
  A possibly lighter weight alternative is libbpf-rs [0]. libbpf-rs is designed to take advantage of BPF's Compile-Once-Run-Everywhere functionality where you can ship a pre-compiled object file to production instead of an entire compiler toolchain. Disclaimer: I wrote libbpf-rs. [0]: https://github.com/libbpf/libbpf-rs https://github.com/libbpf/libbpf-rs
  - tptacek 6y ago
    Do people generally do that? Is this an artifact of people using iovisor/bcc and Python or whatever? We just build .o files with clang and ship 'em.
    - rtkaratekid 6y ago
      I use libbpf-sys but that’s user space
    - brycekahle 6y ago
      Yes. If you ship any eBPF programs that utilize kprobes and/or read kernel structures that change between kernel versions, you have portability problems. See https://facebookmicrosites.github.io/bpf/blog/2020/02/19/bpf-portability-and-co-re.html https://facebookmicrosites.github.io/bpf/blog/2020/02/19/bpf... for a good overview of the problem that CO-RE intends to solve.
      - tptacek 6y ago
        Ah! That makes so much sense. It hadn't occurred; when we rolled out BPF at Fly, the first thing we did was commit to standardize our kernels. After all, there's not much CO-RE can do about your BPF compiler not having tail calls, or not allowing bounded loops. But we're almost entirely XDP; I can see kernel structs being a much bigger problem for people doing observability work.
ithkuil 6y ago
I really love this concise yet informative summary!
fdfddd 6y ago
day 2 stream is here: https://youtu.be/jw8tEPP6jwQ https://youtu.be/jw8tEPP6jwQ
- fdfddd 6y ago
  love the wide variety of lightning talks as well
genbit 6y ago
day 2 to recap - https://news.ycombinator.com/item?id=24944042 https://news.ycombinator.com/item?id=24944042

128 points by genbit 6y ago

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/aquarhead/protect-the-rabbit https://github.com/redsift/redbpf https://github.com/redsift/redbpf

ShaniceWilliams 6y ago
interesting!
tptacek 6y ago
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 are really fussy anyways and you probably won't use them in most programs, so writing in a single language rather than Rust and C might easily be enough of a win).
- mehrdadn 6y ago
  Generic BPF question: do they actually impose a limit based on the loop bound? (If so, what is the limit on the loop bound?)
  - kleendr12 6y ago
    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.
danobi 6y ago
A possibly lighter weight alternative is libbpf-rs [0]. libbpf-rs is designed to take advantage of BPF's Compile-Once-Run-Everywhere functionality where you can ship a pre-compiled object file to production instead of an entire compiler toolchain. Disclaimer: I wrote libbpf-rs. [0]: https://github.com/libbpf/libbpf-rs https://github.com/libbpf/libbpf-rs
- tptacek 6y ago
  Do people generally do that? Is this an artifact of people using iovisor/bcc and Python or whatever? We just build .o files with clang and ship 'em.
  - rtkaratekid 6y ago
    I use libbpf-sys but that’s user space
  - brycekahle 6y ago
    Yes. If you ship any eBPF programs that utilize kprobes and/or read kernel structures that change between kernel versions, you have portability problems. See https://facebookmicrosites.github.io/bpf/blog/2020/02/19/bpf-portability-and-co-re.html https://facebookmicrosites.github.io/bpf/blog/2020/02/19/bpf... for a good overview of the problem that CO-RE intends to solve.
    - tptacek 6y ago
      Ah! That makes so much sense. It hadn't occurred; when we rolled out BPF at Fly, the first thing we did was commit to standardize our kernels. After all, there's not much CO-RE can do about your BPF compiler not having tail calls, or not allowing bounded loops. But we're almost entirely XDP; I can see kernel structs being a much bigger problem for people doing observability work.

ithkuil 6y ago

I really love this concise yet informative summary!

fdfddd 6y ago

day 2 stream is here: https://youtu.be/jw8tEPP6jwQ https://youtu.be/jw8tEPP6jwQ

fdfddd 6y ago
love the wide variety of lightning talks as well

genbit 6y ago

day 2 to recap - https://news.ycombinator.com/item?id=24944042 https://news.ycombinator.com/item?id=24944042