Creating and sharing knowledge for telecommunications

Concolic Execution for WebAssembly

Marques, F. ; Fragoso Santos, J. ; Santos, N. ; Adão, P.

Concolic Execution for WebAssembly, Proc 36th European Conference on Object-Oriented Programming - ECOOP, Berlin, Germany, Vol. 222, pp. 1 - 29, June, 2022.

Digital Object Identifier: 10.4230/LIPIcs.ECOOP.2022.11

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.