[titzer]

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 that has been proven fully functionally correct.

[tptacek]

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

[titzer]

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

[tptacek]

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.

[neerajsi]

I don't think jitting necessarily precludes counting runtime instructions. You could always jit in an internal variable that gets incremented for each high level instruction being translated. And of course you can optimize the increments within each basic block. There's even a cool minimum spanning tree algorithm due to Larus and Ball originally for path profiling that might be adaptable to reduce increments across the blocks.

I know this is a bit of an aside. The point still stands about the user not wanting their bpf program to terminate at runtime investment.

[titzer]

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.

[tptacek]

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.

[sanxiyn]

Program termination is a solved problem with gas metering. Ethereum popularized the idea, but the idea itself is as old as hills.

[tptacek]

There's a subtlety being missed here. Proven termination of BPF programs far predates the adversarial threat model you and the WASM person are thinking about. It was a property of the original 1991 McCanne BPF. It's a safeguard for the programmer against themselves. eBPF shims in all over the place in the kernel; it would not be OK for the guarantee to simply be "there's a worst case maximum cycle budget for programs". eBPF programs are bounded, so they can be installed in hot places in the kernel.

The solved problem you're referring to is a much simpler problem.

[HappyPanacea]

What is the difference between "there's a worst case maximum cycle budget for programs" and bounded? and why it would not be OK?

[sanxiyn]

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.

[tptacek]

Well, for one thing, eBPF predates WebAssembly.