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

摘要：

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

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

所属期刊栏目：39

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2019-10-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：957-966