一种基于SAT的C程序缓冲区溢出漏洞检测技术
首发时间:2010-01-08
摘要:缓冲区溢出是C程序中很多安全问题的根源。本文给出一种基于SAT的C语言缓冲区溢出检测方法。该方法利用源代码变换技术,在程序源码中加入缓冲区属性刻画语句,使用断言刻画缓冲区溢出属性,然后借助SAT工具对断言进行检查。采用该方法设计实现了一个原型工具,它以程序源代码作为输入,能够自动检测程序中包含的缓冲区溢出漏洞。使用该工具对1164个公开的基准程序进行检测,实验结果表明:工具准确地定位出程序中的缓冲区溢出漏洞,误报0个,漏报率约2.08%
For information in English, please click here
A SAT-based technique to detect buffer overflows in C source code
Abstract:Buffer overflows are the source of a vast majority of security issues in C program. This paper presents a SAT-based technique to identify buffer overflows in C source code. Via a source-to-source transformation process, this method adds some statements into the source code to model the properties of buffers, and adds some asserts to describe buffer overflows. Then, those asserts are checked by SAT tools. Based on this technique, we built a prototype which takes as input source code, and can identify buffer overflows in the source code automatically. The prototype was applied to 1164 code fragments from a publicly-available benchmark. Experiments show that it accurately located buffer overflow vulnerabilities in these programs with zero false alarms and an omission rate of about 2.08%
Keywords: model checking buffer overflow Boolean Satisfiability
论文图表:
引用
No.3871350931012629****
同行评议
共计0人参与
勘误表
一种基于SAT的C程序缓冲区溢出漏洞检测技术
评论
全部评论0/1000