基于符号执行的软件脆弱性分析技术研究
|
摘要
网络安全问题归根结底是由软件脆弱性造成的,一直以来对软件产业构成着严重威胁。过去那种依靠专业安全研究人员手动发现软件脆弱性的方法,已经不能满足人们对安全的迫切需求,而传统的脆弱性自动发掘技术如Fuzzing由于自身固有的缺陷,只能随机的生成测试用例,而不能全面的分析、理解目标软件。近年来,针对Fuzzing测试技术存在的不足,符号执行在软件测试和脆弱性发现中得到了广泛的应用。随着约束求解器的进步、计算机性能的提高和新算法的出现,符号执行已成为国内外研究的热点。
脆弱性分析的关键是如何触发软件中潜在的各种异常或漏洞,然而目前针对软件脆弱性问题的分析方法普遍存在着分析精度差、效率低、漏报率高的问题,制约了其在软件脆弱性分析中的进一步应用。本课题针对符号执行自身的优缺点,对其在自动生成测试用例方面进行了深入的研究,致力于以符号执行为主、辅以污点分析技术,研究并改进了相关核心算法,即在符号执行算法中采用启发式搜索、学习和函数摘要技术有效遏制路径爆炸,并在污点分析算法中通过汇编指令语义分析,引入控制流并与数据流有效结合,优化了对符号变量传播关系的跟踪,从而建立起一种高效、自动化软件脆弱性分析模型,从而能够触发传统方式无法发现的软件异常或漏洞,提高了软件脆弱性发现的效率、精度和准确性。本课题同时给出了原型系统的设计方案。
Essentially, the network security problems are caused by software vulnerabilities , which have posed a serious threat to software industry. Nowadays, the method that relies on the professional security researchers to discover software vulnerabilities manually can not meet users' urgent needs for security, and the old-fashioned vulnerability auto-discovery technologies such as Fuzzing have their inherent defects, such as than they can only generate test cases with random inputs, which is not comprehensive enough to understand the target software. In recent years, aiming at the shortcomings of Fuzzing test technology, symbolic execution has been widely used in software testing and vulnerability discovery. Since the development of the constraint solver, the improvement of computing capability and the emergence of new algorithms, symbolic execution has become a hot topic in vulnerability research at home and abroad.
The key to vulnerability analysis is how to trigger all kinds of abnormalities or potential vulnerabilities of software, but the prevalence of poor accuracy, low efficiency and high rate of false negative of the current analysis techniques, restrict its further application in software vulnerability analysis. Therefore, based on the understanding and deep research of test-case generation of symbolic execution, this project is committed to symbolic execution, supplemented by taint analysis, to study and improve the relevant core algorithm.That is, in symbolic execution algorithm, we introduced heuristic search, learning and functions abstraction techniques to effectively address the path explosion problem; and in taint analysis algorithm, after the semantic analysis of assembly instructions, the control flow analysis are introduced and effectively combined with the data flow analysis to optimize the propagation relationship of the symbolic variables. In this way, we established an efficient, automated software vulnerability analysis model, which can discover the hidden defects or software vulnerabilities that the traditional way cannot trigger, and increased the efficiency, precision and accuracy of software vulnerabilitie analysis. The subject also gives a prototype system design solution.
脆弱性分析的关键是如何触发软件中潜在的各种异常或漏洞,然而目前针对软件脆弱性问题的分析方法普遍存在着分析精度差、效率低、漏报率高的问题,制约了其在软件脆弱性分析中的进一步应用。本课题针对符号执行自身的优缺点,对其在自动生成测试用例方面进行了深入的研究,致力于以符号执行为主、辅以污点分析技术,研究并改进了相关核心算法,即在符号执行算法中采用启发式搜索、学习和函数摘要技术有效遏制路径爆炸,并在污点分析算法中通过汇编指令语义分析,引入控制流并与数据流有效结合,优化了对符号变量传播关系的跟踪,从而建立起一种高效、自动化软件脆弱性分析模型,从而能够触发传统方式无法发现的软件异常或漏洞,提高了软件脆弱性发现的效率、精度和准确性。本课题同时给出了原型系统的设计方案。
Essentially, the network security problems are caused by software vulnerabilities , which have posed a serious threat to software industry. Nowadays, the method that relies on the professional security researchers to discover software vulnerabilities manually can not meet users' urgent needs for security, and the old-fashioned vulnerability auto-discovery technologies such as Fuzzing have their inherent defects, such as than they can only generate test cases with random inputs, which is not comprehensive enough to understand the target software. In recent years, aiming at the shortcomings of Fuzzing test technology, symbolic execution has been widely used in software testing and vulnerability discovery. Since the development of the constraint solver, the improvement of computing capability and the emergence of new algorithms, symbolic execution has become a hot topic in vulnerability research at home and abroad.
The key to vulnerability analysis is how to trigger all kinds of abnormalities or potential vulnerabilities of software, but the prevalence of poor accuracy, low efficiency and high rate of false negative of the current analysis techniques, restrict its further application in software vulnerability analysis. Therefore, based on the understanding and deep research of test-case generation of symbolic execution, this project is committed to symbolic execution, supplemented by taint analysis, to study and improve the relevant core algorithm.That is, in symbolic execution algorithm, we introduced heuristic search, learning and functions abstraction techniques to effectively address the path explosion problem; and in taint analysis algorithm, after the semantic analysis of assembly instructions, the control flow analysis are introduced and effectively combined with the data flow analysis to optimize the propagation relationship of the symbolic variables. In this way, we established an efficient, automated software vulnerability analysis model, which can discover the hidden defects or software vulnerabilities that the traditional way cannot trigger, and increased the efficiency, precision and accuracy of software vulnerabilitie analysis. The subject also gives a prototype system design solution.
引文
[1] J. Kong, C. C. Zou, and H. Zhou: Improving Software Security via runtime Instruction-level Taint Checking. In ASID’06: Proceedings f the 1st Workshop on Architectural and System Support for mproving Software Dependability, pages 18–24.
[2] J. Newsome and D. Song: Dynamic Taint Analysis for Automatic Detection, Analysis, and Signature Generation of Exploits on Commodity Software. In Proceedings of the Network and Distributed System Security Symposium (NDSS 2005)
[3] W. Halfond, A. Orso, and P. Manolios: Using Positive Tainting and Syntax-aware Evaluation to Counter SQL Injection Attacks. InSIGSOFT’06/FSE-14: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, pages 175–185, New York, NY, USA, 2006.
[4] A. Nguyen-Tuong, S. Guarnieri, D. Greene, J. Shirley, and D. Evans: Automatically Hardening Web Applications Using Precise Tainting. In 20th IFIP International Information Security Conference, 2005.
[5] Shao Lin, Zhang Xiaosong, and Su Enbiao: New Method of software vulnerability detection based on fuzzing. Computer Application Research, 2009, 26(3): 1086-1088.
[6] Feng Qin, Cheng Wang, Zhenmin Li, Ho-seop Kim, Yuanyuan Zhou, and Youfeng Wu: LIFT: A Low-Overhead Practical Information Flow Tracking System for Detecting Security Attacks.Microarchitecture, 2006. MICRO-39. 39th Annual IEEE/ACM International Symposium on Digital Object Identifier: 10.1109/MICRO.2006.29 Publication Year: 2006 , Page(s): 135– 148.
[7] J.C. King: Symbolic execution and program testing. Commun. ACM 19(7), 385–394(1976).
[8] YoungHan Choi, HyoungChun Kim, and DoHoon Lee: Tag-Aware Text File Fuzz Testing for Security of a Software System. Convergence Information Technology, 2007. International Conference onVolume , Issue , 21-23 Nov. 2007 Page(s):2254–2259.
[9] Liu Guang-Hong, Wu Gang, Tao Zheng, Shuai Jian-Mei, and Tang Zhuo-Chun: Vulnerability Analysis for X86 Executables Using Genetic Algorithm and Fuzzing. Convergence and Hybrid Information Technology, 2008. ICCIT apos; 08. Third International Conference on Volume 2, Issue, 11-13 Nov. 2008 Page(s): 491– 497.
[10] James Clause, Wanchun Li, and Alessandro Orso: Dytan: A Generic Dynamic Taint Analysis Framework.International symposium on Software testing and analysis(2007). Pages: 196-206.
[11]李佳静,王铁磊,韦韬,凤旺森,邹维:一种多项式时间的路径敏感的污点分析方法.计算机学报.2009.V09.
[12]周孔伟,蔡经球:符号执行—介于程序验证和程序调试之间的方法.小型微型计算机系统.1982.V04.
[13]林锦滨,张晓菲,刘晖:符号执行技术研究.全国计算机安全学术交流会论文集(第二十四卷)2008.V03.
[14] Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215–222 (1976).
[15] Ball, T.,Majumdar,R.,Millstein, T.,Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of PLDI (2001).
[16] Khurshid, S., Pǎsǎreanu, C.S., and Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS (2003).
[17] C. S. Pǎsǎreanu and W. Visser: A survey of new trends in symbolic execution for software testing and analysis.
[18] Anand, S., Pǎsǎreanu, C.S., and Visser, W.: JPF-SE: A symbolic execution extension to Java PathFinder. In: Proceedings of TACAS (2007).
[19] Pǎsǎreanu, C.S., Mehlitz, P., Bushnell, D., Gundy-Burlet, K., Lowry, M., Person, S., and Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In: Proceedings of ISSTA (2008).
[20] D. Brumley, C. Hartwig, M. G. Kang, Z. Liang, J. Newsome, D. Song, and H. Yin: BitScope: Automatically dissecting malicious binaries. Technical Report CMU-CS-07-133, School of Computer Science, Carnegie Mellon University, March 2007.
[21] Godefroid, P., Klarlund, N., and Sen, K.: DART: directed automated random testing.In: Proceedings of PLDI (2005).
[22] Sen, K., Marinov, D., and Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC/FSE (2005).
[23] Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., and Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of ACM Conference on Computer and Communications Security 2006).
[24] PEX: Automated Exploratory Testing for .NET: http://research.microsoft.com/Pex
[25] N. Nethercote and J. Seward: Valgrind: A frameworkfor heavyweight dynamic binary instrumentation. In PLDI, 2007.
[26] V. Ganesh, T. Leek, and M. Rinard: Taint-based Directed Whitebox Fuzzing Software Engineering, 2009. ICSE 2009. IEEE 31st International Conference on 16-24 May 2009 Page(s):474 - 484.
[27] P. Godefroid, M. Y. Levin, and D. Molnar: Automated Whitebox Fuzz Testing. Technical Report MS-TR-2007-58, Microsoft, May 2007. See http://research.microsoft.com/users/pg/.
[28] The Choco Constraint Solver: http://choco.sourceforge.net/
[29] IASolver (The Brandeis Interval Arithmetic Constraint Solver): http://www.cs.brandeis.edu/~tim/Applets/IAsolver.html/
[30] Yices: An SMT Solver. http://yices.csl.sri.com/
[31] Luk, C., Cohn, R., Muth, R., Patil, H., Klauser, A., Lowney, G., Wallace, S., Vijay Janapa Reddi, and Hazelwood, K: Pin: building customized program analysis tools with dynamic instrumentation. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL, USA, June 12 - 15, 2005). 190-200.
[32] De Moura, L., Bj(?)rner, N., et al.: Z3: an efficient SMT solver. Software and documentation available at http://research.microsoft.com/projects/z3 (2006–2008).
[33] Probst, M., Krall, A., and Scholz, B: Register liveness analysis for optimizing dynamic binary translation.Reverse Engineering, 2002. Proceedings. Ninth Working Conference on Digital Object Identifier: 10.1109/WCRE.2002.1173062.Publication Year: 2002 , Page(s): 35– 44.
[34] Hui Shu, and Yongjun He: Research on protocol reverse extraction based on DynamoRIO. Communication Systems, Networks and Applications (ICCSNA),2010 Second International Conference on Volume:1. Digital Object Identifier: 10.1109/ICCSNA.2010.5588804. Publication Year: 2010 , Page(s): 5– 9.
[35] Yongjun He, Hui Shu, and Xiaobing Xiong: Protocol Reverse Engineering Based on DynamoRIO. Information and Multimedia Technology, 2009. ICIMT '09. International Conference on Digital Object Identifier: 10.1109/ICIMT.2009.26. Publication Year: 2009 , Page(s): 310– 314.
[36] Nethercote, N., Walsh, R. and Fitzhardinge, J.: Building Workload Characterization Tools with Valgrind. Workload Characterization, 2006 IEEE International Symposium on Digital Object Identifier: 10.1109/IISWC.2006.302723 Publication Year: 2006 , Page(s): 2.
[37] Robson, D., and Strazdins, P.: Parallelisation of the Valgrind Dynamic Binary Instrumentation Framework Parallel and Distributed Processing with Applications, 2008. ISPA '08. International Symposium on Digital Object Identifier: 10.1109/ISPA.2008.94. Publication Year: 2008 , Page(s): 113– 121.
[38] Laurenzano, M.A., Tikir, M.M., Carrington, L. and Snavely, A.: PEBIL: Efficient static binary instrumentation for Linux Performance Analysis of Systems & Software (ISPASS), 2010 IEEE International Symposium on Digital Object Identifier: 10.1109/ISPASS.2010.5452024. Publication Year: 2010 , Page(s): 175– 183.
[39] Holger Hoos and Thomas Stutzle: SATLIB: The Satisfiability Library. Web site at:http://www.satlib.org/
[40] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Schulz, and R. Sebastiani: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In Tools and Algorithms for the Construction and Analysis of Systems, 11th Int. Conf., (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 317-333, 2005.
[41] SMT Competitions. http://www.smtcomp.org/
[42] V. Ganesh and D. Dill: STP: A decision procedure for bitvectors and arrays. Under submission, 2007. http://theory.stanford.edu/~vganesh/stp.html
[43] STP (Simple Theorem Prover). http://sourceforge.net/projects/stp-fast-prover
[44] C. Barrett, L. de Moura, and A. Stump: SMT-COMP: Satisfiability Modulo Theories Competition. In K. Etessami and S. Rajamani, editors, 17th InternationalConference on Computer Aided Verification, pages 20-23. Springer, 2005.
[45] SMT-LIB. http://www.smtlib.org/
[46] Detlefs, D., Nelson, G., and Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005).
[47] R. Majumdar and K. Sen: Hybrid concolic testing. In Proc.ICSE, pages 416–426, 2007.
[48] Month of Browser Bugs, July 2006. Web page: http://browserfun.blogspot.com/
[49] P. Godefroid: Compositional Dynamic Test Generation. In Proceedings of POPL’2007 (34th ACM Symposium on Principles of Programming Languages), pages 47–54, Nice, January 2007.
[50] P. McMinn: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab., 14(2):105–156, 2004.
[51] Xu Xiao, Xiao-song Zhang, and Xiong-da Li: New Approach to Path Explosion Problem of Symbolic Execution. Pervasive Computing Signal Processing and Applications (PCSPA), 2010 First International Conference on Digital Object Identifier: 10.1109/PCSPA.2010.80. Publication Year: 2010 , Page(s): 301– 304.
[52] Microsoft Security Bulletin MS06-001. www.microsoft.com/technet/security/bulletin/ms06-001.mspx
[53] CVE-2010-0188. http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2010-0188
[54] Windows Metafile Format (wmf) Specification. http://download.microsoft.com/download/0/B/E/0BE8BDD7-E5E8-422A-ABFD-4342ED7AD886/WindowsMetafileFormat(wmf)Specification.pdf
[55] TIFF format Specification. http://partners.adobe.com/public/developer/tiff/index.html#spec
[56] S. Bhansali, W. Chen, S. De Jong, A. Edwards, and M. Drinic: Framework for instruction-level tracing and analysis of programs. In Second International Conference on Virtual Execution Environments VEE, 2006.
[57] S. Narayanasamy, Z. Wang, J. Tigani, A. Edwards, and B. Calder: Automatically classifying benign and harmful data races using replay analysis. In Programming Languages Design and Implementation (PLDI), 2007.
[2] J. Newsome and D. Song: Dynamic Taint Analysis for Automatic Detection, Analysis, and Signature Generation of Exploits on Commodity Software. In Proceedings of the Network and Distributed System Security Symposium (NDSS 2005)
[3] W. Halfond, A. Orso, and P. Manolios: Using Positive Tainting and Syntax-aware Evaluation to Counter SQL Injection Attacks. InSIGSOFT’06/FSE-14: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, pages 175–185, New York, NY, USA, 2006.
[4] A. Nguyen-Tuong, S. Guarnieri, D. Greene, J. Shirley, and D. Evans: Automatically Hardening Web Applications Using Precise Tainting. In 20th IFIP International Information Security Conference, 2005.
[5] Shao Lin, Zhang Xiaosong, and Su Enbiao: New Method of software vulnerability detection based on fuzzing. Computer Application Research, 2009, 26(3): 1086-1088.
[6] Feng Qin, Cheng Wang, Zhenmin Li, Ho-seop Kim, Yuanyuan Zhou, and Youfeng Wu: LIFT: A Low-Overhead Practical Information Flow Tracking System for Detecting Security Attacks.Microarchitecture, 2006. MICRO-39. 39th Annual IEEE/ACM International Symposium on Digital Object Identifier: 10.1109/MICRO.2006.29 Publication Year: 2006 , Page(s): 135– 148.
[7] J.C. King: Symbolic execution and program testing. Commun. ACM 19(7), 385–394(1976).
[8] YoungHan Choi, HyoungChun Kim, and DoHoon Lee: Tag-Aware Text File Fuzz Testing for Security of a Software System. Convergence Information Technology, 2007. International Conference onVolume , Issue , 21-23 Nov. 2007 Page(s):2254–2259.
[9] Liu Guang-Hong, Wu Gang, Tao Zheng, Shuai Jian-Mei, and Tang Zhuo-Chun: Vulnerability Analysis for X86 Executables Using Genetic Algorithm and Fuzzing. Convergence and Hybrid Information Technology, 2008. ICCIT apos; 08. Third International Conference on Volume 2, Issue, 11-13 Nov. 2008 Page(s): 491– 497.
[10] James Clause, Wanchun Li, and Alessandro Orso: Dytan: A Generic Dynamic Taint Analysis Framework.International symposium on Software testing and analysis(2007). Pages: 196-206.
[11]李佳静,王铁磊,韦韬,凤旺森,邹维:一种多项式时间的路径敏感的污点分析方法.计算机学报.2009.V09.
[12]周孔伟,蔡经球:符号执行—介于程序验证和程序调试之间的方法.小型微型计算机系统.1982.V04.
[13]林锦滨,张晓菲,刘晖:符号执行技术研究.全国计算机安全学术交流会论文集(第二十四卷)2008.V03.
[14] Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215–222 (1976).
[15] Ball, T.,Majumdar,R.,Millstein, T.,Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of PLDI (2001).
[16] Khurshid, S., Pǎsǎreanu, C.S., and Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS (2003).
[17] C. S. Pǎsǎreanu and W. Visser: A survey of new trends in symbolic execution for software testing and analysis.
[18] Anand, S., Pǎsǎreanu, C.S., and Visser, W.: JPF-SE: A symbolic execution extension to Java PathFinder. In: Proceedings of TACAS (2007).
[19] Pǎsǎreanu, C.S., Mehlitz, P., Bushnell, D., Gundy-Burlet, K., Lowry, M., Person, S., and Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In: Proceedings of ISSTA (2008).
[20] D. Brumley, C. Hartwig, M. G. Kang, Z. Liang, J. Newsome, D. Song, and H. Yin: BitScope: Automatically dissecting malicious binaries. Technical Report CMU-CS-07-133, School of Computer Science, Carnegie Mellon University, March 2007.
[21] Godefroid, P., Klarlund, N., and Sen, K.: DART: directed automated random testing.In: Proceedings of PLDI (2005).
[22] Sen, K., Marinov, D., and Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC/FSE (2005).
[23] Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., and Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of ACM Conference on Computer and Communications Security 2006).
[24] PEX: Automated Exploratory Testing for .NET: http://research.microsoft.com/Pex
[25] N. Nethercote and J. Seward: Valgrind: A frameworkfor heavyweight dynamic binary instrumentation. In PLDI, 2007.
[26] V. Ganesh, T. Leek, and M. Rinard: Taint-based Directed Whitebox Fuzzing Software Engineering, 2009. ICSE 2009. IEEE 31st International Conference on 16-24 May 2009 Page(s):474 - 484.
[27] P. Godefroid, M. Y. Levin, and D. Molnar: Automated Whitebox Fuzz Testing. Technical Report MS-TR-2007-58, Microsoft, May 2007. See http://research.microsoft.com/users/pg/.
[28] The Choco Constraint Solver: http://choco.sourceforge.net/
[29] IASolver (The Brandeis Interval Arithmetic Constraint Solver): http://www.cs.brandeis.edu/~tim/Applets/IAsolver.html/
[30] Yices: An SMT Solver. http://yices.csl.sri.com/
[31] Luk, C., Cohn, R., Muth, R., Patil, H., Klauser, A., Lowney, G., Wallace, S., Vijay Janapa Reddi, and Hazelwood, K: Pin: building customized program analysis tools with dynamic instrumentation. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL, USA, June 12 - 15, 2005). 190-200.
[32] De Moura, L., Bj(?)rner, N., et al.: Z3: an efficient SMT solver. Software and documentation available at http://research.microsoft.com/projects/z3 (2006–2008).
[33] Probst, M., Krall, A., and Scholz, B: Register liveness analysis for optimizing dynamic binary translation.Reverse Engineering, 2002. Proceedings. Ninth Working Conference on Digital Object Identifier: 10.1109/WCRE.2002.1173062.Publication Year: 2002 , Page(s): 35– 44.
[34] Hui Shu, and Yongjun He: Research on protocol reverse extraction based on DynamoRIO. Communication Systems, Networks and Applications (ICCSNA),2010 Second International Conference on Volume:1. Digital Object Identifier: 10.1109/ICCSNA.2010.5588804. Publication Year: 2010 , Page(s): 5– 9.
[35] Yongjun He, Hui Shu, and Xiaobing Xiong: Protocol Reverse Engineering Based on DynamoRIO. Information and Multimedia Technology, 2009. ICIMT '09. International Conference on Digital Object Identifier: 10.1109/ICIMT.2009.26. Publication Year: 2009 , Page(s): 310– 314.
[36] Nethercote, N., Walsh, R. and Fitzhardinge, J.: Building Workload Characterization Tools with Valgrind. Workload Characterization, 2006 IEEE International Symposium on Digital Object Identifier: 10.1109/IISWC.2006.302723 Publication Year: 2006 , Page(s): 2.
[37] Robson, D., and Strazdins, P.: Parallelisation of the Valgrind Dynamic Binary Instrumentation Framework Parallel and Distributed Processing with Applications, 2008. ISPA '08. International Symposium on Digital Object Identifier: 10.1109/ISPA.2008.94. Publication Year: 2008 , Page(s): 113– 121.
[38] Laurenzano, M.A., Tikir, M.M., Carrington, L. and Snavely, A.: PEBIL: Efficient static binary instrumentation for Linux Performance Analysis of Systems & Software (ISPASS), 2010 IEEE International Symposium on Digital Object Identifier: 10.1109/ISPASS.2010.5452024. Publication Year: 2010 , Page(s): 175– 183.
[39] Holger Hoos and Thomas Stutzle: SATLIB: The Satisfiability Library. Web site at:http://www.satlib.org/
[40] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Schulz, and R. Sebastiani: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In Tools and Algorithms for the Construction and Analysis of Systems, 11th Int. Conf., (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 317-333, 2005.
[41] SMT Competitions. http://www.smtcomp.org/
[42] V. Ganesh and D. Dill: STP: A decision procedure for bitvectors and arrays. Under submission, 2007. http://theory.stanford.edu/~vganesh/stp.html
[43] STP (Simple Theorem Prover). http://sourceforge.net/projects/stp-fast-prover
[44] C. Barrett, L. de Moura, and A. Stump: SMT-COMP: Satisfiability Modulo Theories Competition. In K. Etessami and S. Rajamani, editors, 17th InternationalConference on Computer Aided Verification, pages 20-23. Springer, 2005.
[45] SMT-LIB. http://www.smtlib.org/
[46] Detlefs, D., Nelson, G., and Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005).
[47] R. Majumdar and K. Sen: Hybrid concolic testing. In Proc.ICSE, pages 416–426, 2007.
[48] Month of Browser Bugs, July 2006. Web page: http://browserfun.blogspot.com/
[49] P. Godefroid: Compositional Dynamic Test Generation. In Proceedings of POPL’2007 (34th ACM Symposium on Principles of Programming Languages), pages 47–54, Nice, January 2007.
[50] P. McMinn: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab., 14(2):105–156, 2004.
[51] Xu Xiao, Xiao-song Zhang, and Xiong-da Li: New Approach to Path Explosion Problem of Symbolic Execution. Pervasive Computing Signal Processing and Applications (PCSPA), 2010 First International Conference on Digital Object Identifier: 10.1109/PCSPA.2010.80. Publication Year: 2010 , Page(s): 301– 304.
[52] Microsoft Security Bulletin MS06-001. www.microsoft.com/technet/security/bulletin/ms06-001.mspx
[53] CVE-2010-0188. http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2010-0188
[54] Windows Metafile Format (wmf) Specification. http://download.microsoft.com/download/0/B/E/0BE8BDD7-E5E8-422A-ABFD-4342ED7AD886/WindowsMetafileFormat(wmf)Specification.pdf
[55] TIFF format Specification. http://partners.adobe.com/public/developer/tiff/index.html#spec
[56] S. Bhansali, W. Chen, S. De Jong, A. Edwards, and M. Drinic: Framework for instruction-level tracing and analysis of programs. In Second International Conference on Virtual Execution Environments VEE, 2006.
[57] S. Narayanasamy, Z. Wang, J. Tigani, A. Edwards, and B. Calder: Automatically classifying benign and harmful data races using replay analysis. In Programming Languages Design and Implementation (PLDI), 2007.