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.