Classic symbolic execution of WebAssembly

João Pedro Lopes Borges

Key information

Authors:

João Pedro Lopes Borges (João Pedro Lopes Borges)

Supervisors:

José Faustino Fragoso Femenin dos Santos (José Faustino Fragoso Femenin dos Santos); Pedro Miguel dos Santos Alves Madeira Adão (Pedro Miguel dos Santos Alves Madeira Adão)

Published in

June 22, 2023

Abstract

WebAssembly (Wasm) é um formato de instruções binário portável e de baixo nível. Wasm foi desenhado para trazer o desempenho de linguagens compiladas para os browsers, que até esse ponto estavam restringidos a JavaScript, uma linguagem interpretada. Juntamente com o seu melhor desempenho, Wasm herda as vulnerabilidades escritas nas linguagens fonte inseguras. O código fonte destes módulos Wasm compilados é raramente disponibilizado, gerando assim a necessidade de ferramentas que consigam analisar código Wasm. O Web Assembly Symbolic Processor (WASP) é uma ferramenta criada para este fim, realizando Execução Concólica de módulos Wasm. Nesta tese, estendemos o WASP implementando o WASP Estático, um motor de Execução Simbólica Estática baseado numa semântica por nós definida. O design do WASP Estático foi feito com modularidade em mente, permitindo que a estratégia de procura e a estratégia de codificação sejam escolhidas em tempo de execução. A nossa implementação inclui 4 estratégias de procura diferentes e 2 estratégias de codificação. Avaliámos todas as combinações de estratégias em relação ao data-set da Test-Comp'23, e comparámos a performance do WASP Estático com a do WASP Concólico. Esta avaliação foi facilitada pelo WASP-C, um wrapper do WASP que compila programas em C para módulos WASM. WebAssembly (Wasm) is a portable low-level binary instruction format. Wasm was designed to bring the performance of compiled languages to the browser, which was up to that point restricted to JavaScript, an interpreted language. Along with its performance advantages, Wasm inherits the vulnerabilities written in the unsafe source languages. The source code of these compiled Wasm modules is rarely available, creating the need for tools that can analyse Wasm code. The Web Assembly Symbolic Processor (WASP) is one such tool, performing concolic execution of Wasm modules. In this thesis, we extend WASP by implementing Static WASP, a Static Symbolic Execution engine based on a symbolic semantics defined by us. The design of Static WASP had modularity in mind, allowing the search strategy and encoding strategy of the symbolic executor to be chosen at runtime. Our implementation includes 4 different search strategies and 2 encoding strategies. We evaluated all strategy combinations against the Test-Comp'23 data-set, and compared the performance of Static WASP with that of Concolic WASP. This evaluation was enabled by WASP-C, a wrapper of WASP that compiles C programs to Wasm modules.