Document Open Access Logo

Concolic Execution for WebAssembly

Authors Filipe Marques , José Fragoso Santos , Nuno Santos , Pedro Adão

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.11.pdf
  • Filesize: 1.57 MB
  • 29 pages

Document Identifiers

Author Details

Filipe Marques
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal
José Fragoso Santos
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal
Nuno Santos
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal
Pedro Adão
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • Instituto de Telecomunicações, Aveiro, Portugal

Funding

The authors were supported by national funds through Fundação para a Ciência e a Tecnologia (UIDB/50008/2020, Instituto de Telecomunicações, and UIDB/50021/2020, INESC-ID multi-annual funding), projects INFOCOS (PTDC/CCI-COM/32378/2017) and DIVINA (CMU/TIC/0053/2021), and by the European Commission under grant agreement number 830892 (SPARTA).

Acknowledgements

We are grateful to Carolina Costa with whom we designed a preliminary version of WASP and its concolic semantics as part of her M.Sc. thesis [Costa, 2020].

Cite AsGet BibTex

Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão. Concolic Execution for WebAssembly. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 11:1-11:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.11

Abstract

WebAssembly (Wasm) is a new binary instruction format that allows targeted compiled code written in high-level languages to be executed by the browser’s JavaScript engine with near-native speed. Despite its clear performance advantages, Wasm opens up the opportunity for bugs or security vulnerabilities to be introduced into Web programs, as pre-existing issues in programs written in unsafe languages can be transferred down to cross-compiled binaries. The source code of such binaries is frequently unavailable for static analysis, creating the demand for tools that can directly tackle Wasm code. Despite this potentially security-critical situation, there is still a noticeable lack of tool support for analysing Wasm binaries. We present WASP, a symbolic execution engine for testing Wasm modules, which works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library for C and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; and was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software testing and debugging
  • Security and privacy → Formal methods and theory of security
Keywords
  • Concolic Testing
  • WebAssembly
  • Test-Generation
  • Testing C Programs

Metrics

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

Supplementary Materials

