eBPF Verification Is Untenable
twitter.com
eBPF Verification Is Untenable
1–10 of 116 posts
Re: eBPF Verification Is Untenable
#2Hm. Doesn’t look viable to me.
I’m not against language-based security, proof-carrying code, and all that, but I have less than perfect confidence that the Rust compiler currently is or will soon be sound enough to be secure against actively hostile code—AFAIU the language designers haven’t even written down their core calculus, let alone proven it sound. Putting the entirety of the Rust compiler (including, at least for now, millions of lines of C++ from LLVM) in the TCB of your system also feels less than inspiring.
There’s also the part where if you want to instrument the kernel with something other than Rust but still relatively powerful—I dunno, Ada—then you’re looking at putting the compiler for that in the TCB, too; you benefit from none of the verification work. Sound, tractable, and expressive type systems are usually fairly isolated in design space, so source-to-source translation of arbitrary programs is impossible most of the time.
Uploading System F (e.g. Dhall) or CoC to the kernel I could see—except for the tiny problem of memory management of course—but uploading Rust, even precompiled, I honestly can’t.
Re: eBPF Verification Is Untenable
#3This 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, and if someone can get the signing key then the kernel will run their signed code no problem.
2. The Rust compiler famously prevents various memory safety correctness bugs, but does not enforce other important parts of eBPF such as termination. The proposed solution is basically just to have a timeout instead. This moves checking for bugs from load time (with the verifier) to runtime, which means you will not know you have a buggy eBPF program until you actually hit the bug and it's terminated. Timeouts are strictly worse than termination checking because they are always either too long or too short.
3. Their major problem is with "escape hatches", kernel code which eBPF programs call out to. They show that various escape hatches can be eliminated or simplified. However they don't have a plan to eliminate all escape hatches, and don't even demonstrate that their technique would eliminate particularly problematic escape hatches.
Re: eBPF Verification Is Untenable
#4I 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 various subtle ways (not technical problems put people problems).
Re: eBPF Verification Is Untenable
#5I'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/
Re: eBPF Verification Is Untenable
#6This 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…
Your point 1 is the elephant herd in the room. If I were a paranoid person, I would think it’s by design - build in a way to compromise a system retroactively.
Re: eBPF Verification Is Untenable
#7This 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 someone can get the signing key then the kernel will run their signed code no problem.
FWIW I'm pretty sure this is how Microsoft does it. Verifier is in userland and signs programs post-verification. This keeps the attack surface unprivileged and is a great idea if you couple your Kernel to your userland and if your operating system has a notion of process protection - Linux doesn't do either.
Re: eBPF Verification Is Untenable
#8Hm. Doesn’t look viable to me. I’m not against language-based security, proof-carrying code, and all that, but I have less than perfect confidence that the Rust compiler currently is or will soon be sound enough to be secure against actively hostile code—AFAIU the language designers haven’t even written down their core calculus, let alone proven it sound. Putting the entirety of the Rust compiler (including, at least…
> to be secure against actively hostile code
Was that a requirement for the predecessor of eBPF: Custom kernel modules?
Re: eBPF Verification Is Untenable
#9This 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…
Your point 1 is the elephant herd in the room. If I were a paranoid person, I would think it’s by design - build in a way to compromise a system retroactively.
[deleted]
Re: eBPF Verification Is Untenable
#10The Rust compiler has several unsoundness bugs that are years old. If you trusted Rust language security in the kernel, these would all be security holes.