Are you talking about bugs or are you talking about inherent security vulnerabilities in the design?

Less "inherent vulnerabilities" than "If you're using a memory unsafe language (like C), the protections WASM gives you aren't enough to mitigate every possible vuln you might have had in your C code"

The WASM platform does provide some really cool protections, but it's not a silver bullet, you still need to fix your C code.

> The WASM platform does provide some really cool protections, but it's not a silver bullet, you still need to fix your C code.

I mean, the way you're phrasing it, that's true of every system. IIRC seL4 had a couple bugs where the code _and_ the formal model both got it wrong in the same way, and it therefore passed the proof.

The guarantees that wasm attempts to provide are that it's ok for me as a user to run random code in a wasm sandbox, rather than that code is inherently better at it's internal security by being in a sandbox.

ie. wasm doesn't attempt to make the developer's job any easier, other than making it more likely that users will be willing to run their code.

Like, I don't think my c code is any safer when I run it on a system with a hypervisor.

> IIRC seL4 had a couple bugs where the code _and_ the formal model both got it wrong in the same way, and it therefore passed the proof.

I haven't heard this one yet. How did they find it, then?