Elamur Research⌕
☰
home / papers / 2018 / Mechanising and Verifying the WebAssembly Specification

Mechanising and Verifying the WebAssembly Specification

Paper · 2018 · Conrad Watt

Summary

WebAssembly is a low-level bytecode language supported by all major browsers and intended as a universal compilation target for the web. Its designers wrote a formal semantics on paper, but that semantics had never been mechanised, and its claimed type-soundness properties had never been proven. Watt formalises WebAssembly's central type system and the rules governing how its programs execute in the Isabelle proof assistant. Building on this model, he machine-checks the soundness of the type system and develops a separately verified executable interpreter and type checker. The official OCaml reference interpreter supplies parsing and linking. Constructing the proof exposed several flaws in the official specification. Some made the type system unsound, including a problem in how modules interact with the host environment. The specification authors corrected these flaws. The interpreter was then validated against the official conformance tests and through differential fuzzing against commercial engines. According to the paper, this is the first mechanised formalisation of the full core language and the first complete soundness proof. It demonstrates that deep mechanised verification can directly improve an industrial language standard.

Key points

  • The development contains about 11,000 lines of Isabelle code, of which about 700 lines specify the language itself. It is publicly released under a BSD-style license.
  • The specification defines 171 concrete opcodes, which map onto the 28 abstract operations used in Haas et al. (2017).
  • Soundness bugs found during the proof, including one in the host-environment interface, were fixed in the official WebAssembly specification.
  • The verified interpreter passes all core conformance tests in the WebAssembly repository.
  • Differential fuzzing used CSmith and the Binaryen toolchain. It found no bugs in commercial engines, but it uncovered a crash in Binaryen, which was then fixed. The project structure follows the approach of JSCert.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Conrad Watt. 2018. Mechanising and Verifying the WebAssembly Specification. CPP 2018.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{watt2018mechanising,
  title = {{Mechanising and Verifying the WebAssembly Specification}},
  author = {Conrad Watt},
  booktitle = {CPP 2018},
  year = {2018},
  doi = {10.1145/3167082},
  url = {https://doi.org/10.1145/3167082}
}

References

31 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. Springer Berlin Heidelberg, Berlin, Heidelberg, 283–307. https://doi.org/10.1007/978-3-662-46669-8_12 — [doi:10.1007/978-3-662-46669-8_12](https://doi.org/10.1007/978-3-662-46669-8_12) ↗
  2. Martin Bodin, Arthur Chargueraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. 2014. A Trusted Mechanised JavaScript Specification. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). A… — [doi:10.1145/2535838.2535876](https://doi.org/10.1145/2535838.2535876) find
  3. CakeML Projects. (2017). Retrieved October 7, 2017 from https://cakeml.org/projects ↗
  4. Ethereum Group. 2017. eWASM. (2017). Retrieved October 7, 2017 from https://github.com/ewasm ↗
  5. Google. 2017. Welcome to Native Client. (2017). Retrieved October 7, 2017 from https://developer.chrome.com/native-client Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017a. Bringing the Web Up to Speed with Web… ↗
  6. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017b. Bringing the Web Up to Speed with WebAssembly. (March 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/spec/blob/bbb26c42b62096baff860897675… ↗
  7. David Herman, Luke Wagner, and Alon Zakai. 2014. asm.js. (August 2014). Retrieved October 7, 2017 from http://asmjs.org/spec/latest Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In 1st Workshop on Trusted Smart Contracts. ↗
  8. Gerwin Klein and Tobias Nipkow. 2006. A Machine-checked Model for a Java-like Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang. Syst. 28, 4 (July 2006), 619–695. https://doi.org/10.1145/1146809.1146811 — [doi:10.1145/1146809.1146811](https://doi.org/10.1145/1146809.1146811) ↗
  9. Peter J Knaggs. 1993. Towards a Formal Forth. (September 1993). Retrieved October 7, 2017 from http://www.rigwit.co.uk/papers/formal2.pdf Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Sy… — [doi:10.1145/2535838.2535841](https://doi.org/10.1145/2535838.2535841) ↗
  10. Andreas Lochbihler and Lukas Bulwahn. 2011. Animating the Formalised Semantics of a Java-like Language. In Proceedings of the Second International Conference on Interactive Theorem Proving (ITP’11). Springer-Verlag, Berlin, Heidelberg, 216–232. http://dl.acm.org/citation.cfm?id=2033939.2033958 ↗
  11. Jaanus Poial. 1990. Algebraic Specification of Stack Effects for Forth Programs. In Forml Conference Proceedings (Forml 1990). The Forth Interest Group, San Jose, CA, USA, 282– 290. find
  12. Jaanus Poial. 2002. Stack effect calculus with typed wildcards, polymorphism and inheritance. In Proc. 18-th EuroForth Conference. find
  13. James F. Power and David Sinclair. 2004. A Formal Model of Forth Control Words in the Pi-Calculus. J. UCS 10, 9 (2004), 1272–1293. https://doi.org/10.3217/jucs-010-09-1272 — [doi:10.3217/jucs-010-09-1272](https://doi.org/10.3217/jucs-010-09-1272) ↗
  14. Andreas Rossberg. 2017a. [spec] Fix and clean up invariants for host functions. (September 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/spec/pull/563 ↗
  15. Andreas Rossberg. 2017b. [spec] Fix and clean up invariants for host functions. (September 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/spec/commit/772d87705ea4786c0d44d41902097e91cf31f82b ↗
  16. Andreas Rossberg. 2017c. [spec] Fix and clean up invariants for host functions. (September 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/spec/pull/563 ↗
  17. TC39. 2017a. Memory Model. (September 2017). Retrieved October 7, 2017 from https://tc39.github.io/ecma262/\#sec-memory-model ↗
  18. TC39. 2017b. SIMD.js specification v0.9. (April 2017). Retrieved October 7, 2017 from http://tc39.github.io/ecmascript_simd/ ↗
  19. Conrad Watt. 2017a. Conrad Watt. (October 2017). Retrieved November 27, 2017 from http://www.cl.cam.ac.uk/~caw77/ ↗
  20. Conrad Watt. 2017b. Crash in wasm-opt on certain optimisation levels. (August 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/binaryen/issues/1149 ↗
  21. WebAssembly Community Group. 2017a. find
  22. Binaryen. (October 2017). Retrieved October 7, 2017 from https://github.com/ ↗
  23. WebAssembly/binaryen WebAssembly Community Group. 2017b. find
  24. Instructions. (September 2017). Retrieved October 7, 2017 from https://webassembly.github.io/spec/binary/instructions.html WebAssembly Community Group. 2017c. ↗
  25. WebAssembly. (2017). Retrieved October 7, 2017 from http://webassembly.org WebAssembly Community Group. 2017d. ↗
  26. WebAssembly. (October 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/spec/tree/master/interpreter ↗
  27. WebAssembly Community Group. 2017e. find
  28. WebAssembly. (October 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly WebAssembly Community Group. 2017f. ↗
  29. WebAssembly Specification. (September 2017). Retrieved October 7, 2017 from https://webassembly.github.io/spec/ ↗
  30. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’11). ACM, New York, NY, USA, 283–294. https://doi.org/10.1145/1993498.1993532 ↗
  31. Alon Zakai and Robert Nyman. 2013. Gap between asm.js and native performance gets even narrower with float32 optimizations. (December 2013). Retrieved October 7, 2017 from https://hacks.mozilla.org/2013/12/20/ ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/watt-2018-mechanising-verifying-webassembly-specification/