Call for Master's Students 2020/21
MSc Proposal 2020-21 / WS1
Title
Robust Symbolic Execution for WebAssembly
Advisors
José Fragoso Santos, Nuno Santos
Objectives
Symbolic execution consists of a successful program analysis technique for bug-finding and verification of multiple programming languages, ranging from statically typed languages, such as C, C++, and Java, to scripting languages, such as JavaScript, and it has been used to check different types of program properties. It has also been adopted in conjunction with static analysis to automatically generate exploits for web applications written in PHP, triggering vulnerabilities such as SQL injection and cross-site scripting. However, so far, there is no native symbolic execution engine for Wasm, making it impossible to symbolically debug Wasm code directly; one can only symbolically execute source-code programs before they get compiled to Wasm. This limitation is considerable, given that new bugs and vulnerabilities can be introduced by the compilation as well as by the interaction of the compiled Wasm program with its execution environment (i.e., browser and JavaScript engine). To fill this gap, our group has started building WASP, a WebAssembly symbolic execution engine. However, although our current prototype is able to symbolically execute Wasm programs, it has only been evaluated with simple programs, which means we do not know if the technical approach we have currently followed will perform well in real-world Wasm programs.
The goal of this thesis is to build WASP II, a robust symbolic execution engine for WebAssembly. Our approach will be to build two prototype engines (P1 and P2), exploring different approaches and then select the best performing one. For P1, we will leverage the preliminary work performed for WASP, which extended the Wasm reference interpreter with support for reasoning about symbolic values by connecting it to the Z3 SMT solver. For P2, we will use Gillian, a language-independent platform for swift development of static symbolic execution tools, and instantiate it to Wasm. We will evaluate the two prototypes on real-world Wasm applications as well as on a synthetic benchmark. Finally, guided by our applications and examples, we will extend the better-performing prototype as-needed with additional symbolic facilities. We expect this work to make original scientific contributions. The resulting system will be released as an open source project. If you like programming languages and web application programming, this is the right topic for you.
Requirements (e.g., grades, concluded courses)
Interest in programing languages and web application programming. Willingness to learn WebAssembly.
Location
IST-Alameda (INESC-ID) or IST-Tagus
Observations
For more information about this project, please visit: https://www.gsd.inesc-id.pt/~nsantos/msc-topics/msc-topics-WS.html. This work will be performed in collaboration with Pedro Adão.