精准执行可达性分析:理论与应用

来源：软件学报杂志2018年第1期北京时间：

作者：杨克,贺也平,马恒太,王雪飞

单位：杨克，中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10004911,贺也平，中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 100049;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019002,马恒太，中国科学院 软件研究所 基础软件国家工程研究中心, 北京 10019003,王雪飞，中国科学院 软件研究所 基础软件国家工程研究中心, 北京 10019004

摘要：精准执行可达性分析探究计算机程序状态之间的可达性关系，通过分析软件的文档、源代码或二进制程序并进行必要的测试验证，以求出在既定限制下从初始状态到特定代码位置的目标状态的准确触发输入和执行路径.精准执行可达性分析在定向测试、静态分析结果核验、错误复现和漏洞POC构造等领域均有广泛的应用.对近年来国内外学者在该研究领域取得的相关研究成果进行了系统的分析、提炼和总结.首先，指出了精准执行可达性分析对应的约束求解问题，以双向符号分析和程序归纳为主线介绍了其主要研究方法，讨论了相关技术难点；其次，对目前已经存在的精准执行可达性应用进行了分类分析；进而，指出精准执行可达性分析应用中程序分析、归纳和约束求解等方面存在的挑战；最后，对可能的解决办法以及未来发展方向进行了展望.

关键词：程序分析;可达性分析;定向测试;双向符号分析;程序归纳

基金资助：国家科技重大专项（2014ZX01029101-002）