Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Mechanising and verifying the WebAssembly specification
Watt C.  CPP 2018 (Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Los Angeles, CA, Jan 8-9, 2018)53-65.2018.Type:Proceedings
Date Reviewed: Jul 11 2018

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 WebAssembly language is the first real cross-party effort to offer a modern, more realistic compilation target for web browsers (instead of the JavaScript language generated from C/C++ that targets the asm.js subset). JavaScript is routinely used as a low-level compilation target for web browsers, though it was never designed for this and cannot achieve the performance of native compilation. Several companies are behind the WebAssembly language, including Google, Microsoft, Apple, and Mozilla, and have committed to replacing JavaScript with WebAssembly in their respective browsers in an effort to provide better user experience in terms of both performance and security.

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.”

Reviewer:  Santiago Escobar Review #: CR146138 (1809-0512)
Bookmark and Share
  Editor Recommended
Featured Reviewer
 
 
Semantics Of Programming Languages (F.3.2 )
 
 
Mechanical Verification (F.3.1 ... )
 
 
Semantics (D.3.1 ... )
 
 
Verification (D.4.5 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Semantics Of Programming Languages": Date
Contractions in comparing concurrency semantics
Kok J. (ed), Rutten J. Theoretical Computer Science 76(2-3): 179-222, 2001. Type: Article
Aug 1 1991
Abstract language design
Bradley L. Theoretical Computer Science 77(1-2): 5-26, 1990. Type: Article
Nov 1 1991
Determinism → (event structure isomorphism = step sequence equivalence)
Vaandrager F. Theoretical Computer Science 79(2): 275-294, 1991. Type: Article
Dec 1 1991
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy