Conrad Watt
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.
- 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.Google Scholar
- 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) . ACM, New York, NY, USA, 87–100. Google ScholarDigital Library
- CakeML project. 2017. CakeML Projects. (2017). Retrieved October 7, 2017 from https://cakeml.org/projectsGoogle Scholar
- Ethereum Group. 2017. eWASM. (2017). Retrieved October 7, 2017 from https://github.com/ewasmGoogle Scholar
- Google. 2017. Welcome to Native Client. (2017). Retrieved October 7, 2017 from https://developer.chrome. com/native-clientGoogle Scholar
- 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 WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) . ACM, New York, NY, USA, 185–200. Google ScholarDigital Library
- 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/bbb26c42b62096baff86089767531c3b1f108a85/ papers/pldi2017.pdfGoogle Scholar
- David Herman, Luke Wagner, and Alon Zakai. 2014. asm.js. (August 2014). Retrieved October 7, 2017 from http://asmjs. org/spec/latestGoogle Scholar
- Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In 1st Workshop on Trusted Smart Contracts .Google Scholar
- 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. Google ScholarDigital Library
- Peter J Knaggs. 1993. Towards a Formal Forth. (September 1993). Retrieved October 7, 2017 from http://www.rigwit. co.uk/papers/formal2.pdfGoogle Scholar
- 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 Symposium on Principles of Programming Languages (POPL ’14) . ACM, New York, NY, USA, 179–191. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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. polymorphism and inheritance. In Proc. 18-th EuroForth Conference .Google Scholar
- 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.Google Scholar
- 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/563Google Scholar
- 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/772d87705ea4786c0d44d41902097e91cf31f82bGoogle Scholar
- 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/563Google Scholar
- TC39. 2017a. Memory Model. (September 2017). Retrieved October 7, 2017 from https://tc39.github.io/ecma262/ #sec-memory-modelGoogle Scholar
- TC39. 2017b. SIMD.js specification v0.9. (April 2017). Retrieved October 7, 2017 from http://tc39.github.io/ ecmascript_simd/Google Scholar
- Conrad Watt. 2017a. Conrad Watt. (October 2017). Retrieved November 27, 2017 from http://www.cl.cam.ac.uk/~caw77/Google Scholar
- Conrad Watt. 2017b. Crash in wasm-opt on certain optimisation levels. (August 2017). Retrieved October 7, 2017 from https://github.com/WebAssembly/binaryen/issues/1149Google Scholar
- WebAssembly Community Group. 2017a. Binaryen. (October 2017). Retrieved October 7, 2017 from https://github.com/ WebAssembly/binaryenGoogle Scholar
- WebAssembly Community Group. 2017b. Instructions. (September 2017). Retrieved October 7, 2017 from https: //webassembly.github.io/spec/binary/instructions.htmlGoogle Scholar
- WebAssembly Community Group. 2017c. WebAssembly. (2017). Retrieved October 7, 2017 from http://webassembly. orgGoogle Scholar
- WebAssembly Community Group. 2017d. WebAssembly. (October 2017). Retrieved October 7, 2017 from https:// github.com/WebAssembly/spec/tree/master/interpreterGoogle Scholar
- WebAssembly Community Group. 2017e. WebAssembly. (October 2017). Retrieved October 7, 2017 from https: //github.com/WebAssemblyGoogle Scholar
- WebAssembly Community Group. 2017f. WebAssembly Specification. (September 2017). Retrieved October 7, 2017 from https://webassembly.github.io/spec/Google Scholar
- 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. Google ScholarDigital Library
- 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/Google Scholar
Index Terms
- Mechanising and verifying the WebAssembly specification
Recommendations
Programming and verifying a declarative first-order prover in Isabelle/HOL
We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
Comments