2026-07-22T12:37:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16239 2024-03-12T12:00:57Z ddc:004 open_access

Concolic Execution for WebAssembly Marques, Filipe Fragoso Santos, José Santos, Nuno Adão, Pedro Concolic Testing WebAssembly Test-Generation Testing C Programs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Filipe Marques and José Fragoso Santos and Nuno Santos and Pedro Adão 2022 Is Part Of LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2022.11 urn:nbn:de:0030-drops-162394 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.11 eng https://creativecommons.org/licenses/by/4.0/legalcode