Optimizing Symbolic Execution Through Taint Analysis and Path Prioritization (Bachelor Thesis, Ongoing)
Author
Description
Symbolic execution is a powerful technique for analyzing software, but suffers from scalability problems. The efficiency of this technique strongly depends on which program paths are prioritized. A targeted selection of relevant nodes can make exploration more efficient.
This project aims to optimize symbolic execution through the targeted use of taint analysis. Instead of performing an even exploration of all program paths, memory allocations and user input in particular are to be prioritized as safety-critical points.
Relevant nodes are identified using the control flow graph (CFG) or, for example, by scanning for system calls that process external input. These serve as starting points for the symbolic execution. They are then integrated with a symbolic execution engine (e.g. angr) in order to direct the exploration specifically to security-relevant paths and avoid redundant or less meaningful paths. Program paths that have no dependency on input data are ignored (e.g. through taint analysis).
The effectiveness of the optimization is evaluated by a comparative analysis of the symbolic execution with and without prioritization. Criteria such as runtime, detected program paths and potential vulnerabilities are examined.
Start / End Dates
2025/03/03 - 2025/07/02