[HN Gopher] eBPF Verification Is Untenable
___________________________________________________________________
eBPF Verification Is Untenable
Author : williamallthing
Score : 23 points
Date : 2023-06-22 20:54 UTC (2 hours ago)
(HTM) web link (twitter.com)
(TXT) w3m dump (twitter.com)
| dathinab wrote:
| 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
| various subtle ways (not technical problems put people problems).
| Animats wrote:
| 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/
| mananaysiempre wrote:
| Hm. Doesn't look viable.
|
| 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,
| as least for now, millions of lines of C++ in 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, as sound, tractable, and expressive type systems are
| usually fairly isolated in design space, preventing source-to-
| source translation.
|
| 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.
| wzdd wrote:
| 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, 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.
___________________________________________________________________
(page generated 2023-06-22 23:00 UTC)