SAT-based technique to detect buffer overflows in C source codes
Xing Jianying · Journal of Tsinghua University(Science and Technology) · 2009
Buffer overflows are the main source of security issues in C programs.This paper presents a SAT-based technique to identify buffer overflows in C source codes using a source-to-source transformation which adds some statements into the source code to model the buffer properties,with some asserts to describe the buffer overflows.Then,the asserts are checked by SAT tools.This technique was used to automatically identify buffer overflows in source codes in 1 164 code fragments from a publicly available benchmark.Tests show that the system accurately located buffer overflow vulnerabilities in these programs with zero false alarms and an omission rate of only 2.08%.