PhD Dissertation Proposal by TU Haoxin | Boosting Symbolic Execution for Vulnerability Detection

Software systems written by humans tend to be unreliable and insecure, hence bugs (e.g., incomplete or incorrect implementation of software requirements) and vulnerabilities (e.g., memory corruptions that are more likely to be exploited by malicious attackers) in them are inevitable. Symbolic execution has shown considerable potential in detecting diverse types of software bugs and also vulnerabilities that have severe security implications. However, existing symbolic execution engines still suffer from three fundamental limitations in memory modeling, path exploration, and structured input generation, which significantly impede existing engines from efficiently and effectively detecting software bugs and vulnerabilities.

The objective of this proposal is to boost symbolic execution, by designing a new memory model, a new path exploration strategy, and a new structured input generation solution to alleviate three key limitations, to facilitate automatic bug and vulnerability detection. Specifically, in the first work, we propose SymLoc, a vulnerability detection system that designs a new symbolic memory model using concretely mapped symbolic memory operations. In the second work, we propose FastKLEE, a faster path exploration solution achieved by reducing redundant bound checking during execution. An extension of FastKLEE is planned to perform vulnerability-oriented path exploration for effective vulnerability detection. In the third work, we propose Dead, a framework that leverages targeted symbolic execution to generate structured inputs for detecting compiler bugs. An extension of Dead is planned to boost symbolic execution by adopting selective symbolizations of bug-relevant inputs and targeted loop or function summarization.

Haoxin Tu is a Dual-degree Ph.D. candidate at SMU (Singapore Management University) and DUT (Dalian University of Technology). At SMU, he is supervised by Prof. Lingxiao Jiang and Prof. Xuhua Ding. His research focuses on developing practical techniques (e.g., based on fuzzing or symbolic execution) and tools that can help improve the reliability and security of software systems (mainly system software such as compilers and Linux kernels). More information is available at https://haoxintu.github.io/.