Spectre Mitigations Part 2
wasmjit.org
wasmjit.org
What makes this sandbox different from previous sandboxes (JVM, browsers, etc) that makes proponents sufficiently confident to put it in the kernel? All previous sandboxed designed to be secure have been broken on a regular basis.
The rationale seems to be performance, as if it is an innovation to realize that having multiple isolated processes and privilege levels has a cost, and things could be faster without context switches or virtual memory. But everyone knows this already - the real innovation is daring to trust your sandbox so much that you think you can do without process isolation.
Sorry to keep asking, but it strikes me as irresponsible to bash on context switching as having poor performance and not noting that it is really one of the foundations of computer security.
First time I asked: https://news.ycombinator.com/item?id=18406623
(I still agree with you.)
What makes WASM a large env? It was specifically designed to be more tractable to analyse than machine code, so it's already more restricted.
* eBPF explicitly doesn't do register allocation, which simplifies code generation.
* Similarly, eBPF is a 2 address, but load/store architecture, so for the vast majority of cases for both CISC and RISC architectures, there's a one to one correlation between eBPF instructions and native processor instructions, also greatly simplifying code generation.
* The only actually used eBPF implementation heavily reduces the options of the code flow graph to being a not quite Turing complete subset. The code flow graph can only be a DAG, so you can rely on being able to generate programs that you can easily, statically verify will terminate.
* The memory usage is a lot more explicit. The stack can be checked for worst case usage. Heap (called "maps") memory is typed. So types can be easily checked from registers, through the stack, and through to the heap. And that includes when heaps are shared with user space or other eBPF programs running in parallel.
So eBPF sort of starts from a place of remarkable verification, with the idea of loosening the constraints as new ways of guaranteeing code is safe are found. WASM tooling isn't as amenable to working under such circumstances.
It also simplifies the JIT to an almost trivial translation, greatly simplifying verfication of correctness. That is a huge help in the constrained environment of kernel space.
FWIW, part of what I've been working on is formally verifying an eBPF runtime, to cut down the number of standard code bugs. If he's talking about Spectre stuff, there's going to have to be hardware mitigations as you can hit the same architecture flaws even without code generation. It was just easier for Project Zero to use BPF rather than track down the code sequences they were looking for in the existing kernel.
The most recent catastrophic one was CVE-2017-16995.
Yeah, I'm not sure that's accurate, and even if it were, I'm not sure that's relevant. The description of the addressing modes in eBPF [1] means each instruction is polymorphic just like in WASM, yielding a multiplicative explosion in instructions in both cases.
Furthermore, the "extras" in WASM amounts to supporting floating point, different integral types other than 32-bit int, function calling instructions and basic loops. Hardly revolutionary or difficult to implement. Once you add those with the requisite polymorphic instructions, eBPF and WASM aren't so dissimilar. You could argue those aren't necessary, and yet they unarguably make WASM a more attractive target, and the instructions can be specifically optimized in ways that simulating them cannot be.
> * eBPF explicitly doesn't do register allocation, which simplifies code generation.
Translation: eBPF isn't fast. The majority of performance in virtual machines is from decent register allocation.
> [eBPF is a] load/store architecture, so for the vast majority of cases for both CISC and RISC architectures, there's a one to one correlation between eBPF instructions and native processor instructions, also greatly simplifying code generation.
This is shared by WASM.
> * The only actually used eBPF implementation heavily reduces the options of the code flow graph to being a not quite Turing complete subset. The code flow graph can only be a DAG, so you can rely on being able to generate programs that you can easily, statically verify will terminate.
Does not follow. CPP is guaranteed to terminate as well, and yet you can easily write macros [2] that will blow up CPP at compile-time because the generated expression is so large. Not Turing complete does entail "tractable".
> * The memory usage is a lot more explicit. The stack can be checked for worst case usage.
Useful, but this has also been done for Turing complete languages as well, so there's no a priori reason to think you can't get 90% of the same effect with WASM, and without the expressiveness headaches of dealing with non-Turing completeness.
As for verification, yes limiting expressiveness is useful for making certain properties trivial, but it also makes your tool less useful.
[1] https://www.kernel.org/doc/Documentation/networking/filter.t...
The size of the verifier and runtime is absolutely relevant to keeping the TCB down to a manageable level.
> The description of the addressing modes in eBPF [1] means each instruction is polymorphic just like in WASM, yielding a multiplicative explosion in instructions in both cases.
There's two very different ISAs being described in that doc, the classic BPF from the 90s that resembled a CISC architectre with tons of addressing modes, and the more RISC-esque eBPF that only has the one.
> Furthermore, the "extras" in WASM amounts to supporting floating point, different integral types other than 32-bit int, function calling instructions and basic loops. Hardly revolutionary or difficult to implement. Once you add those with the requisite polymorphic instructions, eBPF and WASM aren't so dissimilar. You could argue those aren't necessary, and yet they unarguably make WASM a more attractive target, and the instructions can be specifically optimized in ways that simulating them cannot be.
I described above how they're different, and how that helps simplify the in kernel work for eBPF.
> Translation: eBPF isn't fast. The majority of performance in virtual machines is from decent register allocation.
The register allocation is done by the untrusted code and is only verified by the runtime. You can still achieve very good register usage.
>> [eBPF is a] load/store architecture, so for the vast majority of cases for both CISC and RISC architectures, there's a one to one correlation between eBPF instructions and native processor instructions, also greatly simplifying code generation.
> This is shared by WASM.
Your [] block is telling. It cut off the first half of that clause which is necessary for my comment to make sense. WASM is a stack based machine which means you have a strict choice between fast JITed and a dead simple code generator. The two address register instruction part that you cut off is an extremely important part of that.
> Does not follow. CPP is guaranteed to terminate as well, and yet you can easily write macros [2] that will blow up CPP at compile-time because the generated expression is so large. Not Turing complete does entail "tractable".
I'm not sayig that it's tractable because it's turing incomplete; I'm saying that it's Turing incomplete because it's tractable. It's tractable because the code flow graph is a DAG with non infinite code size. The macro example doesn't apply because there's no in kernel expansion like that.
> Useful, but this has also been done for Turing complete languages as well
It's only been done for Turing complete languages by keeping to a Turing incomplete subset. That's how sel4 works for instance.
> so there's no a priori reason to think you can't get 90% of the same effect with WASM, and without the expressiveness headaches of dealing with non-Turing completeness.
It's the other 10% that worries me. : ) Yeah, you can get 90% of the way there in WASM, but that doesn't cut it for the use case.
> As for verification, yes limiting expressiveness is useful for making certain properties trivial, but it also makes your tool less useful.
Limiting expressiveness is the only way to get to verification. That's a natural consequence of the Halting problem. If you want to do crazy town stuff like getting to the point of running multi-tenant untrusted user code in kernel space, including in interrupt handlers, then you need to reduce expressiveness. Hell, even if you're compiling a regular kernel module you need to reduce expressiveness because of the environment.
Sure, but that's not the point I was making. The missing instructions are largely polymorphic operations on various integral and floating point types. WASM verification is not as hard as you seem to be implying.
> The register allocation is done by the untrusted code and is only verified by the runtime. You can still achieve very good register usage.
There are ways to do this safely even in stack machines. See: http://lambda-the-ultimate.org/node/5375
> WASM is a stack based machine which means you have a strict choice between fast JITed and a dead simple code generator.
A dead simple code generator that can only make use of 10 registers isn't all that compelling. Stack machines are great for compact code, and subexpression elimination and register allocation makes stack machines largely competitive with register machines. A lot of this can be moved offline as well (see link above).
> The two address register instruction part that you cut off is an extremely important part of that.
2-address instructions aren't competitive on all archs. They lead to unnecessary move sequences on 3-address architectures for one. This is why register allocation belongs in the VM.
> It's tractable because the code flow graph is a DAG with non infinite code size. The macro example doesn't apply because there's no in kernel expansion like that.
"DAG with non-infinite code size" also describes CPP, which is why I brought it up. That property simply doesn't say much.
> It's only been done for Turing complete languages by keeping to a Turing incomplete subset. That's how sel4 works for instance.
Not true, it's been done for SML with region-based memory management (MLKit IIRC). Regions with lexical lifetimes are just folded into the stack, but there's no requirement to restrict yourself to a Turing incomplete fragment (although your program must terminate, obviously, but that isn't the same thing).
> Limiting expressiveness is the only way to get to verification. That's a natural consequence of the Halting problem.
There are various ways to restrict programs though, so you don't have to restrict a language at the syntactic level which is far more painful than alternatives. For instance, sized types to guarantee termination and estimate space use.
Furthermore, as for memory and complexity analyses, there's lots of work that doesn't overly restrict expressiveness and yet can infer time, space and complexity bounds, among a few I easily found or have seen before:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142....
https://www.microsoft.com/en-us/research/publication/speed-p...
https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/publik...
https://www.cs.ru.nl/~marko/research/pubs/2007/TFP2007.pdf
Not that I think these are perfect solutions, I'm just pointing out that heavily restricting program expression has various approaches, and a brute force expressiveness-limiting hammer isn't the only way. I sympathize with your goal of wanting to reduce expressiveness to make analysis easier, but that makes the project less attractive as well because targeting it is much more work, and it has strictly limited application due to those restrictions.
Its worth noting that this has in many senses already been extensively research. This was a significant part of the design of Singularity OS, a micro kernel from Microsoft Research with software isolation between components (with much more formal sandboxing than wasmjit, verified with static analysis). Also there have been several operating systems with a JVM in the kernel over the last 2 decades with many of the same benefits.
It's worth noting that the code that will be run under Wasmjit will in general be more trusted than code you run in a browser while browsing the Web. For those who only run trusted code on their servers, Wasmjit incurs no additional risk and provides potentially significant benefit.
Another story pointed out that wasm today still lacks a few features and so, mostly regarding run-time inspection, has drawbacks server-side.
In the article there is no mention that wasm tomorrow could be quite different from wasm today; overall I believe the optimism is warranted.
Formalization was part of the process of developing WASM. That's already a large difference, and it led to a simpler instruction set that's more amenable to analysis.
Clearly if you are trying to run hostile software from multiple vendors on the same box (e.g. a browser), you want more sandboxes.
Also, if you are 100% sure that the code in it is trusted, then there really is no reason to sandbox it, right? If the intent is to only run trusted code, why is this article about spectre mitigations?
Trusted code can have bugs; sandboxing, in a sense, is always useful (not always beneficial)
Speculative vulnerabilities and side channels are a lot more than just variant 1 and 2.
WasmJIT is a nice project. But let me repeat. Do not put it in the kernel and run untrusted code through it, period. Software mitigations are not sufficient. This is not WASM's fault, this is not WasmJIT's fault; it's just a fundamental reality of modern hardware.
Timing related side channels seem unavoidable, but that doesn't mean that answer in -> answer out computation is necessarily intrinsically able to perform it.
Also, if you can trust code to not be malicious, but not to be correct, loading code via WASM and executing it in the same address space isn't necessarily crazy.
You can construct timers from shared mutable memory (think: counter thread), but even in shared-nothing systems, one can construct timers using message passing (think: a crude timer that counts messages in one process and a sender hammering it with messages).
> Also, if you can trust code to not be malicious, but not to be correct, loading code via WASM and executing it in the same address space isn't necessarily crazy.
Sure, agreed. This is why my comment mentioned untrusted code. WebAssembly sandboxing makes sense to protect the kernel from OOB writes, but it cannot guarantee no OOB reads from speculative side-channels.