期刊论文

Yang, Jie(yjclear@gmail.com)

中文

华中科技大学学报(自然科学版)

1671-4512

2014

42

11

86-90

10.13245/j.hust.141116

61272278:国家自然科学基金 x2jsB55101680:国家自然科学基金 61350001:国家自然科学基金 Y201224055:浙江省教育厅项目 9140A15040211CB3901:国防预研项目

本校为其他机构

以C源码为研究对象,提出了一种基于静态插装和约束求解的整数漏洞检测方法。首先在C源码中可能的整数漏洞点前面插装检测代码,同时定位可能导致整数漏洞的输入源,并将其标记为符号变量。之后将静态插装后的源码编译成可执行代码,并进行(符号和具体执行的)混合执行。在动态执行的过程中,通过对插装代码对应的符号约束进行求解,可以检测整数漏洞是否存在,以及获得当整数漏洞存在时符号变量相应的具体取值。进一步地,通过对从程序入口点到整数漏洞点所经过路径上的所有条件跳转约束进行求解,获得引导程序到达整数漏洞点时符号变量相应的具体取值。结合两者可以辅助生成触发漏洞的输入用例。基于CVE...

A static instrumentation and constraint solving based approach for integer vulnerability detection in C source code was introduced. Firstly, vulnerability detection code was statically instrumented before the possible vulnerability positions in the source code. Then, all of the integer input sources that possibly trigger the vulnerabilities were marked as symbolic variants. Next, the instrumented source code was compiled and executed in a concolic manner. During runtime, each instrumented vulnerability detection code will correspond to a symbolic constraint, and each symbolic constraint will b...