ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2016, Vol. 53 ›› Issue (5): 1086-1094.doi: 10.7544/issn1000-1239.2016.20148330

• 软件技术 • 上一篇    下一篇

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

刘经德1,3,陈振邦1,王戟1,2   

  1. 1(国防科学技术大学计算机学院 长沙 410073); 2(并行与分布处理国防科技重点实验室(国防科学技术大学计算机学院) 长沙 410073); 3(95835部队 新疆巴音郭楞 841700) (liujingde@nudt.edu.cn)
  • 出版日期: 2016-05-01
  • 基金资助: 
    国家“九七三”重点基础研究计划基金项目(2014CB340703);国家自然科学基金项目(61120106006,61472440,61272140)

Solving Cost Prediction Based Search in Symbolic Execution

Liu Jingde1,3, Chen Zhenbang1, Wang Ji1,2   

  1. 1(College of Computer, National University of Defense Technology, Changsha 410073); 2(Science and Technology on Parallel and Distributed Processing Laboratory (College of Computer, National University of Defense Technology), Changsha 410073); 3(95835 PLA Troops, Bayingolin, Xinjiang 841700)
  • Online: 2016-05-01

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

关键词: 符号执行, 约束求解, 加权随机搜索, 缺陷查找, 语句覆盖

Abstract: 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.

Key words: symbolic execution, constraint solving, weighted random search, bug finding, statement covering

中图分类号: