中文摘要：

溢出型漏洞是最为普遍且最具危害的漏洞类型之一,溢出漏洞检测也是目前国内外研究的热点问题.目前漏洞检测方法主要分为白盒测试和黑盒测试两类.前者主要针对程序指令进行漏洞分析,但存在效率较低、检测结果不准确等缺点;后者难以保证程序覆盖的全面性与测试数据的针对性.文中提出了一种基于有限约束满足性问题（Constraint Satisfaction Problem,CSP）的溢出漏洞动态检测方法.在程序执行过程中,结合动态污点传播和动态循环分析,选取可能产生溢出漏洞的语句并生成CSP表达式,表达式包括语句的执行条件和漏洞产生条件两部分;通过对此CSP表达式化简求解,验证漏洞的存在性与漏洞的触发条件.该方法可直接分析可执行程序,解决了间接跳转、多态代码等静态分析中难以解决的问题.为了验证该方法的有效性,作者开发了一套原型系统并进行相关实验,结果表明该方法缩小了漏洞分析范围,提高了分析效率.

英文摘要：

Overflow vulnerability is one of the most dangerous vulnerability types.Attackers can make use of this vulnerability to execute arbitrary code and control the vulnerable system.Thus,overflow vulnerability detection has become a hot topic in software analysis field.Vulnerability detection methods can usually be divided into two classes： white-box testing and black-box testing.The former one analyzes instructions of software statically,but it has the problem of inefficiency and impreciseness.The latter one cannot guarantee the coverage of programs.The generated input data is usually not effectiveness,either.This paper presents a dynamic method to detect vulnerabilities based on finite CSP（Constraint Satisfaction Problem）.By launching target programs in virtual surroundings,we choose suitable instructions to generate CSP expressions dynamically with the help of taint analysis and loop analysis.If the CSP expression is satisfiable,the vulnerability exists and the solution can trigger the vulnerability.In this way,it can analyze binary code directly without any source.Our method can solve the problems such as alias pointers and indirect jumps,which is not easy to solve in static analysis.We developed a proof-of-concept system and made several experiments on it.The results show that our method improves the efficiency to detect overflow vulnerabilities.