2025/10/09 by Michael McLoughlin, A. Sheng, Chris Fallin +3 · 2 voices
Computer Science · #Security and Verification in Computing #Logic, programming, and type systems #Software Testing and Debugging Techniques
paper · doi:10.1145/3764383
openalex publication_date 2025/10/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/17
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 develop-er-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: <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mn>60</mml:mn> <mml:mi mathvariant="normal">%</mml:mi> </mml:math> of all specifications benefit from our automation, thereby requiring <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mn>2.6</mml:mn> <mml:mo>×</mml:mo> </mml:math> 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.