Scaling Instruction-Selection Verification against Authoritative ISA Semantics

Abstract

Secure, performant execution of untrusted code—as promised by WebAssembly (Wasm)—requires correct compilation to native code that enforces a sandbox. Errors in instruction selection can undermine the sandbox's guarantees, but prior verification work struggles to scale to the complexity of realistic industrial compilers.

We present Arrival, an instruction-selection verifier for the Cranelift production Wasm-to-native compiler. Arrival enables end-to-end, high-assurance verification while reducing developer effort. Arrival (1) automatically reasons about chains of instruction-selection rules, thereby reducing the need for developer-supplied intermediate specifications, (2) introduces a lightweight, efficient method for reasoning about stateful instruction-selection rules, and (3) automatically derives high-assurance machine code specifications.

Our work verifies nearly all AArch64 instruction-selection rules reachable from Wasm core. Furthermore, Arrival reduces the developer effort required: 60% of all specifications benefit from our automation, thereby requiring 2.6X fewer hand-written specifications than prior approaches. Arrival finds new bugs in Cranelift's instruction selection, and it is viable for integration into production workflows.