Call for Master's Students 2020/21
MSc Proposal 2020-21 / WS3
Title
Symbolic Runtime Modeling for Automatic Exploit Generation
Advisors
Pedro Adão, José Fragoso Santos
Objectives
Automatic exploit generation is a very effective technique for assessing the security impact of existing code vulnerabilities. In general, an exploit consists of a sequence of crafted inputs that can direct an application's execution to a vulnerable sink and deviate its normal execution flow in order to achieve some attacker-defined goal. Exploits unambiguously demonstrate that a given vulnerability is security critical, hence its fixing must be prioritized. To automatically generate exploits, symbolic execution has been proven to yield very good results. In particular, it can be used for symbolic taint tracking of programs. This technique allows us to identify attacks that take advantage of illegal information flows. Exploits can then be synthesized based on path selection heuristics which guide the program's symbolic execution according to specific exploitability goals. However, a particular challenge that occurs in this process is when a symbolic program hits a runtime API call, e.g., Libc functions in C/C++ programs, or JavaScript calls in WebAssembly code. In these cases, since we do not have access to the source code of the runtime environment (library or operating system code), it is no longer possible to carry out with the symbolic execution of the program. This limitation prevents the generation of exploits that take advantage of specific runtime API calls, e.g., format string attacks, which depend on printf.
The goal of this thesis is to develop a language-independent platform for development of runtime-dependent exploit generators. Essentially, this platform will provide symbolic models of runtime API calls named "summaries". Summaries will specify exploitability properties of all functions of the runtime API such that they can be used by symbolic execution engines for the purpose of automatic exploit generation. Using the libc as our case study, these summaries will be developed by analyzing each of the libc's functions and expressing them symbolically. They will then be tested with an existing exploit generation tool for C/C++ programs developed by our team. This work will investigate a way for specifying summaries that can be adopted for different runtime environments and programming languages (e.g., for modeling the JavaScript runtime API for WebAssembly code). This work will begin with the analysis of simpler libc functions, and progressively increase the number and complexity of analyzed functions. 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 software security, this is the right topic for you.
Requirements (e.g., grades, concluded courses)
Interest in programing languages and software security.
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.