Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Two Mechanisations of WebAssembly 1.0

  • Conference paper
  • First Online:
Formal Methods (FM 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13047))

Included in the following conference series:

Abstract

WebAssembly (Wasm) is a new bytecode language supported by all major Web browsers, designed primarily to be an efficient compilation target for low-level languages such as C/C++ and Rust. It is unusual in that it is officially specified through a formal semantics. An initial draft specification was published in 2017 [14], with an associated mechanised specification in Isabelle/HOL published by Watt that found bugs in the original specification, fixed before its publication [37].

The first official W3C standard, WebAssembly 1.0, was published in 2019 [45]. Building on Watt’s original mechanisation, we introduce two mechanised specifications of the WebAssembly 1.0 semantics, written in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. Wasm’s compact design and official formal semantics enable our mechanisations to be particularly complete and close to the published language standard. We present a high-level description of the language’s updated type soundness result, referencing both mechanisations. We also describe the current state of the mechanisation of language features not previously supported: WasmCert-Isabelle includes a verified executable definition of the instantiation phase as part of an executable verified interpreter; WasmCert-Coq includes executable parsing and numeric definitions as on-going work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Our mechanisations are distributed under open source licences on GitHub [36].

References

  1. Allais, G.: Parseque (2017). https://github.com/gallais/parseque

  2. Allais, G.: Agdarsec - total parser combinators. In: JFLA 2018 (2018)

    Google Scholar 

  3. Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283–307. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_12

    Chapter  Google Scholar 

  4. Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263–288 (2009). https://doi.org/10.1007/s10817-009-9148-3. https://hal.inria.fr/inria-00352524

  5. Bodin, M., et al.: A trusted mechanised JavaScript specification. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 87–100. Association for Computing Machinery, New York (2014). https://doi.org/10.1145/2535838.2535876

  6. Bogdanas, D., Roşu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 445–456. Association for Computing Machinery, New York (2015). https://doi.org/10.1145/2676726.2676982

  7. Boldo, S., Jourdan, J.H., Leroy, X., Melquiond, G.: Verified compilation of floating-point computations. J. Autom. Reason. 54(2), 135–163 (2015). http://xavierleroy.org/publi/floating-point-compcert.pdf

  8. Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243–252 (2011). https://doi.org/10.1109/ARITH.2011.40

  9. Bynens, M.: Loading webassembly modules efficiently (2018). https://developers.google.com/web/updates/2018/04/loading-wasm

  10. Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 533–544. Association for Computing Machinery, New York (2012). https://doi.org/10.1145/2103656.2103719

  11. Filaretti, D., Maffeis, S.: An executable formal semantics of PHP. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 567–592. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44202-9_23

    Chapter  Google Scholar 

  12. Fragoso Santos, J., Maksimović, P., Sampaio, G., Gardner, P.: Javert 2.0: compositional symbolic execution for javascript. Proc. ACM Program. Lang. 3(POPL) (2019). https://doi.org/10.1145/3290379

  13. Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of JavaScript. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126–150. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14107-2_7

    Chapter  Google Scholar 

  14. Haas, A., et al.: Bringing the web up to speed with WebAssembly. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM (2017)

    Google Scholar 

  15. Huang, X.: A mechanized formalization of the webassembly specification in coq. In: RIT Computer Science (2019)

    Google Scholar 

  16. Hupel, L., Zhang, Y.: Cakeml. Archive of Formal Proofs, March 2018. https://isa-afp.org/entries/CakeML.html. Formal proof development

  17. Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)

    Google Scholar 

  18. Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006). https://doi.org/10.1145/1146809.1146811

  19. Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 179–191. Association for Computing Machinery, New York (2014). https://doi.org/10.1145/2535838.2535841

  20. Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Principles of Programming Languages (POPL), pp. 179–191. ACM Press (2014). https://doi.org/10.1145/2535838.2535841. https://cakeml.org/popl14.pdf

  21. Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of standard ML. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 173–184. Association for Computing Machinery, New York (2007). https://doi.org/10.1145/1190216.1190245

  22. Leroy, X.: Java bytecode verification: an overview. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 265–285. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_26

    Chapter  MATH  Google Scholar 

  23. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814

  24. Memarian, K., et al.: Into the depths of C: elaborating the de facto standards. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 1–15. Association for Computing Machinery, New York (2016). https://doi.org/10.1145/2908080.2908081

  25. Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 175–188. ACM, New York (2014). https://doi.org/10.1145/2628136.2628143

  26. Norrish, M.: C formalised in HOL. Technical report (1998)

    Google Scholar 

  27. Owens, S.: A sound semantics for OCamllight. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 1–15. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78739-6_1

    Chapter  Google Scholar 

  28. Park, D., Stefănescu, A., Roşu, G.: KJS: A complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 346–356. Association for Computing Machinery, New York (2015). https://doi.org/10.1145/2737924.2737991

  29. Pfenning, F., Schürmann, C.: System description: twelf — a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_14

    Chapter  Google Scholar 

  30. Pierce, B.C.: Types and Programming Languages, 1st edn. The MIT Press, Cambridge (2002)

    Google Scholar 

  31. Ringer, T., Palmskog, K., Sergey, I., Gligoric, M., Tatlock, Z.: QED at large: a survey of engineering of formally verified software. Found. Trends Program. Lang. 5(2-3), 102–281 (2019). https://doi.org/10.1561/2500000045

  32. Rou, G., erbănută, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010). https://doi.org/10.1016/j.jlap.2010.03.012. http://www.sciencedirect.com/science/article/pii/S1567832610000160. Membrane computing and programming

  33. Santos, J.F., Maksimović, P., Grohens, T., Dolby, J., Gardner, P.: Symbolic execution for JavaScript. In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018. Association for Computing Machinery, New York (2018). https://doi.org/10.1145/3236950.3236956

  34. Syme, D.: Proving Java type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 83–118. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48737-9_3

    Chapter  Google Scholar 

  35. Tan, Y.K., Owens, S., Kumar, R.: A verified type system for CakeML. In: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages. IFL 2015. Association for Computing Machinery, New York (2015). https://doi.org/10.1145/2897336.2897344

  36. WasmCert: WasmCert (2021). https://github.com/WasmCert

  37. Watt, C.: Mechanising and verifying the WebAssembly specification. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 53–65. Association for Computing Machinery, New York (2018). https://doi.org/10.1145/3167082

  38. Watt, C.: Mechanising and evolving the formal semantics of WebAssembly: The Web’s new low-level language (2021, not yet published)

    Google Scholar 

  39. WebAssembly Community Group: tests (2020). https://github.com/WebAssembly/spec/tree/704d9d9e9c861fdb957c3d5e928f1d046a31497e/test

  40. WebAssembly Community Group: Webassembly (2020). https://github.com/WebAssembly/spec/tree/704d9d9e9c861fdb957c3d5e928f1d046a31497e/

  41. WebAssembly Community Group: bulk-memory-operations (2021). https://github.com/WebAssembly/bulk-memory-operations

  42. WebAssembly Community Group: GC (2021). https://github.com/WebAssembly/gc

  43. WebAssembly Working Group: Binary format (2019). https://www.w3.org/TR/2019/REC-wasm-core-1-20191205/#binary-format%E2%91%A0

  44. WebAssembly Working Group: Instantiation (2019). https://www.w3.org/TR/2019/REC-wasm-core-1-20191205/#instantiation%E2%91%A1

  45. WebAssembly Working Group: Webassembly core specification (2019). https://www.w3.org/TR/2019/REC-wasm-core-1-20191205/

  46. Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994). https://doi.org/10.1006/inco.1994.1093

