摘要
精准执行可达性分析探究计算机程序状态之间的可达性关系,通过分析软件的文档、源代码或二进制程序并进行必要的测试验证,以求出在既定限制下从初始状态到特定代码位置的目标状态的准确触发输入和执行路径.精准执行可达性分析在定向测试、静态分析结果核验、错误复现和漏洞POC构造等领域均有广泛的应用.对近年来国内外学者在该研究领域取得的相关研究成果进行了系统的分析、提炼和总结.首先,指出了精准执行可达性分析对应的约束求解问题,以双向符号分析和程序归纳为主线介绍了其主要研究方法,讨论了相关技术难点;其次,对目前已经存在的精准执行可达性应用进行了分类分析;进而,指出精准执行可达性分析应用中程序分析、归纳和约束求解等方面存在的挑战;最后,对可能的解决办法以及未来发展方向进行了展望.
The research of precise execution reachability analysis focuses on figuring out the reachability between program states. It tries to find witness inputs and the execution traces that pass through the setting-up target state of certain code location by performing necessary test and verification on executable files, source code and documentation. Precise execution reachability analysis has been applied to direct testing, bug reproduction, construction of proof of concepts of vulnerabilities, verification for result of static analysis and so on. This paper provides a survey of this area. First, the corresponding constraint solving problem of precise teachability analysis is cited. Next, existing typical methods and technical difficulties about bidirectional symbolic analysis and program induction, and some technical difficulties are discussed. Then, the applications of current precise reachability analysis are classified and summarized. Furthermore, the challenges on program analysis, program induction and constraint solving are provided. Last but not least, the possible solution and future research are suggested.
出处
《软件学报》
EI
CSCD
北大核心
2018年第1期1-22,共22页
Journal of Software
基金
国家科技重大专项(2014ZX01029101-002)~~
关键词
程序分析
可达性分析
定向测试
双向符号分析
程序归纳
program analysis
reachability analysis
targeted testing
bidirectional symbolic analysis
program induction
