2． 符号执行的研究型工具
符号执行应用比较多的方面有：单元测试、代码漏洞静态检测等。前者是只进行过程内的分析，后者是进行程序全局的分析且更侧重于代码的安全性相关的检测。符号执行技术与约束求解器结合使用来产生测试例输入是一个比较热门且比较实用的研究点。相关的较新的研究性工具有EXE，CUTE，JPF-SE，DART，SAGE，SMART，PEX，KLEE等；这些研究针对前面所述的三个难点提出相应的改进算法，如采用动态符号执行技术，对约束求解器性能的优化，程序全局分析策略的优化，路径搜索调度策略优化，以及基于x86汇编指令的分析等。
四、 结 语
本文从符号执行的原理、关键技术及相关工具三个方面系统地介绍了符号执行技术。相对于其他的静态分析方法，符号执行方法的分析结果要更为精确，因此该技术也越来越多地被应用于实际的工具中。但是该技术目前还处于一个发展的阶段，包括符号执行的理论研究和具体应用研究。符号执行技术可以用于测试例的自动生成，也可以用于源代码安全性的检测。而这两项工作的成效都十分依赖于约束求解器的性能，同时还受硬件设备处理能力的影响。符号执行技术在实际应用中的效果还是主要取决于前面提到的关键技术，因此更多的研究团体也都主要致力于解决本文前面提到的几个问题。随着符号执行理论及约束求解理论的发展，该技术的实用价值性也会越来越高，将会在静态分析领域逐渐占据主导地位。
源代码静态分析的目标是要找出代码中潜在的漏洞，使用多种静态分析技术结合来开发静态分析工具将是一个可行且有效的方法。虽然这些静态分析工具还无法完美，甚至说效果比较一般，但随着静态分析技术的发展，或者结合其它技术（如动态分析），未来的静态分析工具一定会在软件的安全保障中起到越来越重要的地位。
参考文献
[1] McGraw, Gary. Software Security: Building Security In. Boston, MA: Addison-Wesley, 2006.
[2] W Visser, CS Pǎsǎreanu, S Khurshid, Test input generation with java PathFinder, ISSTA’04, July 11-14, 2004
[3] R Rugina, MC Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems(TOPLAS) Volume 27 ,(March 2005)
[4] Jian Zhang, Symbolic execution of program paths involving pointer structure variables, Quality Software, 2004. QSIC 2004. Proceedings. Fourth International Conference on Publication Date: 8-9 Sept. 2004,On page(s): 87- 92
[5] Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O’Hearn, Thomas Wies and Hongseok Yang, Shape Analysis for Composite Data Structures , Lecture Notes in Computer Science,2007
[6] A Ermedahl, C Sandberg, J Gustafsson, S Bygde, and Bjorn Lisper，Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation, and Invariant Analysis，Workshop on Worst-Case Execution Time Analysis,(WCET’2007)
[7] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: automatically generating inputs of death. In Proc. ACM CCS, pages 322-335, 2006.
[8] K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In Proc. ESEC/FSE, pages 263-272, 2005.
[9] S. Anand, C. S. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to Java Pathfinder. In Proc. TACAS, pages 134-138, 2007.
[10] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. PLDI, pages 75-84, 2005.
[11] GODEFROID, P., LEVIN, M. Y., AND MOLNAR, D. Automated whitebox fuzz testing. In NDSS ’08: Proceedings of Network and Distributed Systems Security (2008), pp. 151-166.
[12] P. Godefroid. Compositional dynamic test generation. In Proc. POPL, pages 47-54, 2007.
[13] Microsoft Research Foundation of Software Engineering Group, Pex: Dynamic Analysis and Test Generation for .NET, 2007. http://research.microsoft.com/Pex/.
[14] N. Tillmann and J. de Halleux. Pex-white box test generation for .NET. In Proc. TAP, pages 134-153, 2008.
[15] Cristian Cadar, Daniel Dunbar, Dawson Engler, KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.
作者简介
1.林锦滨(1985—)，男，研究生
2.张晓菲(1974—)，女，中国信息安全测评中心基础研究实验室总工程师 博士
3.刘 晖(1976—)，女，中国信息安全测评中心基础研究实验室主任 博士
(责任编辑：adminadmin2008)
