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

eBPF Verification Is Untenable

twitter.com

Post reply on HN
Print view View original

51–60 of 116 posts

Re: eBPF Verification Is Untenable

#51

Post by tptacek »

andrewflnr wrote: post #26

I haven't been following the eBPF situation for a while, but... how did it come to this? I thought the point of BPF (sans 'e' anyway) was that it was pretty much secure by construction, or at minimum was simple enough to fully verify in polynomial time. So these eBPF vulnerabilities sound like a completely invented, unnecessary class of problems.

The track record of eBPF to date has been reasonably strong, and the threat model serious systems give to eBPF is narrow: you care a lot about the formal soundness of the verifier if you're loading untrusted code, and much less if you're never doing that. eBPF has been a pretty important victory for the Linux systems design model.

The real goal of eBPF verification is to avoid kernel crashes, and for that goal, eBPF has been unreasonably successful.

Re: eBPF Verification Is Untenable

#52

Post by insanitybit »

tptacek wrote: post #14

This paper is an easy read, but it's basically just restating the premises of eBPF: * Most programs can't be expressed in verified eBPF. * The verifier functions, to the extent it does, in large part by rejecting most programs (and implicitly limiting the uses to which eBPF can be put). * This is "extension code", and by definition, it interacts with the unsafe, unverified C code that the kernel is built out of. (In…

> ows from these premises that vendors should be careful about enabling non-root access to eBPF;

The thing is that it would be really nice to be able to set up a seccomp filter without a suid :\

Re: eBPF Verification Is Untenable

#53

Post by tptacek »

nathants wrote: post #38

to secure linux, both ebpf and io_ring need to be disabled in kconfig at kernel compile time. in security insensitive scenarios, they are both interesting tech.

Radically different thread models. io_uring is conventionally exposed to unprivileged programs, and eBPF virtually never is.

Re: eBPF Verification Is Untenable

#54

Post by insanitybit »

lcvw wrote: post #18
Animats wrote: post #5

I'm not happy about the entire concept of running user code in the kernel. As a special-purpose hack for servers that do very little else, maybe. As a standard OS feature, it seems to create too big an attack surface. One which has been exploited.[1] [1] https://www.theregister.com/2022/02/23/chinese_nsa_linux/

It requires root to use, if someone has root they’ve already owned your system anyway.

The kernel should be considered a tier above root, they shouldn't be considered the same level.

a) Root can be constrained by the kernel via LSM - you can run a program as root and it could be limited to very little given the current set of tools we have.

b) These days unprivileged users can be "root" in their own namespaces, so what "root" is means something very different

Re: eBPF Verification Is Untenable

#55

Post by insanitybit »

lcvw wrote: post #25
nightowl_games wrote: post #24

When I read about eBPF for kernel extension, it immediately made me think it would be full of security problems. I don't even know anything about the kernel, eBPF validation and barely anything about security, but just from a theoretical level, it seems highly insecure to run someone else's code in the kernel. "Verifying" it seems impossible from a theoretical level. Am I wrong? What's the limits of security in eBPF…

1. Using eBPF requires root 2. The verifier checks memory bounds access, guarantees termination in a certain number of instructions, and restricts function calls to a limited number of helper functions provided by the kernel. 3. BPF code runs on a vm, think like the jvm. It’s impossible to express a lot of nasty stuff given the restrictive bytecode language. There have been bugs in the verifier, but overall it works…

> 1. Using eBPF requires root

Unprivileged eBPF has been around for a long time.

Re: eBPF Verification Is Untenable

#56

Post by sanxiyn »

tptacek wrote: post #42
titzer wrote: post #37

Put extensions in a Wasm sandbox. The type system has been proven sound to the highest level of assurance possible with today's technology, mechanized at least twice, once in Coq and once in Isabelle. The algorithm is efficiently implementable and there are approaching a dozen production Wasm engines, some of which have tiers with proven safety guarantees. There is even an interpreter written in a proof assistant tha…

eBPF code gets to read and, with many limits, write kernel memory; further, the most fundamental guarantee BPF provides, going back to 1991, is that programs terminate, which isn't a Wasm guarantee. The verifier is doing something much more ambitious than hardened runtimes do (and that only because it makes drastic compromises in the otherwise valid programs it will accept).

Program termination is a solved problem with gas metering. Ethereum popularized the idea, but the idea itself is as old as hills.

Re: eBPF Verification Is Untenable

#57

Post by nathants »

tptacek wrote: post #53
nathants wrote: post #38

to secure linux, both ebpf and io_ring need to be disabled in kconfig at kernel compile time. in security insensitive scenarios, they are both interesting tech.

Radically different thread models. io_uring is conventionally exposed to unprivileged programs, and eBPF virtually never is.

isn’t the current linux security mindset that all access is potentially privileged?

Re: eBPF Verification Is Untenable

#58

Post by raggi »

Secure code inside the kernel is untenable.

We can do ok, lots of hard work goes in to doing ok, but this isn't the kernels top priority, and never will be.

Userspace is the security boundary.

Re: eBPF Verification Is Untenable

#59

Post by tptacek »

sanxiyn wrote: post #56
tptacek wrote: post #42

Earlier quoted context omitted.

eBPF code gets to read and, with many limits, write kernel memory; further, the most fundamental guarantee BPF provides, going back to 1991, is that programs terminate, which isn't a Wasm guarantee. The verifier is doing something much more ambitious than hardened runtimes do (and that only because it makes drastic compromises in the otherwise valid programs it will accept).

Program termination is a solved problem with gas metering. Ethereum popularized the idea, but the idea itself is as old as hills.

There's a subtlety being missed here. Proven termination of BPF programs far predates the adversarial threat model you and the WASM person are thinking about. It was a property of the original 1991 McCanne BPF. It's a safeguard for the programmer against themselves. eBPF shims in all over the place in the kernel; it would not be OK for the guarantee to simply be "there's a worst case maximum cycle budget for programs". eBPF programs are bounded, so they can be installed in hot places in the kernel.

The solved problem you're referring to is a much simpler problem.

Re: eBPF Verification Is Untenable

#60

Post by tptacek »

aseipp wrote: post #40

eBPF verification was always a laugh from the very beginning design stages, if you ask me, because as this paper demonstrates, it was never going to be enough. Anyone with a modicum of security or PLT experience could have told you this when evaluating the design and history. Like, if I had to be completely honest, the very fact the security/robustness model started on principles like "fixed number of loop iterations…

The original BPF model was "no backedge jumps, constrained memory model", and its track record is quite good. Say more about why you think "no backedge jumps" --- which isn't the current, more-sophisticated, harder-to-understand verification model --- was obviously weak.
Post reply on HN