DSD-Crasher: A hybrid analysis tool for bug finding

ABSTRACT

DSD-Crasher is a bug finding tool that follows a three-step approach to program analysis:

D. Capture the program's intended execution behavior with dynamic invariant detection. The derived invariants exclude many unwanted values from the program's input domain.

S. Statically analyze the program within the restricted input domain to explore many paths.

D. Automatically generate test cases that focus on reproducing the predictions of the static analysis. Thereby confirmed results are feasible.

This three-step approach yields benefits compared to past two-step combinations in the literature. In our evaluation with third-party applications, we demonstrate higher precision over tools that lack a dynamic step and higher efficiency over tools that lack a static step.

REFERENCES

• 1: Anand, S., Godefroid, P., and Tillmann, N. 2008. Demand-driven compositional symbolic execution. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, To appear.
• 2: Anand, S., Pasareanu, C., and Visser, W. 2007. JPF-SE: A symbolic execution extension to Java Pathfinder. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 134--138.
• 3: Apache Software Foundation. 2003. Bytecode engineering library (BCEL). http://jakarta.apache.org/bcel/. (Accessed Dec. 2007.)
• 4: Artzi, S., Ernst, M. D., Kieżun, A., Pacheco, C., and Perkins, J. H. 2006. Finding the needles in the haystack: Generating legal test inputs for object-oriented programs. In Proceedings of the 1st International Workshop on Model-Based Testing and Object-Oriented Systems (M-TOOS).
• 5: Ball, T. 2003. Abstraction-guided test generation: A case study. Tech. rep. MSR-TR-2003-86, Microsoft Research.
• 6: Beck, K. and Gamma, E. 1998. Test infected: Programmers love writing tests. Java Report 3, 7, 37--50.
• 7: Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
• 8: Marat Boshernitsan , Roongko Doong , Alberto Savoia, From daikon to agitator: lessons and challenges in building a commercial tool for developer testing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146258]
• 9: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 10: 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]
• 11: Centonze, P., Flynn, R. J., and Pistoia, M. 2007. Combining static and dynamic analysis for automatic identification of precise access-control policies. In Proceedings of the 23rd Annual Computer Security Applications Conference (ACSAC). IEEE, 292--303.
• 12: L. A. Clarke, A System to Generate Test Data and Symbolically Execute Programs, IEEE Transactions on Software Engineering, v.2 n.3, p.215-222, May 1976 [doi>10.1109/TSE.1976.233817]
• 13: Cok, D. R. and Kiniry, J. R. 2004. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2. Tech. rep. NIII-R0413, Nijmegen Institute for Computing and Information Science.
• 14: Coverity Inc. 2003. Coverity Prevent. http://www.coverity.com/. (Accessed Dec. 2007).
• 15: Christoph Csallner , Yannis Smaragdakis, JCrasher: an automatic robustness tester for Java, Software—Practice & Experience, v.34 n.11, p.1025-1050, September 2004 [doi>10.1002/spe.602]
• 16: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 17: Christoph Csallner , Yannis Smaragdakis, DSD-Crasher: a hybrid analysis tool for bug finding, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146267]
• 18: Christoph Csallner , Yannis Smaragdakis, Dynamically discovering likely interface invariants, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134435]
• 19: Christoph Csallner , Nikolai Tillmann , Yannis Smaragdakis, DySy: dynamic symbolic execution for invariant inference, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368127]
• 20: Marcelo d'Amorim , Carlos Pacheco , Tao Xie , Darko Marinov , Michael D. Ernst, An Empirical Comparison of Automated Generation and Classification Techniques for Object-Oriented Unit Testing, Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, p.59-68, September 18-22, 2006 [doi>10.1109/ASE.2006.13]
• 21: Xianghua Deng , Jooyong Lee , Robby, Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems, Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, p.157-166, September 18-22, 2006 [doi>10.1109/ASE.2006.26]
• 22: Xianghua Deng , Robby , John Hatcliff, Kiasan/KUnit: Automatic Test Case Generation and Analysis Feedback for Open Object-oriented Systems, Proceedings of the Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION, p.3-12, September 10-14, 2007
• 23: Detlefs, D., Nelson, G., and Saxe, J. B. 2003. Simplify: A theorem prover for program checking. Tech. rep. HPL-2003-148, Hewlett-Packard Systems Research Center.
• 24: Hyunsook Do , Sebastian Elbaum , Gregg Rothermel, Supporting Controlled Experimentation with Testing Techniques: An Infrastructure and its Potential Impact, Empirical Software Engineering, v.10 n.4, p.405-435, October 2005 [doi>10.1007/s10664-005-3861-2]
• 25: Engler, D. and Musuvathi, M. 2004. Static analysis versus software model checking for bug finding. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 191--210.
• 26: Ernst, M. D. 2003. Static and dynamic analysis: Synergy and duality. In Proceedings of the ICSE Workshop on Dynamic Analysis (WODA). 24--27.
• 27: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 28: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 29: Patrice Godefroid, Compositional dynamic test generation, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 30: 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
• 31: Neelam Gupta , Aditya P. Mathur , Mary Lou Soffa, Automated test data generation using an iterative relaxation method, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.231-244, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 32: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 33: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 34: Hapner, M., Burridge, R., Sharma, R., and Fialli, J. 2002. Java Message Service: Version 1.1. Sun Microsystems, Inc.
• 35: Henkel, J., Reichenbach, C., and Diwan, A. 2007. Discovering documentation for Java container classes. IEEE Trans. Softw. Engin. 33, 8, 526--543.
• 36: David Hovemeyer , William Pugh, Finding bugs is easy, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028717]
• 37: Daniel Jackson , Martin Rinard, Software analysis: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.133-145, June 04-11, 2000, Limerick, Ireland [doi>10.1145/336512.336545]
• 38: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 39: Khurshid, S., Pasareanu, C. S., and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 553--568.
• 40: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 41: Joseph R. Kiniry , Alan E. Morkan , Barry Denby, Soundness and completeness warnings in ESC/Java2, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181200]
• 42: B. Korel, Automated Software Test Data Generation, IEEE Transactions on Software Engineering, v.16 n.8, p.870-879, August 1990 [doi>10.1109/32.57624]
• 43: Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , Dawson Engler, From uncertainty to belief: inferring the specification within, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
• 44: Kroening, D., Groce, A., and Clarke, E. M. 2004. Counterexample guided abstraction refinement via program execution. In Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM). Springer, 224--238.
• 45: Leavens, G. T., Baker, A. L., and Ruby, C. 1998. Preliminary design of JML: A behavioral interface specification language for Java. Tech. rep. TR98-06y, Department of Computer Science, Iowa State University.
• 46: Leino, K. R. M., Nelson, G., and Saxe, J. B. 2000. ESC/Java user's manual. Tech. rep. 2000-002, Compaq Computer Corporation Systems Research Center.
• 47: McConnell, S. 2004. Code Complete, 2nd Ed. Microsoft Press.
• 48: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 49: Meyer, B., Ciupa, I., Leitner, A., and Liu, L. 2007. Automatic testing of object-oriented software. In Proceedings of the 33rd Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM). Springer, 114--129.
• 50: Jeremy W. Nimmer , Michael D. Ernst, Automatic generation of program specifications, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 51: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
• 52: Pacheco, C. and Ernst, M. D. 2005. Eclat: Automatic generation and classification of test inputs. In Proceedings of the 19th European Conference on Object-Oriented Programming (ECOOP). Springer, 504--527.
• 53: Parasoft Inc. 2002. Jtest. http://www.parasoft.com/. Accessed Dec. 2007.
• 54: Nick Rutar , Christian B. Almazan , Jeffrey S. Foster, A Comparison of Bug Finding Tools for Java, Proceedings of the 15th International Symposium on Software Reliability Engineering, p.245-256, November 02-05, 2004 [doi>10.1109/ISSRE.2004.1]
• 55: Schlenker, H. and Ringwelski, G. 2002. POOC: A platform for object-oriented constraint programming. In Proceedings of the Joint ERCIM/CologNet International Workshop on Constraint Solving and Constraint Logic Programming. Springer, 159--170.
• 56: Sen, K. and Agha, G. 2006. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV). Springer, 419--423.
• 57: 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
• 58: Smaragdakis, Y. and Csallner, C. 2007. Combining static and dynamic reasoning for bug detection. In Proceedings of the 1st International Conference on Tests And Proofs (TAP). Springer, 1--16.
• 59: Mana Taghdiri , Robert Seater , Daniel Jackson, Lightweight extraction of syntactic specifications, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181809]
• 60: Aaron Tomb , Guillaume Brat , Willem Visser, Variably interprocedural program analysis for runtime error detection, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273478]
• 61: Vaziri, M. and Jackson, D. 2003. Checking properties of heap-manipulating procedures with a constraint solver. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 505--520.
• 62: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 63: Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 64: Wagner, S., Jürjens, J., Koller, C., and Trischberger, P. 2005. Comparing bug finding tools with reviews and tests. In Proceedings of the 17th IFIP TC6/WG 6.1 International Conference on Testing of Communicating Systems (TestCom). Springer, 40--55.
• 65: John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 66: Xie, T. and Notkin, D. 2003. Tool-assisted unit test selection based on operational violations. In Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE). IEEE, 40--48.
• 67: Xie, Y. and Engler, D. 2003. Using redundancies to find errors. IEEE Trans. Softw. Engin. 29, 10, 915--928.
• 68: Young, M. 2003. Symbiosis of static analysis and program testing. In Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering (FASE). Springer, 1--5.
• 69: Hong Zhu , Patrick A. V. Hall , John H. R. May, Software unit test coverage and adequacy, ACM Computing Surveys (CSUR), v.29 n.4, p.366-427, Dec. 1997 [doi>10.1145/267580.267590]
• 70: Misha Zitser , Richard Lippmann , Tim Leek, Testing static analysis tools using exploitable buffer overflows from open source code, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Reliability, Verification

Keywords:
Automatic testing, bug finding, dynamic analysis, dynamic invariant detection, extended static checking, false positives, static analysis, test case generation, usability