Precisely detecting buffer overflow vulnerabilities

Buffer overflow (BO) vulnerability is one of the most crucial threats to the security of software system, and a method using model checking was proposed to precisely detect potential BO vulnerabilities in source code. This method converts detecting BO vulnerabilities to verifying the reachability of certain position in programs by static analysis. Then model checking was used to do the verification job. Based on GCC and Blast, a prototype system to precisely detect BO vulnerabilities was developed for this method. At last, wu-ftpd, minicom and CoreHTTP was checked by the prototype system, which not only detected those known BO vulnerabilities but also some unknown BO vulnerabilities.