基于静态插装和约束求解的整数漏洞检测  

Approach for integer vulnerability detection based on static instrumentation and constraint solving

作　　者：张帆[1] 张聪[2] 徐明迪[3] 杨捷[4] 

机构地区：[1]杭州电子科技大学通信工程学院,浙江杭州310018 [2]武汉轻工大学数学与计算机学院,湖北武汉430023 [3]武汉数字工程研究所系统软件部,湖北武汉430072 [4]华南理工大学软件学院,广东广州510006

出　　处：《华中科技大学学报（自然科学版）》2014年第11期86-90,共5页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金资助项目(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 be sent to simple theorem prover(STP)(a constraint solver)to solve.Once a symbolic constraint can be satisfied,an integer vulnerability is detected.Furthermore,all of the conditional jump symbolic constraints in the path that leads the program trigger the vulnerability were also applied to STP.By solving both of the symbolic constraints,the input case that can trigger the vulnerability can be generated.Experimental results show that our approach can successfully detect vulnerabilities announced by CVE(common vulnerabilities and exposures).

关 键 词：整数漏洞 符号执行 约束求解 程序插装 漏洞检测 

分 类 号：TP312.1[自动化与计算机技术—计算机软件与理论] TP309[自动化与计算机技术—计算机科学与技术]