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

101–110 of 116 posts

Re: eBPF Verification Is Untenable

#101

Post by titzer »

tptacek wrote: post #50
titzer wrote: post #47

Earlier quoted context omitted.

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

I get that. Maybe you should read my comment again. Enforcement doesn't have to be dynamic. Any restrictions put on eBPF code could be enforced statically on Wasm code too. Wasm has way better JITs, some of which have been subjected to formal verification. The tech curve for Wasm engines is still pointing up, and eBPF has completely fallen off it and is a liability at this point. It should be abandoned in favor of Wasm.

Re: eBPF Verification Is Untenable

#102

Post by tptacek »

titzer wrote: post #101
tptacek wrote: post #50

Earlier quoted context omitted.

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.

I get that. Maybe you should read my comment again. Enforcement doesn't have to be dynamic. Any restrictions put on eBPF code could be enforced statically on Wasm code too. Wasm has way better JITs, some of which have been subjected to formal verification. The tech curve for Wasm engines is still pointing up, and eBPF has completely fallen off it and is a liability at this point. It should be abandoned in favor of Wa…

If you're back to relying on the same verifier, what does switching to WASM accomplish? I don't understand your "tech curve" point at all. If Rust programs compiled to WASM had to be BPF-verified, you'd be in exactly the same tooling pain you are now with eBPF. The hard part of writing eBPF programs isn't eBPF bytecode, which nobody uses (virtually all eBPF is either C or Rust now), it's passing the verifier.

Re: eBPF Verification Is Untenable

#103

Post by tptacek »

monocasa wrote: post #93
tptacek wrote: post #90

Earlier quoted context omitted.

That's not "quite a few" string helpers.

There are others too, for instance string formatting: https://elixir.bootlin.com/linux/latest/source/kernel/bpf/he...

Write an eBPF program that actually needs to do any kind of meaningful string manipulation, and you'll quickly get a sense of just how rich the BPF helper inventory is in string processing functions. It'll be sharply obvious, because bounded loop enforcement will keep you from writing even the simplest string functions yourself.

Re: eBPF Verification Is Untenable

#104

Post by monocasa »

tptacek wrote: post #103
monocasa wrote: post #93

Earlier quoted context omitted.

There are others too, for instance string formatting: https://elixir.bootlin.com/linux/latest/source/kernel/bpf/he...

Write an eBPF program that actually needs to do any kind of meaningful string manipulation, and you'll quickly get a sense of just how rich the BPF helper inventory is in string processing functions. It'll be sharply obvious, because bounded loop enforcement will keep you from writing even the simplest string functions yourself.

I never said that it's anywhere near a complete set. My point is that they exist as something that must be a helper because they represent a type of raw computation expected of bpf programs, but incompatible with it's verifier model.

The original parent was talking about removing all helpers,

> They show that various escape hatches can be eliminated or simplified. However they don't have a plan to eliminate all escape hatches

which simply doesn't make sense. The string helpers are a good example one might not have thought of beyond helpers that expose linux specific functionality.

The specific quantity of "quite a few" was left intentionally vague as it's orthogonal to my core point.

And yes, string ops are difficult if not impossible to write in verified bpf; that's almost a restatement of what I've been saying this whole thread.

Re: eBPF Verification Is Untenable

#105

Post by monocasa »

insanitybit wrote: post #88
monocasa wrote: post #75

Earlier quoted context omitted.

So "generic string processing helpers" provided by the kernel?

"quite a few" tho

There are others listed in the thread. The specific quantity of 'quite a few' is orthogonal to the core point and was intentionally left vague in what now appears to be a misguided attempt to keep the comment concise and focused.

Re: eBPF Verification Is Untenable

#106

Post by tptacek »

monocasa wrote: post #104
tptacek wrote: post #103

Earlier quoted context omitted.

Write an eBPF program that actually needs to do any kind of meaningful string manipulation, and you'll quickly get a sense of just how rich the BPF helper inventory is in string processing functions. It'll be sharply obvious, because bounded loop enforcement will keep you from writing even the simplest string functions yourself.

I never said that it's anywhere near a complete set. My point is that they exist as something that must be a helper because they represent a type of raw computation expected of bpf programs, but incompatible with it's verifier model. The original parent was talking about removing all helpers, > They show that various escape hatches can be eliminated or simplified. However they don't have a plan to eliminate all escap…

I don't think it's super common to do any kind of serious string manipulation in BPF. I happened to have Facebook's `dnswatch` open in my editor, and there are zero calls to strtol or printf. The idiomatic design here is to do that kind of thing in userland, piping raw stuff down a perf or ring buffer to postprocess in a "real" language runtime.

So my rebuttal would be: you could just remove those few string helpers, and not change much about the programming model.

Re: eBPF Verification Is Untenable

#107

Post by tptacek »

monocasa wrote: post #105
insanitybit wrote: post #88

Earlier quoted context omitted.

"quite a few" tho

There are others listed in the thread. The specific quantity of 'quite a few' is orthogonal to the core point and was intentionally left vague in what now appears to be a misguided attempt to keep the comment concise and focused.

Rookie mistake! :P

Re: eBPF Verification Is Untenable

#108

Post by edefefefee2 »

insanitybit wrote: post #7
wzdd wrote: post #3

This is weird. 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…

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

I'm a bit skeptical of this. It will work for some BPF use cases, but for others it might be a nightmare to deploy something in production at scale this way. Essentially on the target machine you're no better than signed kernel modules. If someone gets in possession of the key, they can do whatever they want given there is no verification mechanism anymore. It sounds good for programs of rather static nature, but for more complex application it's rather theory imo.

Re: eBPF Verification Is Untenable

#109

Post by dathinab »

insanitybit wrote: post #21
dathinab wrote: post #4

I hope no one tries to use the rust "safety" guarantees for security guards. They are designed to prevent bugs not intentional abuse. If perfect without bugs they theoretically might be usable for security guards, but it's not where priorities lies when it comes to bug fixes and design. And people mistaking rust safety + no unsafe lint for "security against evil code" could be long term quite an issue for rust in var…

They didn't mistake rust safety for anything. This is called out by them as a shrotcoming of their approach that has to be mitigated separately.

Because my comment was "in general" not specific to any specific case I very intentionally did not refer to the paper at all.

Re: eBPF Verification Is Untenable

#110

Post by dathinab »

IshKebab wrote: post #89
dathinab wrote: post #4

I hope no one tries to use the rust "safety" guarantees for security guards. They are designed to prevent bugs not intentional abuse. If perfect without bugs they theoretically might be usable for security guards, but it's not where priorities lies when it comes to bug fixes and design. And people mistaking rust safety + no unsafe lint for "security against evil code" could be long term quite an issue for rust in var…

Postgres does that for its new Rust support. https://news.ycombinator.com/item?id=35501065 They do ban unsafe and also the stdlib which probably covers a lot of soundness holes. Also I suspect the trust level required is somewhere in the middle.

in most situations custom SQL function are from a trusted source, through potentially run with untrusted inputs in a unprivileged/trusted execution environment.

this would mean they don't necessary rely on it for sandboxing untrusted code purpose

it's more like a convenient way to write a native extension function

through it's still a bit worrisome

Post reply on HN