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

41–50 of 116 posts

Re: eBPF Verification Is Untenable

#41

Post by sanxiyn »

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…

This is such an obvious solution that I wonder why eBPF exists at all. WebAssembly is better for the purpose in like every way? Be against Not-Invented-Here, don't reinvent the wheel.

Re: eBPF Verification Is Untenable

#42

Post by tptacek »

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

Re: eBPF Verification Is Untenable

#43

Post by tptacek »

sanxiyn wrote: post #41
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…

This is such an obvious solution that I wonder why eBPF exists at all. WebAssembly is better for the purpose in like every way? Be against Not-Invented-Here, don't reinvent the wheel.

Well, for one thing, eBPF predates WebAssembly.

Re: eBPF Verification Is Untenable

#44

Post by tptacek »

lcvw wrote: post #29

I feel that this proposal defeats the entire purpose of ebpf. The point is to have a bytecode language that can do simple processing in the kernel. This code is frequently generated adhoc, such as with bpftrace. I don’t like all the limitations that currently exist in bpf, but just replacing it with rust and signature verification basically turns this into kernel modules all over again.

There's nothing really "simple" about eBPF bytecode; it's a full fledged ISA, so much so that the idiomatic way to build eBPF programs is to compile them from straight C with clang.

Re: eBPF Verification Is Untenable

#45

Post by tptacek »

stefan_ wrote: post #23
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…

Surely if you are allowing non-root eBPF then security of the programs is one of your least worries? Given all the implicit privilege escalation that comes with allowing non-root to spy on everything the kernel does.

Unprivileged BPF is used for socket filters, for programs to BPF-extend themselves. It wasn't ever the case that unprivileged eBPF would allow you to, say, load a TC filter and read everybody's traffic.

Re: eBPF Verification Is Untenable

#46

Post by insanitybit »

bayindirh wrote: post #39
insanitybit wrote: post #20

Earlier quoted context omitted.

That makes no sense

You should read Ken Thompson's "Reflections on trusting trust". Outsourcing security to a tool which you have to blindly trust, and can't verify is very, very dangerous.

You've obviously misunderstood the proposal - there's nothing about this that is "blind trust" at all.

Re: eBPF Verification Is Untenable

#47

Post by titzer »

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

> eBPF code gets to read and, with many limits, write kernel memory

Import kernel read/write functions into the Wasm module, so they can be policed. Or, if performance needs be, map limited portions of the kernel memory into the Wasm extensions linear memory.

> programs terminate,

Several Wasm runtimes count Wasm instructions (e.g. by internal bytecode rewriting) and dynamically enforce execution times. If static enforcement of termination is really all that important, exactly the same kinds of restrictions could be applied to Wasm code (e.g. bounded loops, no recursion, limits on function size, memory size, etc).

Re: eBPF Verification Is Untenable

#48

Post by insanitybit »

lcvw wrote: post #27
insanitybit wrote: post #11

First off, I kinda skimmed this. So I think the critical thing here is that verification is not enough . It has to be the critical thing, because the implementation in the kernel might suck but Microsoft has shown that it's possible to build a powerful eBPF verifier that isn't a hacky mess. The main issue is seemingly these helper functions. The position is that even a perfectly verified program won't be safe because…

It’s worth noting the verifier doesn’t verify C code, it verifies the compiled ebpf bytecode. You can generate that bytecode from rust (the solana cryptocurrency does this) but you still need to verify the actual instructions since someone can just write whatever they want by hand.

I'm suggesting that the ebpf code still be verified and that the only rust code used is to implement the verifier and the virtual machine itself.

Re: eBPF Verification Is Untenable

#49

Post by insanitybit »

mananaysiempre wrote: post #36
insanitybit wrote: post #7

Earlier quoted context omitted.

> 1. Instead of having the kernel verify the program about to be installed at installation time, they rely on a trusted compiler and having the kernel perform signature validation. This means that the kernel is relying on a userspace component to enforce kernel-level safety guarantees, adds another level of coupling (via key infrastructure) between the kernel and a particular version of the Rust compiler, and if some…

Driver Verifier? That’s not intended to prove the code under test secure, only to hopefully show that it’s not complete crap in well-known ways. Even a signed driver is still trusted code and requires administrator privileges to install. I guess the closest Linux counterpart would be a distro maintainer running a hardware vendor’s out-of-tree module under KASAN and, if it passes, signing the package with their PGP ke…

No, not driver verifier. https://github.com/vbpf/ebpf-verifier

Re: eBPF Verification Is Untenable

#50

Post by tptacek »

titzer wrote: post #47
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).

> eBPF code gets to read and, with many limits, write kernel memory Import kernel read/write functions into the Wasm module, so they can be policed. Or, if performance needs be, map limited portions of the kernel memory into the Wasm extensions linear memory. > programs terminate, Several Wasm runtimes count Wasm instructions (e.g. by internal bytecode rewriting) and dynamically enforce execution times. If static enf…

The BPF verifier doesn't simply count instructions (though there is a maximum instruction count as a failsafe). It can't: eBPF programs are JIT'd down to machine code --- that's part of what makes eBPF so attractive, because the code you're running is comparably fast to the "native" kernel code. Instead, it refuses to admit programs that can't be proven to constrain their loops.
Post reply on HN