DARTS.8.2.20.pdf
- Filesize: 0.61 MB
- 3 pages
Document
Concolic Execution for WebAssembly (Artifact)
Authors
Filipe Marques 
,
José Fragoso Santos ,
Nuno Santos ,
Pedro Adão
-
Part of:
Issue:
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Volume: DARTS, Volume 8 (ECOOP 2022)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-23
Artifact Description
Document Identifiers
Author Details
- Instituto Superior Técnico, University of Lisbon, Portugal
- INESC-ID Lisbon, 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 As Get 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
DARTS-8-2-20-artifact-18c15a089a044dcc0b55742c364d6f5a.gz.tar
(Filesize: 0.89 GB)
MD5 Sum:
18c15a089a044dcc0b55742c364d6f5a
(Get MD5 Sum)
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)
0PDF Downloads
References
-
Dirk Beyer. International Competition on Software Testing (Test-Comp). In Tools and Algorithms for the Construction and Analysis of Systems, 2019.
-
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.
-
Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: Directed automated random testing. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005.
-
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.
- Srđan Panić. Collections-C [online]. Accessed 5th-July-2021. URL: https://github.com/srdja/Collections-C [cited 5th July 2021].
-
Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A Concolic Unit Testing Engine for C. ACM SIGSOFT Software Engineering Notes, 2005.
- Amazon Web Services. AWS Encryption SDK for C. https://github.com/aws/aws-encryption-sdk-c. Accessed: 2021-09-08.
-
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.