一句话：在 Isabelle/HOL 中实现并机器化验证 WebAssembly 单子解释器，作为 Wasmtime 的模糊测试预言机，兼顾规范对应性与性能。
WebAssembly 官方 OCaml 参考解释器因性能不佳被 Wasmtime 放弃用作模糊测试预言机，而未经验证的预言机又难以保证与规范一致。本文提出 WasmRef-Isabelle：一个用 Isabelle/HOL 编写的 WebAssembly 单子解释器，并通过两步 refinement 证明其相对于 WasmCert-Isabelle 机械化形式化规范的正确性。该解释器已被部署到 Wasmtime 的持续集成基础设施中充当模糊测试预言机。实验表明其性能显著优于官方参考解释器，与工业级解释器 Wasmi 的 Rust debug 构建相当，在 Wasmtime 模糊测试基础设施中的吞吐量可与未经验证的预言机相比。此外，作者为 WasmCert-Isabelle 增加了对若干即将到来的 WebAssembly 特性的支持，并完整机器化了整数运算的数值语义，以增强其作为模糊测试预言机的实用性。
We present WasmRef-Isabelle, a monadic interpreter for WebAssembly written in Isabelle/HOL and proven correct with respect to the WasmCert-Isabelle mechanisation of WebAssembly. WasmRef-Isabelle has been adopted and deployed as a fuzzing oracle in the continuous integration infrastructure of Wasmtime, a widely used WebAssembly implementation. Previous efforts to fuzz Wasmtime against WebAssembly's official OCaml reference interpreter were abandoned by Wasmtime's developers after the reference interpreter exhibited unacceptable performance characteristics, which its maintainers decided not to fix in order to preserve the interpreter's close definitional correspondence with the official specification. With WasmRef-Isabelle, we achieve the best of both worlds - an interpreter fast enough to be useable as a fuzzing oracle that also maintains a close correspondence with the specification through a mechanised proof of correctness. We verify the correctness of WasmRef-Isabelle through a two-step refinement proof in Isabelle/HOL. We demonstrate that WasmRef-Isabelle significantly outperforms the official reference interpreter, has performance comparable to a Rust debug build of the industry WebAssembly interpreter Wasmi, and competes with unverified oracles on fuzzing throughput when deployed in Wasmtime's fuzzing infrastructure. We also present several new extensions to WasmCert-Isabelle which enhance WasmRef-Isabelle's utility as a fuzzing oracle: we add support for a number of upcoming WebAssembly features, and fully mechanise the numeric semantics of WebAssembly's integer operations.
@article{paperbot2005,
title = {WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly},
author = {Conrad Watt and Maja Trela and Peter Lammich and Florian Märkl},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591224}
}