Formal verification has had many successful applications to industry standards over the last few years, but an important question is whether formal verification can be included in standard design efforts. This paper presents the use of theorem-proving techniques for formal verification to define the WebAssembly language. The author participated in constructive discussions with the working group defining the WebAssembly language. He was able to specify and verify new features of the language as they were added, providing enormously effective feedback.
The paper targets an audience interested in what can be obtained by integrating formal verification into standard design. It includes three notable contributions.
First, the process of modeling WebAssembly language in Isabelle revealed a deficiency in the working group’s original paper about how a WebAssembly implementation interfaces with its host environment. Specifically, the possible non-determinism was not formally specified. The author fixes this problem and provides a fully mechanized proof.
Second, the author models the semantics of a WebAssembly program by defining a WebAssembly interpreter in Isabelle. In this way, he is able to prove execution properties of the WebAssembly program using an Isabelle specification of the interpreter. Moreover, this interpreter could be turned into an executable interpreter thanks to the Isabelle extraction mechanism for OCaml code. The author also tests the extracted executable interpreter, applying it to both theorem-proving techniques and standard testing techniques.
Finally, since it is essential to consider only correctly typed programs, the author defines a type checker for the WebAssembly language in Isabelle. He does not consider Isabelle’s tools for extracting a typing relation, but rather defines a type checker from scratch to match industry type checking implementations. He proves that this type checker is “sound and complete with respect to the inductive typing relation [extracted from this] mechanization.”