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 of them. To me, the situation makes me think "so why are we allowing these helper functions?". The suggestion is, among other things, to replace these helpers with Rust code. But couldn't we just have the helpers not suck to begin with?
Using the Rust compiler as a sort of safety oracle also ignores the fact that rustc has numerous problems that can lead to unsafe code without `unsafe` (and tbh I don't really see the project prioritizing these cases because it's just not a meaningful problem for the typical rust threat model). They sort of address this but not very well imo - timers and runtime mitigations aren't ideal.
I think what might make much more sense is to instead have the eBPF Virtual Machine (and verifier) written in Rust, including all helper functions, but to still execute pure, verified ebpf within it, using a verifier that's been built in a way that's actually sound.
1. The verifier attack surface goes down because it's Rust. I think that removes the need to keep it in userland, which would fly for Windows / BSD but not Linux.
2. Helpers are in Rust so they're at least safer - I feel like this addresses a (the?) major priority in the paper. Based on the paper's notes about implementing helpers in rust requiring no unsafe, it's probably safe to say that the verifier and helpers being in Rust would solve a lot of problems without requiring eBPF programs to be in Rust (and good news, Rust programs can expose a C API).
3. We don't throw out the baby with the bath water. A verified program is a cool thing to have. I would rather keep verification.