3 ms·

Linux already allows untrusted user code to be run in a ring 0 VM, via BPF/eBPF. Honestly, given the choice between Web Assembly and eBPF to run in kernel mode,

Linux already allows untrusted user code to be run in a ring 0 VM, via BPF/eBPF. Honestly, given the choice between Web Assembly and eBPF to run in kernel mode, I'd go with Web Assembly. The fewer secure VMs that have to be audited, the better.

monocasa 8y ago
To be fair, BPF/eBPF is far more designed for simple and obviously correct verification. For eBPF, it's 10 register, two address, but load store, so that on CISC and RISC platforms there's generally a 1 to 1 between eBPF asm and JITed ASM. So the in kernel JIT doesn't even need a register allocator. The code flow graph is constrained to be a DAG so you can solve the halting problem on programs. etc. You're looking at at least a couple of orders of magnitude more work to get to the same level of correctness for a WebAssembly runtime.
- titzer 8y ago
  There has been a WebAssembly interpreter implemented in Isabelle [1] and it's been proved correct. Not fast, but still pretty cool. [1] https://www.isa-afp.org/entries/WebAssembly.html https://www.isa-afp.org/entries/WebAssembly.html
  - titzer 8y ago
    That said, I still wouldn't put it in ring 0, as per my comment on the other thread: https://news.ycombinator.com/item?id=17186842 https://news.ycombinator.com/item?id=17186842
  - monocasa 8y ago
    > Not fast That's the kicker. BPF is simpler, _and_ in spitting distance of native code perf. And if you're doing something crazy like injecting user code into interrupts, you care about perf. That being said, you're totally right that it's possible to get parity, just orders of magnitudes more work.
- pcwalton 8y ago
  Is it really that much worse? A simple greedy register allocator is very, well, simple. (You don't even need a register allocator, in fact, though your performance will be poor.) I'm not sure guaranteeing that a program halts really matters, either; really what you want is the ability to limit the amount of time a filter can run, which is simple to do directly. (In fact, it's simpler to add a timeout than to perform control flow analysis.)
  - monocasa 8y ago
    > Is it really that much worse? A simple greedy register allocator is very, well, simple. (You don't even need a register allocator, in fact, though your performance will be poor.) I mean, if you're doing something so crazy as pushing user controlled code into interrupt context, you care about performance. And the BPF scheme is within spitting distance of natively compiled code. > I'm not sure guaranteeing that a program halts really matters, either; really what you want is the ability to limit the amount of time a filter can run, which is simple to do directly. (In fact, it's simpler to add a timeout than to perform control flow analysis.) Right now, I don't think that there's a way for a BPF filter to 'fail' once it's been verified. It's sort of like a graphics shader in that regard. And timeouts can't be implemented with a timer since the the filters run at interrupt context already, and manual bookkeeping comes with a perf cost (at least a lost register, and some basic block epilogue code). And that's in addition to the "well the filter failed, now how do we handle that" question that's hinted at above.

monocasa 8y ago

To be fair, BPF/eBPF is far more designed for simple and obviously correct verification. For eBPF, it's 10 register, two address, but load store, so that on CISC and RISC platforms there's generally a 1 to 1 between eBPF asm and JITed ASM. So the in kernel JIT doesn't even need a register allocator. The code flow graph is constrained to be a DAG so you can solve the halting problem on programs. etc. You're looking at at least a couple of orders of magnitude more work to get to the same level of correctness for a WebAssembly runtime.

titzer 8y ago
There has been a WebAssembly interpreter implemented in Isabelle [1] and it's been proved correct. Not fast, but still pretty cool. [1] https://www.isa-afp.org/entries/WebAssembly.html https://www.isa-afp.org/entries/WebAssembly.html
- titzer 8y ago
  That said, I still wouldn't put it in ring 0, as per my comment on the other thread: https://news.ycombinator.com/item?id=17186842 https://news.ycombinator.com/item?id=17186842
- monocasa 8y ago
  > Not fast That's the kicker. BPF is simpler, _and_ in spitting distance of native code perf. And if you're doing something crazy like injecting user code into interrupts, you care about perf. That being said, you're totally right that it's possible to get parity, just orders of magnitudes more work.
pcwalton 8y ago
Is it really that much worse? A simple greedy register allocator is very, well, simple. (You don't even need a register allocator, in fact, though your performance will be poor.) I'm not sure guaranteeing that a program halts really matters, either; really what you want is the ability to limit the amount of time a filter can run, which is simple to do directly. (In fact, it's simpler to add a timeout than to perform control flow analysis.)
- monocasa 8y ago
  > Is it really that much worse? A simple greedy register allocator is very, well, simple. (You don't even need a register allocator, in fact, though your performance will be poor.) I mean, if you're doing something so crazy as pushing user controlled code into interrupt context, you care about performance. And the BPF scheme is within spitting distance of natively compiled code. > I'm not sure guaranteeing that a program halts really matters, either; really what you want is the ability to limit the amount of time a filter can run, which is simple to do directly. (In fact, it's simpler to add a timeout than to perform control flow analysis.) Right now, I don't think that there's a way for a BPF filter to 'fail' once it's been verified. It's sort of like a graphics shader in that regard. And timeouts can't be implemented with a timer since the the filters run at interrupt context already, and manual bookkeeping comes with a perf cost (at least a lost register, and some basic block epilogue code). And that's in addition to the "well the filter failed, now how do we handle that" question that's hinted at above.