一句话：提出 Crocus，对 Cranelift 中 WebAssembly 到 aarch64 的指令降级规则进行轻量级模块化验证，复现并发现多个编译器缺陷。
语言级安全保证（如 WebAssembly 的模块运行时隔离）的强度取决于生成最终原生机器码的编译器。将语言级构造降级为 ISA 特定指令的过程可能引入违反安全保证的细微缺陷。本文提出 Crocus，一个对 Cranelift（生产级可重定向 Wasm 原生代码生成器）中指令降级规则进行轻量级、模块化验证的系统。作者使用 Crocus 验证了 ARM aarch64 后端中覆盖 WebAssembly 1.0 整数运算支持的降级规则。实验表明，Crocus 能够复现 3 个已知缺陷（包括一个严重度为 9.9/10 的 CVE），发现 2 个此前未知的缺陷以及一个未充分规定的编译器不变式，并帮助分析一个新缺陷的根本原因。
Language-level guarantees---like module runtime isolation for WebAssembly (Wasm)---are only as strong as the compiler that produces a final, native-machine-specific executable. The process of lowering language-level constructions to ISA-specific instructions can introduce subtle bugs that violate security guarantees. In this paper, we present Crocus, a system for lightweight, modular verification of instruction-lowering rules within Cranelift, a production retargetable Wasm native code generator. We use Crocus to verify lowering rules that cover WebAssembly 1.0 support for integer operations in the ARM aarch64 backend. We show that Crocus can reproduce 3 known bugs (including a 9.9/10 severity CVE), identify 2 previously-unknown bugs and an underspecified compiler invariant, and help analyze the root causes of a new bug.
@inproceedings{VanHattumPFSB24,
title = {Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection},
author = {Alexa VanHattum and Monica Pardeshi and Chris Fallin and Adrian Sampson and Fraser Brown},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3617232.3624862}
}