Mechanising and verifying the WebAssembly specification
View / Open Files
Authors
Publication Date
2018-01-08Journal Title
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Conference Name
CPP '18: Certified Proofs and Programs
ISBN
9781450355865
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Watt, C. (2018). Mechanising and verifying the WebAssembly specification. Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs https://doi.org/10.1145/3167082
Abstract
WebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js and Native Client. The WebAssembly working group has incorporated formal techniques into the development of the language, but their efforts so far have focussed on pen and paper formal specification.
We present a mechanised Isabelle specification for the WebAssembly language, together with a verified executable interpreter and type checker. Moreover, we present a fully mechanised proof of the soundness of the WebAssembly type system, and detail how our work on this proof has exposed several issues with the official WebAssembly specification, influencing its development. Finally, we give a brief account of our efforts in performing differential fuzzing of our interpreter against industry implementations.
Sponsorship
EPSRC (EP/K008528/1)
EPSRC (1790117)
Identifiers
External DOI: https://doi.org/10.1145/3167082
This record's URL: https://www.repository.cam.ac.uk/handle/1810/274174
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved