Hacker News Reader

Comment by _0w8t | Hacker News Reader

Both PNaCl and WebAssembly need a compiler to a get the machine code run by CPU, but the output of PNaCl is checked via NaCl verifier while nothing checks that the output of WebAssembly is safe machine code.

As the verifier for NaCl is likely to be an order magnitude smaller than a component in WebAssembly implementation that verifies and compiles the bytecode to the native code, PNaCl attack surface is much smaller.

View on HN

> nothing checks that the output of WebAssembly is safe machine code

By this line of reasoning, “nothing checks that the output of the JavaScript compiler is safe machine code”. Because that is essentially what WebAssembly is: like asm.js, it's just another kind of input to your JS VM.

And… well, you're right. It's the JIT's job to produce sensible code, and it's the browser's job to sandbox that well.

But what's wrong with that?

At least with WebAssembly it's a well-defined, small language that's easy to verify.

>nothing checks that the output of WebAssembly is safe machine code.

The JS/WASM VM does. If unsafe WASM code is allowed to execute, there is a bug in VM. VM must prevent semantically incorrect WASM from executing Control flow integrity and incorrect use of pointers are detected at load time. There are traps for invalid indexes, exceeding stack limits, invalid indexes in the index space.

This is not about unsafe WASM which should be rejected by verifier. This is about the raw machine output that the compiler generates from WASM. As with JIT for JS currently nothing verifies WASM compiler output. So a bug in the compiler may result in a WASM that passes the verifier to be translated into unsafe machine code.

Same thing applies to NaCl verifier. Bugs in verifier can cause problems. Verification or generation bugs are bug, not security weaknesses in the architecture.

(I should not need to mention this but compiling is form of verification).

NaCl verifier in practice is much simpler than WASM compiler leading to a significantly reduced attack surface.

This is not true. NEXE has different security boundaries enforced differently on each supported platform. You need to write disassembler for each supported instruction set and verify them. This is more complex task than generating correct code from wasm.

"Same thing applies to NaCl verifier. Bugs in verifier can cause problems. "

Not like with the other, though. You can statically verify NaCl stuff because it was designed for that to be easy. If WebAssembly doesn't do that, then it's a step down from NaCl at least on this risk. That it matters should be obvious given all the research by the kind of CompSci people that invented NaCl on eliminating that risk from the TCB. It's part of a larger concept where you make the things generating the risky code untrusted with the trusted checkers so simple they can be mathematically verified. Here's an example from a top group on NaCl:

http://www.cse.psu.edu/~gxt29/paper/rocksalt.pdf

I'm not worried about this too much as it will probably be some brilliant student's personal project in near future if it's not being researched already. A quick Google shows the Github has the full, C semantics with compiler (KCC) and a Javascript semantics at least has a prototype from 2015 of WebAssembly.

https://github.com/kframework/wasm-semantics

"...the verifier for NaCl is likely to be an order magnitude smaller than a component in WebAssembly implementation..."

Why is this so?

NaCL verifier is just a loop that essentially matches the instructions against a white list and checks their format and offsets. WebAssembly needs parser/linker/optimizer/assembler. Granted that the format is optimized for fast translation, but just the amount of code to support data structures in the implementation like maps, lists etc. must be big.

As in my other comment, something like that can be mathematically verified for correctness as well. That requires simplicity if one doesn't want to throw person-years of work at it w/ possibility of finding out it was impossible. My comment links to a formally-verified checker for NaCl as well.

https://news.ycombinator.com/item?id=14460649

NaCL also needs those things because it has to compile it's bytecode to machine code on multiple architectures. It's no different than webasm, just a different bytecode. A big advantage of webasm is that it's integrated into the existing javascript VM, that has already been sandboxed and battle hardened.

I believe that's PNaCl. NaCl just handles already-compiled machine code. But of course NaCl isn't portable, which is why PNaCl exists.

It would be possible to leverage a simple machine code verifier similar to NaCl's in a WebAssembly backend. Nobody does it right now, but there's been some work on taking WebAssembly as input to their Subzero PNaCl->NaCl compiler.

This.

Webassembly is an overcomplication. But, as always, I suppose we have to live with it.

Reply on news.ycombinator.com