back
2 comments
Very cool, this part is neat:

> ...We present LibSignal*, a brand new, verified implementation of the Signal protocol in WebAssembly, that can be readily used by messaging applications like WhatsApp, Skype, and Signal.

I'm particularly interested in WASM for desktop apps (i.e Photoshop on the browser) but this looks very promising in the security side of things.

The paper is way over my head, but is there any work on WASM security?

For timing side-channels specifically, they basically assume them away. For example, they say that WASM guarantees constant-time 64-bit arithmetic, but conflate providing the semantics of 64-bit arithmetic with how it's actually performed on the hardware. An odd claim considering in the previous paragraph they show how Emscripten has to synthesize 64-bit arithmetic using unsafe 32-bit primitives, as-if no WASM engine would ever do the same or something equally problematic.

They play semantic games elsewhere. They say that there's no undefined behavior in WASM therefore it's all good. Well, there may not be undefined behavior but there is unspecified behavior, both explicit and implicit, which is functionally equivalent. And by making assumptions about unspecified behavior based on observations of the few existing implementations they (and others) recapitulate the very same judgments that made unspecified and undefined behavior problematic in C in the first place.

So many newer languages and advocates simply conflate the absence of the phrase "undefined behavior" with the absence of the underlying traps. Some of them may be gone, but not all of them; they don't disappear just because they're not explicitly identified as such.