Andreas Haas
JF Bastien
ABSTRACT
The maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D visualization, audio and video software, and games. With that, efficiency and security of code on the Web has become more important than ever. Yet JavaScript as the only built-in language of the Web is not well-equipped to meet these requirements, especially as a compilation target.
Engineers from the four major browser vendors have risen to the challenge and collaboratively designed a portable low-level bytecode called WebAssembly. It offers compact representation, efficient validation and compilation, and safe low to no-overhead execution. Rather than committing to a specific programming model, WebAssembly is an abstraction over modern hardware, making it language-, hardware-, and platform-independent, with use cases beyond just the Web. WebAssembly has been designed with a formal semantics from the start. We describe the motivation, design and formal semantics of WebAssembly and provide some preliminary experience with implementations.
- Activex controls. https://msdn.microsoft.com/en-us/ library/aa751968(v=vs.85).aspx. Accessed: 2016-11- 14.Google Scholar
- Adobe Shockwave Player. https://get.adobe.com/ shockwave/. Accessed: 2016-11-14.Google Scholar
- ART and Dalvik. https://source.android.com/devices/ tech/dalvik/. Accessed: 2016-11-14.Google Scholar
- asm.js. http://asmjs.org. Accessed: 2016-11-08.Google Scholar
- Indexed Database API. https://www.w3.org/TR/IndexedDB/. Accessed: 2016-11-08.Google Scholar
- LEB128. https://en.wikipedia.org/wiki/LEB128. Accessed: 2016-11-08.Google Scholar
- PolyBenchC: the polyhedral benchmark suite. http://web. cs.ucla.edu/~pouchet/software/polybench/. Accessed: 2017-03-14.Google Scholar
- Scimark 2.0. http://math.nist.gov/scimark2/. Accessed: 2017-03-15.Google Scholar
- Unity benchmarks. http://beta.unity3d.com/jonas/ benchmark2015/. Accessed: 2017-03-15.Google Scholar
- P. Akritidis, M. Costa, M. Castro, and S. Hand. Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. In Proceedings of the 18th Conference on USENIX Security Symposium, SSYM’09, pages 51–66, Berkeley, CA, USA, 2009. USENIX Association. Google ScholarDigital Library
- J. Ansel, P. Marchenko, U. Erlingsson, E. Taylor, B. Chen, D. L. Schuff, D. Sehr, C. L. Biffle, and B. Yee. Languageindependent sandboxing of just-in-time compilation and selfmodifying code. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 355–366, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
- C. Click and M. Paleczny. A simple graph-based intermediate representation. SIGPLAN Not., 30(3):35–49, Mar. 1995. Google ScholarDigital Library
- J. Criswell, A. Lenharth, D. Dhurjati, and V. Adve. Secure Virtual Architecture: A safe execution environment for commodity operating systems. SIGOPS Oper. Syst. Rev., 41(6):351–366, Oct. 2007. Google ScholarDigital Library
- N. G. de Bruijn. Lambda calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34:381–392, 1972.Google ScholarCross Ref
- D. Dean, E. Felten, and D. Wallach. Java security: from HotJava to Netscape and beyond. In Symposium on Security and Privacy. IEEE Computer Society Press, 1996. Google ScholarDigital Library
- J. Devietti, C. Blundell, M. M. K. Martin, and S. Zdancewic. HardBound: Architectural support for spatial safety of the C programming language. SIGPLAN Not., 43(3):103–114, Mar. 2008. Google ScholarDigital Library
- D. Dhurjati, S. Kowshik, and V. Adve. SAFECode: Enforcing alias analysis for weakly typed languages. SIGPLAN Not., 41(6):144–157, June 2006. Google ScholarDigital Library
- A. Donovan, R. Muth, B. Chen, and D. Sehr. PNaCl: Portable native client executables. Technical report, 2010.Google Scholar
- A. Gal, C. W. Probst, and M. Franz. Complexity-based denial of service attacks on mobile-code systems. Technical Report 04-09, School of Information and Computer Science, University of California, Irvine, Irvine, CA, April 2004.Google Scholar
- M. Grimmer, R. Schatz, C. Seaton, T. Würthinger, and H. Mössenböck. Memory-safe execution of C on a Java VM. In Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, PLAS’15, pages 16–27, New York, NY, USA, 2015. ACM. Google ScholarDigital Library
- D. Gudeman. Representing type information in dynamically typed languages. Technical Report 93-27, Department of Computer Science, University of Arizona, Phoenix, Arizona, October 1993.Google Scholar
- U. Hölzle, C. Chambers, and D. Ungar. Debugging optimized code with dynamic deoptimization. SIGPLAN Not., 27(7):32–43, July 1992. Google ScholarDigital Library
- T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In Proceedings the USENIX Annual Technical Conference, ATEC ’02, pages 275–288, Berkeley, CA, USA, 2002. USENIX Association. Google ScholarDigital Library
- C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the International Symposium on Code Generation and Optimization, CGO ’04, Palo Alto, California, Mar 2004. Google ScholarDigital Library
- X. Leroy. Java bytecode verification: Algorithms and formalizations. J. Autom. Reason., 30(3-4):235–269, Aug. 2003. Google ScholarDigital Library
- X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy, and J. Vouillon. The OCaml system. INRIA, 2016.Google Scholar
- T. Lindholm, F. Yellin, G. Bracha, and A. Buckley. The Java Virtual Machine Specification (Java SE 8 Edition). Technical report, Oracle, 2015. Google ScholarDigital Library
- G. Morrisett, D. Tarditi, P. Cheng, C. Stone, P. Cheng, P. Lee, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In In Workshop on Compiler Support for Systems Software, 1996.Google Scholar
- G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to Typed Assembly Language. ACM TOPLAS, 21(3):527– 568, May 1999. Google ScholarDigital Library
- S. Nagarakatte, M. M. K. Martin, and S. Zdancewic. WatchdogLite: Hardware-accelerated compiler-based pointer checking. In Proceedings of Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO ’14, pages 175:175–175:184, New York, NY, USA, 2014. ACM. Google ScholarDigital Library
- S. Nagarakatte, J. Zhao, M. M. Martin, and S. Zdancewic. SoftBound: Highly compatible and complete spatial memory safety for C. SIGPLAN Not., 44(6):245–258, June 2009. Google ScholarDigital Library
- G. C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’97, pages 106–119, New York, NY, USA, 1997. ACM. Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proceedings of the 11th International Conference on Compiler Construction, CC ’02, pages 213– 228, London, UK, UK, 2002. Google ScholarDigital Library
- G. C. Necula, S. McPeak, and W. Weimer. CCured: Type-safe retrofitting of legacy code. SIGPLAN Not., 37(1):128–139, Jan. 2002. Google ScholarDigital Library
- B. Pierce. Types and Programming Languages. The MIT Press, Cambridge, Massachusetts, USA, 2002. Google ScholarDigital Library
- G. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17–139, 2004.Google ScholarCross Ref
- Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC’97), Amsterdam, The Netherlands, June 1997.Google Scholar
- Y. Shi, K. Casey, M. A. Ertl, and D. Gregg. Virtual machine showdown: Stack versus registers. ACM Transactions on Architecture and Code Optimizations, 4(4):2:1–2:36, Jan. 2008. Google ScholarDigital Library
- R. F. Strk and J. Schmid. Java bytecode verification is not possible (extended abstract). In Formal Methods and Tools for Computer Science (Proceedings of Eurocast 2001, pages 232–234, 2001.Google Scholar
- K. Wang, Y. Lin, S. M. Blackburn, M. Norrish, and A. L. Hosking. Draining the Swamp: Micro virtual machines as a solid foundation for language development. In 1st Summit on Advances in Programming Languages, volume 32 of SNAPL ’15, pages 321–336, Dagstuhl, Germany, 2015.Google Scholar
- A. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115, 1994. Google ScholarDigital Library
- B. Yee, D. Sehr, G. Dardyk, B. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native Client: A sandbox for portable, untrusted x86 native code. In IEEE Symposium on Security and Privacy, Oakland ’09, IEEE, 3 Park Avenue, 17th Floor, New York, NY 10016, 2009. Google ScholarDigital Library
- A. Zakai. Emscripten: An LLVM-to-JavaScript compiler. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’11, pages 301–312, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
Index Terms
- Bringing the web up to speed with WebAssembly
Recommendations
Bringing the web up to speed with WebAssembly
PLDI '17The maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D visualization, audio and video software, and games. With that, efficiency and security of code on the Web has become more important ...
Weakening WebAssembly
WebAssembly (Wasm) is a safe, portable virtual instruction set that can be hosted in a wide range of environments, such as a Web browser. It is a low-level language whose instructions are intended to compile directly to bare hardware. While the initial ...
Comments