References

  1. Syrus Akbary and Ivan Enderlin. Wasmer: Run any code on any client [online]. Accessed 27th-October-2021. URL: https://wasmer.io.
  2. Kaled M. Alshmrany, Rafael S. Menezes, Mikhail R. Gadelha, and Lucas C. Cordeiro. FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution). In Fundamental Approaches to Software Engineering, 2021. Google Scholar
  3. AWS. Amazon DynamoDB Encryption Client [online]. Accessed 28th-October-2021. URL: https://docs.aws.amazon.com/crypto/latest/userguide/awscryp-service-ddb-client.html.
  4. Sacha Ayoun, Alexis Marinoiu, and Petar Maksimović. Collections-C for symbolic testing with Gillian-C [online]. Accessed 15th-December-2020. URL: https://github.com/GillianPlatform/collections-c-for-gillian [cited 15th December 2020].
  5. Roberto Baldoni, Emilio Coppa, Daniele Cono D'elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys, 2018. Google Scholar
  6. Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. Secure information flow by self-composition. Mathematical Structures in Computer Science, 2011. Google Scholar
  7. Animesh Basak Chowdhury, Raveendra Kumar Medicherla, and Venkatesh R. VeriFuzz: Program Aware Fuzzing. In Tools and Algorithms for the Construction and Analysis of Systems, 2019. Google Scholar
  8. Eli Bendersky. pycparser [online]. Accessed 1st-November-2021. URL: https://github.com/eliben/pycparser.
  9. John Bergbom. Memory safety: old vulnerabilities become new with WebAssembly. Technical report, Forcepoint, December 2018. Google Scholar
  10. Dirk Beyer. International Competition on Software Testing (Test-Comp). In Tools and Algorithms for the Construction and Analysis of Systems, 2019. Google Scholar
  11. Dirk Beyer. Status Report on Software Testing: Test-Comp 2021. In Fundamental Approaches to Software Engineering, 2021. Google Scholar
  12. Dirk Beyer and Marie-Christine Jakobs. CoVeriTest: Cooperative Verifier-Based Testing. In Fundamental Approaches to Software Engineering, 2019. Google Scholar
  13. Ruben Bridgewate. Node v12.3.0 [online]. Accessed 27th-October-2021. URL: https://nodejs.org/en/blog/release/v12.3.0.
  14. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In USENIX Conference on Operating Systems Design and Implementation, 2008. Google Scholar
  15. Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Pasareanu, Koushik Sen, Nikolai Tillmann, and Willem Visser. Symbolic execution for software testing in practice: preliminary assessment. In International Conference on Software Engineering, 2011. Google Scholar
  16. Cristian Cadar and Koushik Sen. Symbolic execution for software testing: Three decades later. Communications of the ACM, 2013. Google Scholar
  17. Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. Unleashing Mayhem on Binary Code. In IEEE Symposium on Security and Privacy, 2012. Google Scholar
  18. Marek Chalupa, Jakub Novák, and Jan Strejcek. Symbiotic 8: Parallel and targeted test generation. Fundamental Approaches to Software Engineering, 2021. Google Scholar
  19. Ting Chen, Xiao-song Zhang, Rui-dong Chen, Bo Yang, and Yang Bai. Conpy: Concolic execution engine for python applications. In Algorithms and Architectures for Parallel Processing, 2014. Google Scholar
  20. Lin Clark. Standardizing WASI: A system interface to run WebAssembly outside the web [online]. Accessed 27th-October-2021. URL: https://hacks.mozilla.org/2019/03/standardizing-wasi-a-webassembly-system-interface.
  21. Thomas H Cormen, Charles E Leiserson, Ronald L Rivest, and Clifford Stein. Introduction to algorithms. MIT press, 2022. Google Scholar
  22. C. Costa. Concolic execution for WebAssembly. Master’s thesis, Instituto Superior Técnico, Universidade de Lisboa, 2020. Master’s Thesis. Google Scholar
  23. Michael Pradel Daniel Lehmann, Johannes Kinder. Everything Old is New Again: Binary Security of WebAssembly. In USENIX Security Symposium, 2020. Google Scholar
  24. Leonardo De Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 2008. Google Scholar
  25. Jonathan Foote. Hijacking the control flow of a WebAssembly program [online]. Accessed 27th-October-2021. URL: https://www.fastly.com/blog/hijacking-control-flow-webassembly [cited 27th October 2021].
  26. José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, Part I: A Multi-Language Platform for Symbolic Execution. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020. Google Scholar
  27. William Fu, Raymond Lin, and Daniel Inge. Taintassembly: Taint-based information flow control tracking for WebAssembly. arXiv preprint, 2018. Google Scholar
  28. Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: Directed automated random testing. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005. Google Scholar
  29. GoogleSecurityResearch. Google Chrome 73.0.3683.103 - 'WasmMemoryObject::Grow' Use-After-Free [online]. Accessed 27th-October-2021. URL: https://www.exploit-db.com/exploits/46968 [cited 27th October 2021].
  30. 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 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017. Google Scholar
  31. Adam Hall and Umakishore Ramachandran. An execution model for serverless functions at the edge. In Tools and Algorithms for the Construction and Analysis of Systems, 2019. Google Scholar
  32. Paul Havlak. Nesting of reducible and irreducible loops. ACM Transactions on Programming Languages and Systems, 1997. Google Scholar
  33. Eric Hennenfent. Symbolically Executing WebAssembly in Manticore [online]. Accessed: 30th-November-2021. URL: https://blog.trailofbits.com/2020/01/31/symbolically-executing-webassembly-in-manticore.
  34. Pat Hickey. Announcing Lucet: Fastly’s native WebAssembly compiler and runtime [online]. Accessed 27th-October-2021. URL: https://www.fastly.com/blog/announcing-lucet-fastly-native-webassembly-compiler-runtime.
  35. Aaron Hilbig, Daniel Lehmann, and Michael Pradel. An Empirical Study of Real-World WebAssembly Binaries: Security, Languages, Use Cases. In Proceedings of the Web Conference, 2021. Google Scholar
  36. IEEE. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008), 2019. Google Scholar
  37. Joxan Jaffar, Rasool Maghareh, Sangharatna Godboley, and Xuan-Linh Ha. Tracerx: Dynamic symbolic execution with interpolation (competition contribution). Fundamental Approaches to Software Engineering, 2020. Google Scholar
  38. Bhaskar Kashyap. Introduction to smart contracts [online]. Accessed: 30th-November-2021. URL: https://ethereum.org/en/developers/docs/smart-contracts.
  39. Sarfraz Khurshid, Corina S. Păsăreanu, and Willem Visser. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for the Construction and Analysis of Systems, 2003. Google Scholar
  40. H. Kim. Fuzzing with stochastic optimization. Master’s thesis, LMU Munich, 2020. Bachelor’s Thesis. Google Scholar
  41. James C. King. Symbolic execution and program testing. Communications of the ACM, 1976. Google Scholar
  42. Daniel Kroening and Michael Tautschnig. CBMC - C Bounded Model Checker. In Tools and Algorithms for the Construction and Analysis of Systems, 2014. Google Scholar
  43. Daniel Larimer and Brendan Blumer. EOS.IO Technical White Paper [online]. Accessed: 30th-November-2021. URL: https://github.com/EOSIO/Documentation/blob/master/TechnicalWhitePaper.md.
  44. Hoang M. Le. LLVM-based Hybrid Fuzzing with LibKluzzer (Competition Contribution). In FASE, 2020. Google Scholar
  45. Thomas Lemberger. Plain random test generation with PRTest. International Journal on Software Tools for Technology Transfer, 2020. Google Scholar
  46. Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert Memory Model, Version 2. Research Report RR-7987, INRIA, June 2012. URL: https://hal.inria.fr/hal-00703441.
  47. Guodong Li, Esben Andreasen, and Indradeep Ghosh. SymJS: Automatic symbolic testing of JavaScript web applications. In ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2014. Google Scholar
  48. Dongge Liu, Gidon Ernst, Toby Murray, and Benjamin I. P. Rubinstein. Legion: Best-First Concolic Testing (Competition Contribution). In Fundamental Approaches to Software Engineering, 2020. Google Scholar
  49. Aishwarya Lonkar and Siddhesh Chandrayan. The dark side of WebAssembly [online]. Accessed 27th-October-2021. URL: https://www.virusbulletin.com/virusbulletin/2018/10/dark-side-webassembly [cited 27th October 2021].
  50. Brian McFadden, Tyler Lukasiewicz, Jeff Dileo, and Justin Engler. Security Chasms of WASM. Technical report, NCC Group, August 2018. Google Scholar
  51. Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts, 2019. URL: http://arxiv.org/abs/1907.03890.
  52. Srđan Panić. Collections-C [online]. Accessed 5th-July-2021. URL: https://github.com/srdja/Collections-C [cited 5th July 2021].
  53. Lawrence C Paulson. Isabelle [online]. Accessed 27th-November-2021. URL: https://isabelle.in.tum.de.
  54. Corina S. Păsăreanu and Neha Rungta. Symbolic PathFinder: Symbolic Execution of Java Bytecode. In IEEE/ACM International Conference on Automated Software Engineering, 2010. Google Scholar
  55. Ohad Rodeh, Josef Bacik, and Chris Mason. BTRFS: The Linux B-Tree Filesystem. ACM Transactions on Storage, 2013. Google Scholar
  56. Andreas Rossberg. WebAssembly Reference Interpreter [online]. Accessed 3rd-December-2020. URL: https://github.com/WebAssembly/spec/tree/master/interpreter [cited 3rd December 2020].
  57. Andreas Rossberg. WebAssembly Core Specification. Technical report, W3C, 2019. URL: https://www.w3.org/TR/wasm-core-1.
  58. Sebastian Ruland, Malte Lochau, and Marie-Christine Jakobs. HybridTiger: Hybrid Model Checking and Domination-based Partitioning for Efficient Multi-Goal Test-Suite Generation (Competition Contribution). In Fundamental Approaches to Software Engineering, 2020. Google Scholar
  59. Jan Rüth, Torsten Zimmermann, Konrad Wolsing, and Oliver Hohlfeld. Digging into browser-based crypto mining. In Internet Measurement Conference, 2018. Google Scholar
  60. José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby, and Philippa Gardner. Symbolic execution for JavaScript. In International Symposium on Principles and Practice of Declarative Programming, 2018. Google Scholar
  61. José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner. JaVerT 2.0: compositional symbolic execution for JavaScript. Proceedings of the ACM on Programming Languages, 2019. Google Scholar
  62. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. A symbolic execution framework for JavaScript. In IEEE Symposium on Security and Privacy, 2010. Google Scholar
  63. Koushik Sen and Gul Agha. CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. In CAV, 2006. Google Scholar
  64. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A Concolic Unit Testing Engine for C. ACM SIGSOFT Software Engineering Notes, 2005. Google Scholar
  65. Koushik Sen, George Necula, Liang Gong, and Wontae Choi. MultiSE: Multi-path symbolic execution using value summaries. In Joint Meeting on Foundations of Software Engineering, 2015. Google Scholar
  66. Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitry Vyukov. AddressSanitizer: A Fast Address Sanity Checker. In USENIX Conference on Annual Technical Conference, 2012. Google Scholar
  67. Amazon Web Services. AWS Encryption SDK for C. https://github.com/aws/aws-encryption-sdk-c. Accessed: 2021-09-08.
  68. Quentin Stiévenart and Coen De Roover. Compositional Information Flow Analysis for WebAssembly Programs. In IEEE International Working Conference on Source Code Analysis and Manipulation. IEEE, 2020. Google Scholar
  69. Aron Szanto, Timothy Tamm, and Artidoro Pagnoni. Taint tracking for WebAssembly. arXiv preprint, 2018. Google Scholar
  70. The Coq Development Team. The Coq Proof Assistant [online]. Accessed 27th-November-2021. URL: https://coq.inria.fr.
  71. Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014. Google Scholar
  72. W3C. W3C WebAssembly Core Specification [online]. Accessed 27th-November-2021. URL: https://www.w3.org/TR/wasm-core-1.
  73. Dong Wang, Bo Jiang, and W. K. Chan. WANA: Symbolic Execution of Wasm Bytecode for Cross-Platform Smart Contract Vulnerability Detection, 2020. URL: http://arxiv.org/abs/2007.15510.
  74. Conrad Watt. Mechanising and verifying the WebAssembly specification. In ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018. Google Scholar
  75. Conrad Watt, Petar Maksimovic, Neelakantan R. Krishnaswami, and Philippa Gardner. A program logic for first-order encapsulated WebAssembly. In Alastair F. Donaldson, editor, European Conference on Object-Oriented Programming, 2019. Google Scholar
  76. Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. Two Mechanisations of WebAssembly 1.0. In Formal Methods, 2021. Google Scholar
  77. Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan. CT-Wasm: Type-driven Secure Cryptography for the Web Ecosystem. Proceeding of the ACM on Programming Languages, 2019. Google Scholar
  78. WebAssembly. WebAssembly FAQ [online]. Accessed: 29th-October-2021. URL: https://webassembly.org/docs/faq.
  79. Shu-Hung You, Robert Bruce Findler, and Christos Dimoulas. Sound and complete concolic testing for higher-order functions. In ESOP, 2021. Google Scholar
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