DROPS

Document

Artifact

Concolic Execution for WebAssembly (Artifact)

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

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

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.

Cite as

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)

Copy BibTex To Clipboard

@Article{marques_et_al:DARTS.8.2.20,
  author =	{Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro},
  title =	{{Concolic Execution for WebAssembly (Artifact)}},
  pages =	{20:1--20:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.20},
  URN =		{urn:nbn:de:0030-drops-162181},
  doi =		{10.4230/DARTS.8.2.20},
  annote =	{Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C Programs}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2022.11

Concolic Execution for WebAssembly

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

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{marques_et_al:LIPIcs.ECOOP.2022.11,
  author =	{Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro},
  title =	{{Concolic Execution for WebAssembly}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{11:1--11:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.11},
  URN =		{urn:nbn:de:0030-drops-162394},
  doi =		{10.4230/LIPIcs.ECOOP.2022.11},
  annote =	{Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C Programs}
}

Search Results

Documents authored by Marques, Filipe

Concolic Execution for WebAssembly (Artifact)

Abstract

Cite as

Concolic Execution for WebAssembly

Abstract

Cite as

Thanks for your feedback!

Could not send message