Abstract:

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 S2E, 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.

Key words: symbol execution, constraint solving, test case generation, static analysis, vulnerability mining