Hacker News new | ask | show | jobs
by slimsag 915 days ago
Formally verified C code, or WASM[0]

[0] https://news.ycombinator.com/item?id=38613031

1 comments

WASM is a funny case and I don't agree that it's safe.

When people say WASM is "safe" in this sense what they mean is that it won't corrupt your browser process (or other wasm runtime). That's a useful guarantee! But that's sandboxing, not memory-safety as a language property. You can sandbox C too, that doesn't make C a memory-safe language.

As far as I know you can still trigger unsafe access to the WASM heap, and therefore many kinds of of attacks still work. They don't "break out" but also, lots of valuable data or controllable user behavior is in-heap anyway.

Or, for an even more analogous example, see Google's pNaCl which was a native compilation target that provided many of the same security guarantees as wasm does while avoiding the need for complex JITs. pNaCl utilized a set of rules about control flow transitions and address formation which were enforced by a verifier to allow direct native code execution.
Such a shame this didn’t take off. Couldn’t LLVM in theory be made to target pNaCL instructions?