Call for Master's Students 2020/21
MSc Proposal 2020-21 / WS2
Title
Exploit Generation for WebAssembly with SE-based Taint Tracking
Advisors
Pedro Adão, José Fragoso Santos
Objectives
WebAssembly is an emerging technology that promises to bring radical changes to the Web. Currently supported by all major browsers, it consists of a new web standard that defines a low-level binary instruction format and a corresponding assembly-like text format for the executable code in web pages. WebAssembly code can execute nearly as fast as running native code, enabling it to complement JavaScript to speed up performance-critical parts of web applications. However, WebAssembly may bring unexpected security risks. In particular, given that it is compiled from unsafe languages namely C/C++, vulnerabilities presumably extinct with a growing adoption of memory-safe languages like Java, will resurface on the Web under a new guise. In fact, despite WebAssembly's protection mechanisms, some C/C++ coding flaws can still transition into WebAssembly code, for instance buffer overflows, format string bugs, or use-after-free errors. If such flaws exist and can be exploitable, an attacker can leverage them in new ways for launching Web-based attacks such as cross-site scripting. To assess the security impact of existing vulnerabilities, an effective approach is to automatically generate exploits. The synthetic exploits will unambiguously demonstrate that a given vulnerability is security critical, hence its fixing must be prioritized.
The goal of this thesis is to build SWAT, a tool for automatic Synthesis of WebAssembly exploiTs. Our general approach will be to leverage symbolic execution to check Wasm program paths for exploitability properties. This work will proceed in two steps. First, we will extend the WASP symbolic execution engine with support for symbolic taint tracking in Wasm. This technique will allow us to identify security attacks that take advantage of illegal information flows. To tackle the scalability problem of path selection, we will devise path-selection heuristics to guide the program's execution to favor the selection of vulnerable paths in early exploration stages. Second, we will leverage symbolic taint tracking for constructing a sequence of crafted inputs that direct an application's execution to a vulnerable sink. This process will be steered by specific exploitability goals that depend on the type of targeted vulnerabilities. This work will begin with the generation of simple exploits for basic vulnerabilities, and then, time permitting, increase their complexity. For symbolic execution, we will use WASP, the symbolic execution engine currently under development by our team. 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, security, and web 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 Nuno Santos.