Active Checking Buffer Overflow Vulnerability In Binaries With Symbolic Execution

Buffer overflows in C and C++ programs are among the most common and serious classes of software vulnerabilities for two decades. To mitigate and to eradicate this security threat, many detection approaches based on static and dynamic analysis techniques have been proposed. This paper aims to provide an alternative and multipath solution to existing symbolic execution approaches by catching the red-zones in memory, rather than the strict memory object bounds, which are absolute vulnerable to buffer overflows. From the observations of buffer overflow attacks that are commonly overwrite a special position to exploit the vulnerabilities, in this paper, we propose a multipath dynamic buffer overflow detecting approach (symbolic-execution-based), relying on catching the red-zones in the stack and heap memory. We examine every memory store operation both in concrete addresses and symbolic pointers, whose writing size should never overlap or cross a red-zone position. We implement a practical dynamic checking tool called MACBin based on S2E platform. We apply it to test several real world software, the results show that MACBin is useful and effective at detecting buffer overflow vulnerabilities.