The challenge of compiling for verified architectures

Posted Oct 8, 2023 5:04 UTC (Sun) by ibukanov (subscriber, #3942)
In reply to: The challenge of compiling for verified architectures by roc
Parent article: The challenge of compiling for verified architectures

Checks at runtime can be bypassed via a speculation, checks in the verifier cannot. Some runtime checks can be protected against speculative leaks, but V8 implementation of JS and Wasm, for example, gave up on that.

So Wasm sandbox requires too many dynamic checks to hope for reliable practical protection against SPECTRE and friends. EBP implementation in Linux, by reducing the number of runtime checks and constraining the code sufficiently, still managed to provide the protection against known attacks. Hence ability to provide practical protection against speculative leaks is a useful criterion to classify.

The challenge of compiling for verified architectures

Posted Oct 8, 2023 7:06 UTC (Sun) by Cyberax (✭ supporter ✭, #52523) [Link]

> Checks at runtime can be bypassed via a speculation, checks in the verifier cannot.

Does that include new and fancy features like iterators?

The challenge of compiling for verified architectures

Posted Oct 8, 2023 9:57 UTC (Sun) by roc (subscriber, #30627) [Link] (1 responses)

Looks to me like Wasmtime is still "hoping for reliable practical protection against SPECTRE and friends".
https://bytecodealliance.org/articles/security-and-correc...

I still think this is a poor way to draw a line between "sandbox" and "verifier". If Spectre vulnerabilities are found in eBPF will it cease to be a verifier and become a sandbox? That doesn't make sense to me.

The challenge of compiling for verified architectures

Posted Oct 8, 2023 12:57 UTC (Sun) by ibukanov (subscriber, #3942) [Link]

Presently all found speculation bugs have been promptly addressed in BPF while Wasm implementations continue to hope. Yes, this difference is poorly defined and probably cannot be formalized. Yet it is clear that it is affected by the nature of checks that has to be done at runtime.