一句话：提出 Arrival，为 Cranelift 生产级 Wasm 编译器验证指令选择，自动化规则链与有状态规则推理，显著减少人工规约。
WebAssembly 要求不受信代码在原生执行时仍受沙箱保护，因此 Wasm 到原生的编译必须正确，而指令选择的错误会破坏沙箱保证。此前验证工作难以扩展到真实工业编译器的复杂度。本文提出 Arrival，一个针对 Cranelift（生产级 Wasm 到原生编译器）的指令选择验证器，支持端到端高保障验证并降低开发者负担。Arrival 的三项技术是：自动推理指令选择规则链，减少开发者提供的中间规约；提出轻量高效的方法推理有状态指令选择规则；自动派生高保障的机器码规约。作者验证了 Wasm 核心可达的几乎所有 AArch64 指令选择规则，60% 的规约受益于自动化，相比先前方法手写规约减少 2.6 倍。Arrival 还发现了 Cranelift 指令选择中的新缺陷，并具备集成到生产工作流的可行性。
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: 60 % of all specifications benefit from our automation, thereby requiring 2.6 × 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.
@article{paperbot2893,
title = {Scaling Instruction-Selection Verification against Authoritative ISA Semantics},
author = {Michael McLoughlin and Ashley Sheng and Chris Fallin and Bryan Parno and Fraser Brown and Alexa VanHattum},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3764383}
}