符号执行研究综述

Survey of Symbolic Execution

符号执行作为一种重要的程序分析方法,可以为程序测试提供高覆盖率的测试用例,以触发深层的程序错误。首先,介绍了经典符号执行方法的原理;然后,阐述了基于符号执行发展形成的混合测试、执行生成测试和选择性符号执行方法,同时,对制约符号执行方法在程序分析中的主要因素进行了分析,并讨论了缓解这些问题和提高符号执行可行性的主要方法;随后,介绍了当前主流的符号执行分析工具,并比较分析了其优缺点;最后,总结并讨论了符号执行的未来发展方向。

As an important program analysis method,symbolic execution can generate high coverage tests to trigger deeper vulnerabilities.This paper firstly introduced the principle of classical symbolic execution,and elaborated three dynamic symbolic execution methods which are known as concolic testing,execution generated test and selective symbolic execution.Meanwhile,the essence of main challenges of symbolic execution and the current major solutions were discussed.Symbolic execution has been incubated in dozens of tools which were described and compared in this paper.Finally,the develop directions of symbolic execution were forecasted.