Concolic Execution for WebAssembly (Artifact)

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



PDF
Thumbnail PDF

Artifact Description

DARTS.8.2.20.pdf
  • Filesize: 0.61 MB
  • 3 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

Acknowledgements

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

Cite AsGet BibTex

Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão. Concolic Execution for WebAssembly (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/DARTS.8.2.20

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy

Abstract

This artifact contains the implementation of WASP, a symbolic execution engine for Wasm, and WASP-C, a symbolic execution framework for testing C programs built using WASP . WASP works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation [Andreas Haas et al., 2017]. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; WASP 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

References

  1. Dirk Beyer. International Competition on Software Testing (Test-Comp). In Tools and Algorithms for the Construction and Analysis of Systems, 2019. Google Scholar
  2. 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
  3. 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
  4. 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
  5. Srđan Panić. Collections-C [online]. Accessed 5th-July-2021. URL: https://github.com/srdja/Collections-C [cited 5th July 2021].
  6. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A Concolic Unit Testing Engine for C. ACM SIGSOFT Software Engineering Notes, 2005. Google Scholar
  7. Amazon Web Services. AWS Encryption SDK for C. https://github.com/aws/aws-encryption-sdk-c. Accessed: 2021-09-08.
  8. 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
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