BOFT: Exploitable Buffer Overflow Detection by Information Flow Tracking
Muhammad Monir Hossaina, Farimah Farahmandib, Mark Tehranipoorc and Fahim Rahmand
Electrical and Computer Engineering, University of Florida, Gainesville, Florida 32611, USA
ahossainm@ufl.edu@ece.ufl.edu
bfarimah@ece.ufl.edu
ctehranipoor@ece.ufl.edu
dfahimrahman@ece.ufl.edu
ABSTRACT
Buffer overflow is one of the most critical software vulnerabilities with numerous functional and security impacts on memory boundaries and program calls. An exploitable buffer overflow, which can be directly or indirectly triggered through external user domain inputs, is of a greater concern because it can be misused during run-time for adversarial intention. Although some existing tools offer buffer overflow detection to certain extents, there are major limitations, such as, poor detection coverage and ad-hoc/manual verification efforts due to inadequate predefined executions for static analysis and substantially large input subspace for dynamic verification. In this paper, to provide program verification in static time with high detection coverage, we propose an automated framework for Exploitable Buffer Overflow Detection by Information Flow Tracking (BOFT). We achieve this goal following three steps – first, BOFT analyzes the usage of arrays, pointers, and vulnerable application programming interface (APIs) in the program code and automatically inserts assertions required for buffer overflow detection. Second, BOFT instruments the program with taints for direct and indirect information flow tracking using an extensive set of formal expressions. Finally, it symbolically analyzes the instrumented code for maximum coverage and provides the list of exploitable buffer overflow vulnerabilities. BOFT is evaluated on standard benchmarks from SAMATE Juliet Test Suite (NIST) with a successful detection of ∼94.87% (minimum) of exploitable buffer overflows with zero false positives.
Keywords: Buffer Overflow, Formal Verification, Information Flow Tracking, LLVM IR, Symbolic Execution.
