WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Watch a 17-minute video presentation from the PLDI 2023 conference introducing WasmRef-Isabelle, a verified monadic interpreter for WebAssembly. Learn how this Isabelle/HOL-based interpreter, proven correct against the WasmCert-Isabelle mechanization, has been adopted as a fuzzing oracle in Wasmtime's continuous integration. Discover how WasmRef-Isabelle achieves both performance and specification correspondence, outperforming the official reference interpreter while maintaining correctness through a mechanized proof. Explore the two-step refinement proof process, performance comparisons with other interpreters, and extensions to WasmCert-Isabelle that enhance its utility as a fuzzing oracle. Gain insights into theorem proving, refinement techniques, and virtual machine implementation for WebAssembly.
Syllabus
[PLDI'23] WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
Taught by
ACM SIGPLAN
Related Courses
Future Possibilities for .NET Core and WASI - WebAssembly on the ServerMicrosoft via YouTube Introduction to WebAssembly and waSCC - Secure Capabilities for Cloud-Native Applications
Rawkode Academy via YouTube Doing Server Side WebAssembly the Hard Way
Linux Foundation via YouTube Security and Correctness in Wasmtime
Linux Foundation via YouTube Getting Started with AI and WebAssembly
Linux Foundation via YouTube