基于参数约束的分支覆盖符号执行优化算法
2020年信息技术与网络安全第1期
於家伟，李世明，毕雪洁，李秋月，高胜花
（1.哈尔滨师范大学 计算机科学与信息工程学院，黑龙江 哈尔滨 150025； 2.上海市信息安全综合管理技术研究重点实验室，上海 200240）
摘要：软件质量检测常用的方法是软件测试，符号执行作为主流的测试技术已被广泛应用于学术界与工业界中。但是随着程序规模的增大和函数调用的增加，因某些路径约束条件的特殊性，而难以生成正确的测试用例，从而导致符号执行不能对所有路径做到全覆盖。为了提高符号执行在特殊约束条件对路径的覆盖率等问题，本文提出了基于参数约束的符号执行优化算法。首先，该算法通过搜索收集程序代码中函数的特殊参数，然后利用这些特殊参数作为约束条件，最后将约束条件添加到路径的约束集中。该算法使符号执行生成的测试用例更加精确，从而实现覆盖特殊约束条件下的路径分支，以提高符号执行的精确性和路径覆盖率。在开源符号执行平台CREST中实验并验证上述优化算法，验证及测试结果表明本文提出的算法能够提高符号执行在特殊约束条件下对路径的覆盖率。
中图分类号：TP311
文献标识码：A
DOI：10.19358/j.issn.2096-5133.2020.01.003
引用格式：於家伟。基于参数约束的分支覆盖符号执行优化算法［J］。信息技术与网络安全，2020,39（1）：14-18.
文献标识码：A
DOI：10.19358/j.issn.2096-5133.2020.01.003
引用格式：於家伟。基于参数约束的分支覆盖符号执行优化算法［J］。信息技术与网络安全，2020,39（1）：14-18.
Optimization of branch covering symbol execution based on constraints
Yu Jiawei，Li Shiming，Bi Xuejie，Li Qiuyue，Gao Shenghua
（1.College of Computer Science and Information Engineering,Harbin Normal University,Harbin 150025,China;2.Shanghai Key Laboratory of Information Security Management Technology Research,Shanghai 200240,China）
Abstract：A common method for software quality inspection is software testing.Symbol execution as a mainstream testing technology has been widely used in academia and industry.However,with the increase in program size and function calls,due to the special nature of certain path constraints,it is difficult to generate correct test cases,which results in symbolic execution not being able to cover all paths.In order to improve the problem of symbol execution on the path coverage under special constraints,this paper proposes a symbolic execution optimization algorithm based on parameter constraints.Firstly,the algorithm collects special parameters of functions in the program code by searching,then uses these special parameters as constraints,and finally adds constraints to the constraint set of the path.This algorithm makes the test cases generated by symbol execution more accurate,so as to achieve path branch coverage under special constraints,to improve the accuracy of symbol execution and path coverage.Experiment is carried out to verify the above optimization algorithm in the open source symbol execution platform CREST.The results of verification and testing show that the algorithm proposed in this paper can improve the path coverage of symbol execution under special constraints.
Key words :symbolic execution;parameter constraint;test case;software test
0 引言
软件漏洞是软件中潜藏的代码缺陷，通过提高检测代码的覆盖率可以提高漏洞的发现概率，而生成高覆盖率的测试用例进行检测漏洞时，若代码执行通过率高时，可认为该程序在一定程度上是可靠的。
作为一种程序测试技术，符号执行在软件测试、程序缺陷挖掘和测试用例生成中得到广泛的研究和应用，其程序变量是以抽象符号形式来通过符号模拟程序运行并搜集路径上的约束条件。此外，根据程序的语义、遍历程序的路径空间也可用来检测程序是否满足一定的安全特性。
输入约束作为符号执行优化的方法之一，近年来业界已取得了一定成果。TRABISH D等人 结合静态分析和符号切片技术使符号执行能够搜索到更重要的路径；GODEFROID P等人提出以调用该执行函数生成的摘要作为约束条件来减少代码的重复执行；RAMOS D A等人将约束条件引入到KLEE中，通过检查被测程序的单个功能而不是整个程序，提高了效率；WONG E等人提出了基于文档辅助的建模方法，通过自然语言处理和试探法生成文档并提取约束条件；郭曦等人通过分析路径逻辑表达式和提取共享表达式来提高状态合并的效率；安靖等人通过生成外部调用函数摘要来避免因多次测试外部调用而引起的路径爆炸问题。
本文详细内容请下载:http://www.chinaaet.com/resource/share/2000003092
作者信息：
於家伟，李世明，毕雪洁，李秋月，高胜花
（1.哈尔滨师范大学 计算机科学与信息工程学院，黑龙江 哈尔滨 150025；2.上海市信息安全综合管理技术研究重点实验室，上海 200240）
此内容为AET网站原创，未经授权禁止转载。