一种基于SAT的C程序缓冲区溢出漏洞检测技术

SAT-based technique to detect buffer overflows in C source codes

缓冲区溢出是C程序中很多安全问题的根源。该文给出一种基于SAT的C语言缓冲区溢出检测方法。该方法利用源代码变换技术,在程序源码中加入缓冲区属性刻画语句,使用断言刻画缓冲区溢出属性,然后借助SAT工具对断言进行检查。采用该方法设计实现了一个原型工具,它以程序源代码作为输入,能够自动检测程序中包含的缓冲区溢出漏洞。使用该工具对1 164个公开的基准程序进行检测,结果表明:工具准确地定位出程序中的缓冲区溢出漏洞,误报0个,漏报率约2.08%。

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%.