符号执行中的约束求解问题研究进展

Survey of Constraint Solving Techniques Research Progress in Symbolic Execution

  • 摘要: 在符号执行中,约束求解主要负责路径可达性进行判定及测试输入生成的工作,但路径爆炸问题带来的频繁调用,以及SMT求解器本身的能力和效率的不足,使得约束求解占用了符号执行中主要的性能开销,约束求解问题也成为符号执行中面临的主要瓶颈问题之一.本文介绍了符号执行和约束求解的基本概念,并分析了符号执行中约束求解问题的由来,对近年来的约束求解问题研究进展进行了归类,涉及的技术包括非相关约束分支切片、约束简化、快速不满足性检查及多求解器支持等.对这方面的研究进行了展望和总结.提出未来工作应在提高路径约束逻辑精简率、提高约束求解结果存储和重用的效率、约束求解并行化以及约束求解配置预测等方面展开.

     

    Abstract: In symbolic execution, constraint solving is mainly responsible for path reachability prediction and test input generation, but due to the path explosion problem and the limited power of the SMT solver, constraint solving occupy high overhead in symbolic execution, and this problem has become one of the bottlenecks in symbolic execution. This paper first introduces the basic concepts of symbolic execution, constraint solving, and analyzes the origin of the constraint solving problem. Second, this paper divides the optimization techniques in recent years into three stages:pre-solving, in-solving and post-solving. The related techniques include slicing, simplification, fast unsatisfiability check, multi-solver support, etc. Finally, the conclusions and prospects are made. It is proposed that the future work should focus on the improvements in respect of constraint reduction, constraint solutions reuse, parallel solving, solving configuration prediction, etc.

     

/

返回文章
返回