Maja Trela
Software engineer @ Jane Street
I studied Computer Science at University of Cambridge, where my love of formal verification, functional programming, and similar topics awakened. For my master's thesis I worked with Conrad Watt on verifying WasmRef-Isabelle, the results of which were incorporated into its associated paper. As of now I'm working as a software engineer at Jane Street.
WasmRef-Isabelle – or how to formally verify a not-slow interpreter with not-insane amount of effort
OBJECTIVES
- High-level strategy for formally verifying more efficient programs
- That proof automation in Isabelle/HOL is pretty cool
- That better tools keep lowering the barrier to practical formal verification
AUDIENCE
People with some interest in formal verification
DESCRIPTION
WasmRef-Isabelle is a WebAssembly interpreter written in Isabelle/HOL verified to be sound with respect to the WasmCert-Isabelle mechanisation of WebAssembly. Its main improvement on both the existing verified interpreter included in WasmCert-Isabelle and even the official (but unverified) WebAssembly reference interpreter is in performance – in fact, thanks to that, the Wasmtime (one of the main WebAssembly implementations) team adopted it as their fuzzing oracle.
So, how much direct effort does it take to achieve such a practical result in formal verification? Actually, not an insane amount. I'll talk about how we verified WasmRef-Isabelle as a two-step refinement proof, using the WasmCert-Isabelle interpreter as the springboard so to speak, in a single (one-year) master's thesis time.
←Back
