WebAssembly (Wasm) is a low-level intermediate representation (IR) that has been widely used as a compilation target for high-level programming languages, and can be executed in various environments, such as browsers and clouds. Concolic execution is a program analysis for bug detection and program testing. By executing the program concretely and symbolically at the same time, it can generate inputs by solving path constraints obtained from the corresponding execution.

In this presentation, we present a design for efficient concolic execution of WebAssembly. Building on top of a WebAssembly’s CPS semantics, we are building a concolic execution compiler for WebAssembly, which generates performant code by eliminating the overhead that commonly exists in other interpretation-based concolic execution tools. By manipulating continuations in the generated code, our design makes it possible to reuse the snapshots, avoiding the overhead of re-execution that typically exists in instrumentation-based concolic execution tools. The talk will demonstrate the generation of high-performance C++ concolic execution code from WebAssembly source file, and the generation of test cases that trigger errors in the source WebAssembly program.