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

Survey of Constraint Solving Techniques Research Progress in Symbolic Execution

作　　者：邹权臣 吴润浦[1] 马金鑫[1] 王欣[1] 辛伟[1] 侯长玉 李美聪 ZOU Quan-chen;WU Run-pu;MA Jin-xin;WANG Xin;XIN Wei;HOU Chang-yu;LI Mei-cong(China Information Technology Security Evaluation Center,Beijing 100085,China;360 Security Research Labs,Beijing 100016,China;Beijing Central Security Evaluation Technology Co.Ltd.,Beijing 100085,China)

机构地区：[1]中国信息安全测评中心,北京100085 [2]360安全研究院,北京100016 [3]北京中测安华科技有限公司,北京100085

出　　处：《北京理工大学学报》2019年第9期957-966,共10页Transactions of Beijing Institute of Technology

基　　金：国家自然科学基金资助项目(U1636115,61502536,61872386);国家重点研发计划项目(2016QY071401,2016YFB0800902)

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

关 键 词：符号执行 约束求解 性能优化 漏洞挖掘 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]