Precise pointer reasoning for dynamic test generation

ABSTRACT

Dynamic test generation consists of executing a program while gathering symbolic constraints on inputs from predicates encountered in branch statements, and of using a constraint solver to infer new program inputs from previous constraints in order to steer next executions towards new program paths. Variants of this technique have recently been adopted in several bug detection tools, including our whitebox fuzzer SAGE, which has found dozens of new expensive security-related bugs in many Windows applications and is now routinely used in various Microsoft groups.

In this paper, we discuss how to perform precise symbolic pointer reasoning in the context of dynamic test generation. We present a new memory model for representing arbitrary symbolic pointer dereferences to memory regions accessible by a program during its execution, and show that this memory model is the most precise one can hope for in our context, under some realistic assumptions. We also describe how the symbolic constraints generated by our model can be solved using modern SMT solvers, which provide powerful constructs for reasoning about bit-vectors and arrays. This new memory model has been implemented in SAGE, and we present results of experiments with several large Windows applications showing that an increase in precision can often be obtained at a reasonable cost. Better precision in symbolic pointer reasoning means more relevant constraints and fewer imprecise ones, hence better test coverage, more bugs found and fewer redundant test cases.

REFERENCES

• 1: D. Babic and A. J. Hu. Structural Abstraction of Software Verification Conditions. In Proceedings of CAV'2007 (19th Conference on Computer Aided Verification), Berlin, July 2007.
• 2: M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of FMCO'2005 (4th International Symposium on Formal Methods for Components and Objects), volume 4111 of LNCS, pages 364--387. Springer, September 2006.
• 3: Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180445]
• 4: E. Clarke, D. Kroening, and F. Lerda. A Tool for Checking ANSI-C Programs. In Proceedings of TACAS'2004 (Tools and Algorithms for the Construction and Analysis of Systems), volume 2988 of Lecture Notes in Computer Science, pages 168--176. Springer, 2004.
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: L. de Moura and N. Bjorner. Z3: An Efficient SMT Solver. In TACAS '08: Tools and Algorithms for the Construction and Analysis of Systems, 2008.
• 7: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 8: Patrice Godefroid , Michael Y. Levin , David A. Molnar, Active property checking, Proceedings of the 8th ACM international conference on Embedded software, October 19-24, 2008, Atlanta, GA, USA [doi>10.1145/1450058.1450087]
• 9: P. Godefroid, M.Y. Levin, and D. Molnar. Automated Whitebox Fuzz Testing. In Proceedings of NDSS'2008 (Network and Distributed Systems Security), pages 151--166, San Diego, February 2008.
• 10: Satish Narayanasamy , Zhenghao Wang , Jordan Tigani , Andrew Edwards , Brad Calder, Automatically classifying benign and harmful data racesallusing replay analysis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 11: Pex. Web page: http://research.microsoft.com/Pex.
• 12: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.16-31, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237725]
• 13: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 14: Dries Vanoverberghe , Nikolai Tillmann , Frank Piessens, Test Input Generation for Programs with Pointers, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,, March 22-29, 2009, York, UK [doi>10.1007/978-3-642-00768-2_25]
• 15: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 16: Ru-Gang Xu , Patrice Godefroid , Rupak Majumdar, Testing for buffer overflows with length abstraction, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA [doi>10.1145/1390630.1390636]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Reliability, Security, Verification

Keywords:
automatic test generation, pointer reasoning, program verification, software testing