Automated detection of race condition vulnerabilities in binary programs using symbolic execution
| dc.contributor.author | Makan, Keith | |
| dc.date.accessioned | 2025-10-09T08:46:52Z | |
| dc.date.available | 2025-10-09T08:46:52Z | |
| dc.date.issued | 2025 | |
| dc.description.abstract | Identifying race conditions in binary programs is challenging due to limited research on the subject and the lack of thoroughly evaluated methods, especially those applied to consumer-grade, off-the-shelf binary programs without requiring source code. Symbolic execution is a static analysis technique that significantly enhances vulnerability identi- fication, especially in fuzzing-driven security analysis. However, its scalability is often restricted by the computational demands of constraint solving, high memory consump-tion, and the state explosion problem—the rapid increase in the number of states caused by program structures. To overcome these challenges, many vulnerability analysis meth-ds incorporate techniques to manage state explosion, enabling the analysis of more complex programs. The approach presented by this thesis employs symbolic vulnerability analysis for bi-naries by introducing a novel approach called "Xegmap" which uses Directed Symbolic Execution to strategically guide the exploration of program states. Xegmap is designed to prioritise the detection of Global Memory Access Points, operating on the premise that identifying these points facilitates the detection of potentially race-prone threadinteractions. It accomplishes this through a two-phase process: a naive symbolic execu-tion phase, Negmap, followed by a directed phase, Degmap. Degmap directs symbolic execution toward global memory access points and evaluates memory interactions using a hybrid lock-set and happens-before analysis. Experimentation demonstrates Xegmap’s enhanced capacity to increase code coverage in consumer-grade, off-the-shelf binaries and to detect race conditions in binaries of varying complexity, including those with intricate input constraints and numerous threads, all without the need for source code. | |
| dc.identifier.uri | https://hdl.handle.net/10566/21042 | |
| dc.language.iso | en | |
| dc.publisher | University of the Western Cape | |
| dc.subject | Race Conditions | |
| dc.subject | Binary Programs | |
| dc.subject | Consumer-Grade | |
| dc.subject | Xegmap | |
| dc.subject | Degmap | |
| dc.title | Automated detection of race condition vulnerabilities in binary programs using symbolic execution | |
| dc.type | Thesis |