AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We found that post-order ASTs decode and verify faster than pre-order ASTs, but that the stack machine, which can be seen as a generalization of the post-order format, more extended to multi-value support and allowed even more space optimizations

Bringing the web up to speed with WebAssembly.

PLDI, no. 12 (2018): 185-200

Cited by: 165|Views252
EI

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...More

Code:

Data:

0
Introduction
  • The Web began as a simple document exchange network but has become the most ubiquitous application platform ever, accessible across a vast array of operating systems and

    Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed foPptohnreerorvmtfpuhidilrselesodciofifiittnahrttatsioototncrmpooacpankioegetshmedea.irgmfieiCrtsnaetoolrptopcamrgiyhaeara.dlirCegdaoohcdprotvydpsraiiisegfntshroitotbrasfugfpttoehaerdrittarhfoodinrrrd-dap-plprlaotaohfirrftttaytyohtcriocsccmowoopmpomorminkepeefsnoroctrnsbiapoeelefnaartsdhrtovsinsatahnowltiafoosgrrtkenhcmaloianssutdssirwtctohbeoaoemtrahckounonspdmeoieritsesuhdbgs.eertFaaonrfbrutteehaldillslhwocnoitoithnhtteiaocoruteuritsaeofenednsde,.
  • Thanks to the type system (Section 4), the layout of the operand stack can be statically determined at any point in the code, so that actual implementations can compile the data flow between instructions directly without ever materializing the operand stack.The stack organization is merely a way to achieve a compact program representation, as it has been shown to be smaller than a register machine [38].2
Highlights
  • The Web began as a simple document exchange network but has become the most ubiquitous application platform ever, accessible across a vast array of operating systems and
  • Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed foPptohnreerorvmtfpuhidilrselesodciofifiittnahrttatsioototncrmpooacpankioegetshmedea.irgmfieiCrtsnaetoolrptopcamrgiyhaeara.dlirCegdaoohcdprotvydpsraiiisegfntshroitotbrasfugfpttoehaerdrittarhfoodinrrrd-dap-plprlaotaohfirrftttaytyohtcriocsccmowoopmpomorminkepeefsnoroctrnsbiapoeelefnaartsdhrtovsinsatahnowltiafoosgrrtkenhcmaloianssutdssirwtctohbeoaoemtrahckounonspdmeoieritsesuhdbgs.eertFaaonrfbrutteehaldillslhwocnoitoithnhtteiaocoruteuritsaeofenednsde
  • We found that post-order ASTs decode and verify faster than pre-order ASTs, but that the stack machine, which can be seen as a generalization of the post-order format, more extended to multi-value support and allowed even more space optimizations
  • Code Specialization While base can be stored in a dedicated machine register for quick access, a JIT compiler can be even more aggressive and specialize the machine code generated for a module to a specific memory base, embedding the base address as a constant directly into the code, freeing a register
  • Code Caching While implementors have spent a lot of resources improving compilation speed of JITs to reduce cold startup time of WebAssembly, we expect that warm startup time will become important as users will likely visit the same Web pages repeatedly
Results
  • The dynamic signature check protects integrity of the execution environment; a successful signature check ensures that a single machine-level indirect jump to the compiled code of the target function is safe.
  • This implies the absence of type safety violations such as invalid calls or illegal accesses to locals, it guarantees memory safety, and it ensures the inaccessibility of code addresses or the call stack.
  • The embedder defines how modules are loaded, how imports and exports between modules are resolved, provides foreign functions to accomplish I/O and timers, and specifies how WebAssembly traps are handled.
  • In the work the primary use case has been the Web and JavaScript embedding, so these mechanisms are implemented in terms of JavaScript and Web APIs. JavaScript API In the browser, WebAssembly modules can be loaded, compiled and invoked through a JavaScript API.
  • Each instruction t.load a o k with type t, alignment a, static offset o and dynamic address k represents a read of the memory at smem(i, k + o, |t|).
  • Code Specialization While base can be stored in a dedicated machine register for quick access, a JIT compiler can be even more aggressive and specialize the machine code generated for a module to a specific memory base, embedding the base address as a constant directly into the code, freeing a register.
  • Parallel Compilation Since both V8 and SpiderMonkey implement ahead-of-time compilation, it is a clear performance win to parallelize compilation of WebAssembly modules, dispatching individual functions to different threads.
Conclusion
  • Code Caching While implementors have spent a lot of resources improving compilation speed of JITs to reduce cold startup time of WebAssembly, the authors expect that warm startup time will become important as users will likely visit the same Web pages repeatedly.
  • In comparison to typed intermediate languages, typed assembly languages, and safe “C” machines, WebAssembly radically reduces the scope of responsibility for the VM: it is not required to enforce the type system of the original program at the granularity of individual objects; instead it must only enforce memory safety at the much coarser granularity of a module’s memory.