Download references

Acknowledgement

Watt, Pichon-Pharabod, Bodin, and Gardner were supported by the EPSRC grant REMS: Rigorous Engineering for Mainstream Systems (EP/K008528/1). Watt and Pichon-Pharabod were supported by the VeTSS/NCSC grant Mechanising Concurrent WebAssembly (G105616 RI2).

Watt was supported by a Peterhouse Research Fellowship and a Google PhD Fellowship in Programming Technology and Software Engineering. Rao was supported by an Imperial College London, Department of Computing, Doctoral Scholarship Award. Pichon-Pharabod was supported by the ERC grant Engineering with Logic and Verification: Mathematically Rigorous Engineering for Safe and Secure Computer Systems (789108). Bodin and Gardner were supported by the EPSRC fellowship VeTSpec: Verified Trustworthy Software Specification (EP/R034567/1).

Author information

Authors and Affiliations

  1. University of Cambridge, Cambridge, UK

    Conrad Watt & Jean Pichon-Pharabod

  2. Imperial College London, London, UK

    Xiaojia Rao, Martin Bodin & Philippa Gardner

  3. Inria, Rocquencourt, France

    Martin Bodin

Authors
  1. Conrad Watt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xiaojia Rao
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean Pichon-Pharabod
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Bodin
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Philippa Gardner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Conrad Watt .

Editor information

Editors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Marieke Huisman

  2. NASA Ames Research Center, Moffett Field, CA, USA

    Corina Păsăreanu

  3. Institute of Software, Chinese Academy of Sciences, Beijing, China

    Naijun Zhan

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Watt, C., Rao, X., Pichon-Pharabod, J., Bodin, M., Gardner, P. (2021). Two Mechanisations of WebAssembly 1.0. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-90870-6_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-90869-0

  • Online ISBN: 978-3-030-90870-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation