基于求解开销预测的符号执行搜索策略研究

Solving Cost Prediction Based Search in Symbolic Execution

符号执行中约束求解所占的时间比例非常高.同时,不同复杂度约束的求解时间开销差距悬殊,这一现象在对包含复杂数值计算的程序进行符号执行时尤为明显.在指定时间内求解更多约束有利于覆盖更多语句和探索更多路径.为此,提出了基于求解开销预测的符号执行搜索策略.基于实验总结出了度量约束复杂度的经验公式,并结合约束的历史求解开销来预测当前的求解开销,从而在符号执行过程中优先探索求解开销较小的路径.在KLEE中实现了上述搜索策略,并对GNU科学计算库(GSL)中的12个模块进行了实验.实验结果表明,相比现有搜索策略,提出的搜索策略在保证语句覆盖率的同时,可以探索更多的路径(平均24.34%提高);而且,在相同时间内,可以查找出更多的软件缺陷,同时查找出相同缺陷的时间开销平均降低了44.43%.

In symbolic execution ,constraint solving needs a large proportion of execution time .The solving time of a constraint differs a lot with respect to the complexity ,which happens a lot when analyzing the programs with complex numerical calculations . Solving more constraints within a specified time contributes to covering more statements and exploring more paths .Considering this feature ,we propose a solving cost prediction based search strategy for symbolic execution .Based on the experimental data of constraint solving , we conclude an empirical formula to evaluate the complexity of constraints ,and predict the solving cost of a constraint combined with historical solving cost data .The formula is used in our strategy to explore the paths with a lower solving cost with a higher priority .We have implemented our strategy in KLEE ,a state-of-art symbolic executor for C , and carried out the experiments on the randomly selected 12 modules in GNU Scientific Library （GSL ） . The experimental results indicate that ： in a same period , compared with the existing strategy ,our strategy can explore averagely 24 .34% more paths ,without sacrificing the statement coverage ;and our strategy can find more bugs .In addition ,the time of using our strategy for finding same bugs decreases 44 .43% in average .