缓冲区溢出是C程序中很多安全问题的根源。该文给出一种基于SAT的C语言缓冲区溢出检测方法。该方法利用源代码变换技术,在程序源码中加入缓冲区属性刻画语句,使用断言刻画缓冲区溢出属性,然后借助SAT工具对断言进行检查。采用该方法设计实现了一个原型工具,它以程序源代码作为输入,能够自动检测程序中包含的缓冲区溢出漏洞。使用该工具对1 164个公开的基准程序进行检测,结果表明:工具准确地定位出程序中的缓冲区溢出漏洞,误报0个,漏报率约2.08%。 Buffer overflows are a source of many security issues in C programs. This paper presents a C language buffer overflow detection method based on SAT. This method uses the source code transform technology, adds the buffer attribute description statement in the program source code, and uses the assertion to describe the buffer overflow property, and then uses the SAT tool to check the assertion. Using this method, a prototype tool is designed and implemented, which takes program source code as input and can automatically detect the buffer overflow vulnerability contained in the program. Using this tool to test 1 164 open benchmark programs, the results show that the tool accurately locates buffer overflow vulnerabilities in the program, with 0 false positives and a false negative rate of 2.08%.