- 倪康奇 2009级硕士 程序分析
- Email: firstname.lastname@example.org
- Motto：Search for solutions rather than excuses.
- Title: A Dynamic Symbolic Execution Tool for x86 Binary Programs
- Program analysis is playing an important role in the field of computer security. It is useful for the evaluation of both applications and operating system. Nowadays, there are many program analysis approaches. Taint analysis and symbolic execution have been the most popular and effective technique among the others. Typically, symbolic execution is more precise than the taint analysis, and becomes the great research topic in the field of program analysis all over the world.
- Traditional symbolic execution replaces the concrete variables with symbols, and runs the program. At the branch instruction, symbolic execution establishes a constraint, and gathers all the constraints to form a path condition along the program path. The program input that satisfies such a path condition can lead the program to the corresponding path.
- However, traditional symbolic execution suffers from several severe problems such as state explosion, complex mathematical constraints, low efficiency, etc. In order to tackle those problems, we present a lightweight dynamic symbolic execution tool, LDSE. LDSE mixes dynamic and symbolic execution, and deploys the dynamic backward program slicing to effectively relieve the existing issues.
- LDSE introduces four contributions:
- 1) A compact unified memory model.
- 2) Instruction cache.
- 3) Dynamic backward program slicing.
- 4) A lightweight dynamic symbolic execution framework for x86 programs.
- Our experiment results show that the lightweight dynamic symbolic execution tool can be applied in both testcase generation and program path coverage. Typically, dynamic backward program slicing makes the symbolic execution degrade gracefully.
- Key words: binary analysis, symbolic execution, dynamic backward program slicing
- Full text
-  King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976).
-  Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing.SIGPLAN Notices 40(6), 213–223 (2005).
-  Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: automatically generating inputs of death. In: CCS 2006: Proceedings of the 13th ACM conference on Computer and communications security, pp. 322–335. ACM Press,New York (2006).
-  P. Saxena, P. Poosankam, S. McCamant, and D. Song. Loop-extended symbolic execution on binary programs. In International Symposium on Software Testing and Analysis, Chicago, IL, July 2009.
-  Godefroid, P.: Compositional dynamic test generation. In: POPL 2007: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 47–54. ACM Press, New York (2007).
-  Godefroid, P., Levin, M.Y., Molnar, D.: Automated whitebox fuzz testing. Technical Report MSR-TR-2007-58, Microsoft Research, Redmond, WA (May 2007).
-  N. Tillmann and J. de Halleux. Pex – white box test generation for .NET. In Proc. Second International Conference on Tests and Proofs (TAP). Springer, Apr. 2008.
-  C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008.
-  Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for c. In: ESEC/FSE-13: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 263–272. ACM Press, New York (2005).
-  Anand, S., Pasareanu, C.S., Visser, W.: Jpf-se: A symbolic execution extension to java pathfinder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 134–138. Springer, Heidelberg (2007).
-  Dawn Song, David Brumley, Heng Yin, Juan Caballero, Ivan Jager, Min Gyung Kang, Zhenkai Liang, James Newsome, Pongsin Poosankam, and Prateek Saxena. BitBlaze: A new approach to computer security via binary analysis. In International Conference on Information Systems Security, Hyderabad, India, December 2008. Keynote invited paper.
-  C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself (invited paper). In SPIN’05, Aug 2005.
-  Xu Z, Zhang J. A test data generation tool for unit testing of C programs. Proceedings of the QSIC. Beijing, China, 2006: 107-116.
-  Korel B, Laski J. Dynamic slicing of computer programs [J]. J Systems and Software, 1990, 13(3): 187-195.
-  Korel B, Rilling J. Dynamic program slicing methods [J]. Information and Software Technology, 1998, 40(11): 647-659.
-  MASSACHUSETTS INSTITUTE OF TECHNOLOGY. Dynamic Instrumentation Tool Platform. http://dynamorio.org/.
-  Nicholas Nethercote, Julian Seward. Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation [C]. Proceedings of PLDI’07. San Diego, USA. June 2007.
-  Chi-Keung Luk, Robert S. Cohn, Robert Muth, Harish Patil, Artur Klauser, P. Geoffrey Lowney, Steven Wallace, Vijay Janapa Reddi, Kim M. Hazelwood: Pin: building customized program analysis tools with dynamic instrumentation. PLDI 2005.
-  L. de Moura and N. Bjorner, "Z3: An Efficient Smt Solver," Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2008.
-  UNIVERSITY OF ILLINOIS AT URBANA-CHAMPAIGN. The LLVM Compiler Infrastructure. http://llvm.org/.
-  WANG, T., WEI, T., LIN, Z., AND ZOU, W. Intscope: Automatically detecting integer overflow vulnerability in x86 binary using symbolic execution. In Network Distributed Security Symposium (NDSS) (2009), Citeseer.
-  ZHANG, L., XIE, T., ZHANG, L., TILLMANN, N., DE HALLEUX, J., AND MEI, H. Test generation via dynamic symbolic execution for mutation testing. In Software Maintenance (ICSM), 2010 IEEE International Conference on (2010), IEEE, pp. 1–10.
-  林锦滨, 张晓菲，刘晖. 符号执行技术研究. 全国计算机安全学术交流会论文集. pp. 404-408.
-  http://www.intel.com/products/processor/manuals/.
-  C. Cadar, P. Godefroid, S. Khurshid, C.S. Pasareanu, K. Sen, N. Tillmann, and W. Visser.: Symbolic Execution for Software Testing in Practice – Preliminary Assessment. In Proceedings of ICSE’2011, Honolulu. (2011).
-  R. Santelices and M. J. Harrold.: Exploiting program dependencies for scalable multiple-path symbolic execution. In Proc. of Int’l Symp. on Softw. Testing and Analysis, pp. 195-206. Jul. (2010).
-  S. Artzi, A. Kiezun, J. Dolby, F. Tip, D. Dig, A. Paradkar, and M. D. Ernst.: Finding bugs in dynamic web applications. In ISSTA’08. (2008).
-  M. Baluda, P. Braione, G. Denaro, and M. Pezze.: Structural Coverage of Feasible Code. In AST’10, pages 59-66. ACM. (2010).
-  http://www.microsoft.com/technet/security/Bulletin/MS10-005.mspx/.
-  ALBARCHOUTHI, A., GURFINKEL, A., WEI, O., AND CHECKHIK, M. Abstract Analysis of Symbolic Executions. 495-510.
-  COSTA, M., CASTRO, M., ZHOU, L., ZHANG, L., AND PEINADO, M. Bouncer: Securing software by blocking bad input. 117-130.
-  ZHANG, L., XIE, T., ZHANG, L., TILLMANN, N., DE HALLEUX, J., AND MEI, H. Test generation via dynamic symbolic execution for mutation testing. In Software Maintenance (ICSM), 2010 IEEE International Conference on (2010), IEEE, pp. 1-10.
-  http://cseweb.ucsd.edu/classes/sp00/cse231/report/node12.html/.
-  http://xen.org/.
All the time you invest learning will serve you well in the future.
Doc & Patent
1、Coverage Maximization Using Dynamic Taint Tracing
2、CIL:Intermediate Language and Tools for Analysis and Transformation of C programs
3、Intraprocedural Static Slicing of Binary Executables
4、BintHunt: Automatically Finding Semantic Differences in Binary Programs
5、TEMU: Binary Code Analysis via Whole-System Layered Annotative Execution
6、All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution
7、Cute: A Concolic Unit Testing Engine for C