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