Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Best of 2016 Recommended by Editor Recommended by Reviewer Recommended by Reader
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
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?
Other reviews under "Semantics Of Programming Languages": Date
Bit-precise procedure-modular termination analysis
Chen H., David C., Kroening D., Schrammel P., Wachter B.  ACM Transactions on Programming Languages and Systems 40(1): 1-38, 2018. Type: Article
Apr 27 2018
Repairing sequential consistency in C/C++11
Lahav O., Vafeiadis V., Kang J., Hur C., Dreyer D.  PLDI 2017 (Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, Spain,  Jun 18-23, 2017) 618-632, 2017. Type: Proceedings
Apr 26 2018
 Differential hybrid games
Platzer A.  ACM Transactions on Computational Logic 18(3): 1-44, 2017. Type: Article
Mar 22 2018

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2018 ThinkLoud, Inc.
Terms of Use
| Privacy Policy