Related work
  • The most direct precursors of WebAssembly are (P)NaCl [42, 11, 18] and asm.js [4], which we discussed in Section 1.1.

    Efficient memory safety is a hard design constraint of WebAssembly. Previous systems such as CCured [34] and Cyclone [23] have imposed safety at the C language level, which generally requires program changes. Other attempts have enforced it at the C abstract machine level with combinations of static and runtime checks [10, 20, 31], sometimes assisted by hardware [16, 30]. For example, the Secure Virtual Architecture [13] defines an abstract machine based on LLVM bitcode that enforces the SAFECode [17] properties.

    Typed intermediate languages carry type information throughout the compilation process. For example, TIL [28] and FLINT [37] pioneered typed ILs for functional languages, allowing higher confidence in compiler correctness and more type-based optimizations. However, typed ILs have a different purpose than a compilation target. They are typically compiler-specific data structures that exist only as an intermediate stage of compilation, not as a storage or execution format.
Reference
  • Activex controls. https://msdn.microsoft.com/en-us/library/aa751968(v=vs.85).aspx. Accessed:2016-1114.
    Findings
  • Adobe Shockwave Player. https://get.adobe.com/shockwave/. Accessed:2016-11-14.
    Findings
  • ART and Dalvik. https://source.android.com/devices/tech/dalvik/. Accessed:2016-11-14.
    Findings
  • asm.js. http://asmjs.org. Accessed:2016-11-08.
    Findings
  • Indexed Database API. https://www.w3.org/TR/IndexedDB/. Accessed:2016-11-08.
    Findings
  • LEB128. https://en.wikipedia.org/wiki/LEB128. Accessed:2016-11-08.
    Findings
  • PolyBenchC: the polyhedral benchmark suite. http://web.cs.ucla.edu/~pouchet/software/polybench/. Accessed:2017-03-14.
    Findings
  • Scimark 2.0. http://math.nist.gov/scimark2/. Accessed:2017-03-15.
    Findings
  • Unity benchmarks. http://beta.unity3d.com/jonas/benchmark2015/. Accessed:2017-03-15.
    Findings
  • 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 ScholarLocate open access versionFindings
  • 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, 20ACM.
    Google ScholarLocate open access versionFindings
  • C. Click and M. Paleczny. A simple graph-based intermediate representation. SIGPLAN Not., 30(3):35–49, Mar. 1995.
    Google ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • D. Dhurjati, S. Kowshik, and V. Adve. SAFECode: Enforcing alias analysis for weakly typed languages. SIGPLAN Not., 41(6):144–157, June 2006.
    Google ScholarLocate open access versionFindings
  • A. Donovan, R. Muth, B. Chen, and D. Sehr. PNaCl: Portable native client executables. Technical report, 2010.
    Google ScholarFindings
  • 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 ScholarFindings
  • M. Grimmer, R. Schatz, C. Seaton, T. Wurthinger, and H. Mossenbock. 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 ScholarLocate open access versionFindings
  • 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 ScholarFindings
  • U. Holzle, C. Chambers, and D. Ungar. Debugging optimized code with dynamic deoptimization. SIGPLAN Not., 27(7):32–43, July 1992.
    Google ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • X. Leroy. Java bytecode verification: Algorithms and formalizations. J. Autom. Reason., 30(3-4):235–269, Aug. 2003.
    Google ScholarLocate open access versionFindings
  • X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Remy, and J. Vouillon. The OCaml system. INRIA, 2016.
    Google ScholarLocate open access versionFindings
  • T. Lindholm, F. Yellin, G. Bracha, and A. Buckley. The Java Virtual Machine Specification (Java SE 8 Edition). Technical report, Oracle, 2015.
    Google ScholarFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • G. C. Necula, S. McPeak, and W. Weimer. CCured: Type-safe retrofitting of legacy code. SIGPLAN Not., 37(1):128–139, Jan. 2002.
    Google ScholarLocate open access versionFindings
  • B. Pierce. Types and Programming Languages. The MIT Press, Cambridge, Massachusetts, USA, 2002.
    Google ScholarFindings
  • G. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17–139, 2004.
    Google ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • A. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115, 1994.
    Google ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
Author
Andreas Rossberg
Andreas Rossberg
Michael Holman
Michael Holman
Dan Gohman
Dan Gohman
Luke Wagner
Luke Wagner
Alon Zakai
Alon Zakai
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科