WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
summary
A verified monadic interpreter for WebAssembly implemented in Isabelle/HOL and proven via a two-step refinement proof against WasmCert-Isabelle, extracted to an imperative implementation and deployed as a fuzzing oracle in Wasmtime’s CI since March; it removes the reference interpreter’s quadratic evaluation cost for deeply nested blocks, runs orders of magnitude faster than the OCaml reference in those cases, matches a Rust Wasmi debug build in speed, and competes with unverified oracles on fuzzing throughput while adding mechanised integer semantics and new feature support.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:03WebAssembly context
- 2:06Fuzzing oracle challenge
- 3:50WasmRef-Isabelle solution
- 5:16Soundness property extraction
- 6:17Refinement proof technique
- 7:43Monadic interpreter steps
- 9:57Automation in proofs
- 11:00Performance results
- 11:45Future work
- 12:50Q&A
related talks
19mUpdating WasmCert-Isabelle to WebAssembly 2.0
29mVerification of WebAssembly Features
30mMechanising WebAssembly Well?
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
30mCertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
01h 08mOn WebAssembly
29mWasocaml: a compiler from OCaml to WebAssembly