Document Open Access Logo

A Program Logic for First-Order Encapsulated WebAssembly

Authors Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, Philippa Gardner

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.9.pdf
  • Filesize: 0.74 MB
  • 30 pages

Document Identifiers

Author Details

Conrad Watt
  • University of Cambridge, UK
Petar Maksimović
  • Imperial College London, UK
  • Mathematical Institute SASA, Serbia
Neelakantan R. Krishnaswami
  • University of Cambridge, UK
Philippa Gardner
  • Imperial College London, UK

Acknowledgements

We would like to thank the reviewers, whose comments were valuable in improving the paper. All authors were supported by the EPSRC Programme Grant "REMS: Rigorous Engineering for Mainstream Systems" (EP/K008528/1). In addition: Watt was supported by an EPSRC DTP award (EP/N509620/1); Maksimović was supported by the Serbian Ministry of Education and Science through the Mathematical Institute SASA, projects ON174026 and III44006; Krishnaswami was supported by the EPSRC Programme Grant "Semantic Foundations for Interactive Programs" (EP/N02706X/2); and Gardner was supported by the EPSRC Fellowship "VeTSpec: Verified Trustworthy Software Specification" (EP/R034567/1).

Cite AsGet BibTex

Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.9

Abstract

We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong guarantees given by WebAssembly’s type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
Keywords
  • WebAssembly
  • program logic
  • separation logic
  • soundness
  • mechanisation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Fabian Bannwart and Peter Müller. A Program Logic for Bytecode. Electron. Notes Theor. Comput. Sci., 141(1):255-273, December 2005. URL: http://dx.doi.org/10.1016/j.entcs.2005.02.026.
  2. Björn Bartels and Nils Jähnig. Mechanized, Compositional Verification of Low-Level Code. In Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods, pages 98-112, Cham, 2014. Springer International Publishing. Google Scholar
  3. Nick Benton. A Typed, Compositional Logic for a Stack-based Abstract Machine. In Proceedings of the Third Asian Conference on Programming Languages and Systems, APLAS'05, pages 364-380, Berlin, Heidelberg, 2005. Springer-Verlag. URL: http://dx.doi.org/10.1007/11575467_24.
  4. Lennart Beringer and Martin Hofmann. A Bytecode Logic for JML and Types. In Proceedings of the 4th Asian Conference on Programming Languages and Systems, APLAS'06, pages 389-405, Berlin, Heidelberg, 2006. Springer-Verlag. URL: http://dx.doi.org/10.1007/11924661_24.
  5. Lars Birkedal and Hongseok Yang. Relational Parametricity and Separation Logic. In Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS'07, pages 93-107, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1760037.1760047.
  6. Stephen Brookes and Peter W. O'Hearn. Concurrent Separation Logic. ACM SIGLOG News, 3(3):47-65, August 2016. URL: http://dx.doi.org/10.1145/2984450.2984457.
  7. M. Clint and C. A. R. Hoare. Program proving: Jumps and functions. Acta Informatica, 1(3):214-224, September 1972. URL: http://dx.doi.org/10.1007/BF00288686.
  8. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, Third Edition. The MIT Press, 3rd edition, 2009. Google Scholar
  9. Arie de Bruin. Goto statements: semantics and deduction systems. Acta Informatica, 15(4):385-424, August 1981. URL: http://dx.doi.org/10.1007/BF00264536.
  10. Y. Dong, S. Wang, L. Zhang, and P. Yang. Modular Certification of Low-Level Intermediate Representation Programs. In 2009 33rd Annual IEEE International Computer Software and Applications Conference, volume 1, pages 563-570, July 2009. URL: http://dx.doi.org/10.1109/COMPSAC.2009.81.
  11. Jonas Echterhoff. On the future of Web publishing in Unity, 2014. URL: https://blogs.unity3d.com/2014/04/29/on-the-future-of-web-publishing-in-unity/.
  12. José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner. JaVerT: JavaScript Verification Toolchain. Proc. ACM Program. Lang., 2(POPL):50:1-50:33, December 2017. URL: http://dx.doi.org/10.1145/3158138.
  13. José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner. JaVerT 2.0: Compositional Symbolic Execution for JavaScript. Proc. ACM Program. Lang., 3(POPL):66:1-66:31, January 2019. URL: http://dx.doi.org/10.1145/3290379.
  14. William Fu, Raymond Lin, and Daniel Inge. TaintAssembly: Taint-Based Information Flow Control Tracking for WebAssembly, 2018. URL: http://arxiv.org/abs/arXiv:1802.01050.
  15. Philippa Anne Gardner, Sergio Maffeis, and Gareth David Smith. Towards a Program Logic for JavaScript. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pages 31-44, New York, NY, USA, 2012. ACM. URL: http://dx.doi.org/10.1145/2103656.2103663.
  16. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. Bringing the Web Up to Speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 185-200, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3062341.3062363.
  17. David Herman, Luke Wagner, and Alon Zakai. asm.js, 2014. URL: http://asmjs.org/spec/latest.
  18. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Commun. ACM, 12(10):576-580, October 1969. URL: http://dx.doi.org/10.1145/363235.363259.
  19. Marieke Huisman and Bart Jacobs. Java Program Verification via a Hoare Logic with Abrupt Termination. In Tom Maibaum, editor, Fundamental Approaches to Software Engineering, pages 284-303, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  20. Jonas B. Jensen, Nick Benton, and Andrew Kennedy. High-level Separation Logic for Low-level Code. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 301-314, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2429069.2429105.
  21. Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The Essence of Higher-Order Concurrent Separation Logic. In Proceedings of the 26th European Symposium on Programming Languages and Systems - Volume 10201, pages 696-723, New York, NY, USA, 2017. Springer-Verlag New York, Inc. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_26.
  22. Neelakantan R. Krishnaswami. Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA., July 2011. Google Scholar
  23. Daniel Lehmann and Michael Pradel. Wasabi: A Framework for Dynamically Analyzing WebAssembly. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19, pages 1045-1058, New York, NY, USA, 2019. ACM. URL: http://dx.doi.org/10.1145/3297858.3304068.
  24. Tim Lindholm, Frank Yellin, Gilad Bracha, and Alex Buckley. The Java Virtual Machine Specification, 2013. URL: https://docs.oracle.com/javase/specs/jvms/se7/jvms7.pdf.
  25. Mozilla. Mozilla and Epic Preview Unreal Engine 4 Running in Firefox, 2014. URL: https://blog.mozilla.org/blog/2014/03/12/mozilla-and-epic-preview-unreal-engine-4-running-in-firefox/.
  26. Peter Müller and Martin Nordio. Proof-transforming Compilation of Programs with Abrupt Termination. In Proceedings of the 2007 Conference on Specification and Verification of Component-based Systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, SAVCBS '07, pages 39-46, New York, NY, USA, 2007. ACM. URL: http://dx.doi.org/10.1145/1292316.1292321.
  27. Marius Musch, Christian Wressnegger, Martin Johns, and Konrad Rieck. Web-based Cryptojacking in the Wild, 2018. URL: http://arxiv.org/abs/arXiv:1808.09474.
  28. Magnus O. Myreen, Anthony C. J. Fox, and Michael J. C. Gordon. Hoare Logic for ARM Machine Code. In Proceedings of the 2007 International Conference on Fundamentals of Software Engineering, FSEN'07, pages 272-286, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1775223.1775241.
  29. Magnus O. Myreen and Michael J. C. Gordon. Hoare Logic for Realistically Modelled Machine Code. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'07, pages 568-582, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1763507.1763565.
  30. Tobias Nipkow. Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In Julian Bradfield, editor, Computer Science Logic, pages 103-119, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  31. Martin Nordio, Peter Müller, and Bertrand Meyer. Proof-Transforming Compilation of Eiffel Programs. In Objects, Components, Models and Patterns, 46th International Conference, TOOLS EUROPE 2008, Zurich, Switzerland, June 30 - July 4, 2008. Proceedings, pages 316-335, 2008. URL: http://dx.doi.org/10.1007/978-3-540-69824-1_18.
  32. Peter W. O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and Information Hiding. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '04, pages 268-280, New York, NY, USA, 2004. ACM. URL: http://dx.doi.org/10.1145/964001.964024.
  33. David von Oheimb. Hoare Logic for Mutual Recursion and Local Variables. In Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 168-180, London, UK, UK, 1999. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=646837.708364.
  34. Mohammad Raza and Philippa Gardner. Footprints in Local Reasoning. In Roberto Amadio, editor, Foundations of Software Science and Computational Structures, pages 201-215, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  35. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS '02, pages 55-74, Washington, DC, USA, 2002. IEEE Computer Society. URL: http://dl.acm.org/citation.cfm?id=645683.664578.
  36. Andreas Rossberg, Ben L. Titzer, Andreas Haas, Derek L. Schuff, Dan Gohman, Luke Wagner, Alon Zakai, J. F. Bastien, and Michael Holman. Bringing the Web Up to Speed with WebAssembly. Commun. ACM, 61(12):107-115, November 2018. URL: http://dx.doi.org/10.1145/3282510.
  37. Ando Saabas and Tarmo Uustalu. A Compositional Natural Semantics and Hoare Logic for Low-Level Languages. Electron. Notes Theor. Comput. Sci., 156(1):151-168, May 2006. URL: http://dx.doi.org/10.1016/j.entcs.2005.09.031.
  38. Ando Saabas and Tarmo Uustalu. Compositional Type Systems for Stack-based Low-level Languages. In Proceedings of the Twelfth Computing: The Australasian Theory Symposium - Volume 51, CATS '06, pages 27-39, Darlinghurst, Australia, Australia, 2006. Australian Computer Society, Inc. URL: http://dl.acm.org/citation.cfm?id=2523791.2523798.
  39. Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. A Separation Logic for Fictional Sequential Consistency. In Programming Languages and Systems, ESOP '15, pages 736-761, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  40. Ben Smith. Threading proposal for WebAssembly, 2018. URL: https://github.com/WebAssembly/threads.
  41. Aron Szanto, Timothy Tamm, and Artidoro Pagnoni. Taint Tracking for WebAssembly, 2018. URL: http://arxiv.org/abs/arXiv:1807.08349.
  42. Gang Tan and Andrew W. Appel. A Compositional Logic for Control Flow. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI'06, pages 80-94, Berlin, Heidelberg, 2006. Springer-Verlag. URL: http://dx.doi.org/10.1007/11609773_6.
  43. Viktor Vafeiadis and Chinmay Narayan. Relaxed Separation Logic: A Program Logic for C11 Concurrency. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA '13, pages 867-884, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2509136.2509532.
  44. Carsten Varming and Lars Birkedal. Higher-Order Separation Logic in Isabelle/HOLCF. Electron. Notes Theor. Comput. Sci., 218:371-389, October 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.10.022.
  45. Wenhao Wang, Benjamin Ferrell, Xiaoyang Xu, Kevin W. Hamlen, and Shuang Hao. SEISMIC: SEcure In-lined Script Monitors for Interrupting Cryptojacks. In Javier Lopez, Jianying Zhou, and Miguel Soriano, editors, Computer Security, pages 122-142, Cham, 2018. Springer International Publishing. Google Scholar
  46. Conrad Watt. Mechanising and Verifying the WebAssembly Specification. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 53-65, New York, NY, USA, 2018. ACM. URL: http://dx.doi.org/10.1145/3167082.
  47. Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly, 2018. URL: http://arxiv.org/abs/1811.03479.
  48. Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan. CT-wasm: Type-driven Secure Cryptography for the Web Ecosystem. Proc. ACM Program. Lang., 3(POPL):77:1-77:29, January 2019. URL: http://dx.doi.org/10.1145/3290390.
  49. WebAssembly Community Group. Roadmap, 2018. URL: https://webassembly.org/roadmap/.
  50. WebAssembly Community Group. WebAssembly Specifications, 2018. URL: https://webassembly.github.io/spec/.
  51. Hongseok Yang. Semantics of Separation-Logic Typing and Higher-Order Frame Rules. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS '05, pages 260-269, Washington, DC, USA, 2005. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.2005.47.
  52. Bennet Yee, David Sehr, Gregory Dardyk, J Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. Native Client: A sandbox for portable, untrusted x86 native code. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 2009. Google Scholar
  53. Alon Zakai. Emscripten: An LLVM-to-JavaScript Compiler. In Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, OOPSLA '11, pages 301-312, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/2048147.2048224.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact