面向漏洞挖掘的基于符号分治区的测试用例生成技术

在漏洞挖掘中,符号执行技术是一种常用的测试用例生成技术。但当软件中包含加解密、校验和检验等复杂数学运算函数时,使用符号执行技术生成测试用例存在无法有效求解约束表达式的问题,导致漏洞挖掘效率低下。针对该问题,文章结合分治算法的思想提出基于符号分治区的测试用例生成技术。首先通过静态分析技术识别软件中的加解密、校验和检验等函数;然后以程序中的加解密、校验和检验函数为分界点对软件进行分区,符号执行引擎每执行到软件的一个分治区,就在本区引入一个新的符号变元进行约束构建,在约束求解时从软件最后一个分治区开始递归求解。基于该方法,文章在符号执行平台S2E上实现了漏洞挖掘原型系统Divide,并与现有的符号执行生成测试用例技术进行对比实验。实验结果表明,文章方法能够快速、有效地生成测试用例,提高漏洞挖掘的效率。

Test Case Generation Technology Based on Symbol Divide and Conquer Area for Vulnerability Mining

In vulnerability mining,symbol execution technology is a common test case generation technology.However,when the software contains complex mathematical operation functions such as encryption and decryption,checksum verification,using symbol execution technology to generate test cases cannot effectively solve constraint expressions,which results in low efficiency in vulnerability mining.In order to solve this problem,combining the idea of divide and conquer algorithm,this paper proposes a test case generation technique based on symbol divide and conquer area.Firstly,the functions of encryption and decryption,checksum verification in software are identified through static analysis technology.Then using the functions of encryption and decryption,checksum verification in the program as the partition point to partition the software.Every time the symbol execution engine executes to a divide and conquer area of software,a new symbol variable is introduced into this area for constraint construction.When solving constraints,the software will start to solve recursively from the last divide and conquer area of software.Based on this method,this paper implements a vulnerability mining prototype system Divide on the symbolic execution platform S2 E,and compares with the existing symbol execution generation test case technologies.The experimental results show that this method can generate test cases quickly and effectively,and improve the efficiency of vulnerability mining.