改进动态符号执行中的非线性约束求解过程

Improving the Solving of Non-linear Arithmetic Constraints in Dynamic Symbolic Execution

动态符号执行用程序变量的具体值替换动态数据结构及复杂表达式中的符号变量以便简化路径条件.这种简化路径条件的方法虽然简单,但不精确,会导致路径条件无法约束求解或者求解结果不正确.为此,提出一种改进动态符号执行中非线性算术约束求解过程的方法.该方法利用连续求解的路径条件约束具有相似性这一特征,在进行非线性算术约束求解时充分利用上次约束求解的输出信息.它用具体值依次试探替换符号变量;若所有符号变量都被试探替换而仍未求解成功,则枚举涉及非线性算术约束的变量的取值情况,将非线性算术约束转化为线性算术约束并进行求解.实验结果表明,与传统的动态符号执行工具相比,本文方法对非线性算术约束具有更快的求解速度.

Dynamic symbolic execution replaces the symbolic variables in dynamic data structures and complex expressions with con- crete values to simplify the path condition. Such simplification is simple, yet not accurate. It may lead to the failure or the wrong so- lution of solving path constraints. Therefore, the paper proposes an approach to improve the process of non-linear arithmetic con- straints in dynamic symbolic execution. By exploiting the similarity between the path constraints to solve in succession, the proposed approach makes the best of the last solution when solving the current non-linear arithmetic path constraint. It tries to replace the sym- bolic variables with concrete values successively; if all the tries fail to obtain the solution, then the values of variables in non-linear a- rithmetic constraints are enumerated to convert the non-linear arithmetic constraints to linear arithmetic constraints. Experimental re- sults show that the proposed approach solves non-linear arithmetic constraints faster, compared to the traditional dynamic symbolic ex- ecution tool.