EXE: automatically generating inputs of death

ABSTRACT

This paper presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code. Instead of running code on manually or randomly constructed input, EXE runs it on symbolic input initially allowed to be "anything." As checked code runs, EXE tracks the constraints on each symbolic (i.e., input-derived) memory location. If a statement uses a symbolic value, EXE does not run it, but instead adds it as an input-constraint; all other statements run as usual. If code conditionally checks a symbolic expression, EXE forks execution, constraining the expression to be true on the true branch and false on the other. Because EXE reasons about all possible values on a path, it has much more power than a traditional runtime tool: (1) it can force execution down any feasible program path and (2) at dangerous operations (e.g., a pointer dereference), it detects if the current path constraints allow any value that causes a bug.When a path terminates or hits a bug, EXE automatically generates a test case by solving the current path constraints to find concrete values using its own co-designed constraint solver, STP. Because EXE's constraints have no approximations, feeding this concrete input to an uninstrumented version of the checked code will cause it to follow the same path and hit the same bug (assuming deterministic code).EXE works well on real code, finding bugs along with inputs that trigger them in: the BSD and Linux packet filter implementations, the udhcpd DHCP server, the pcre regular expression library, and three Linux file systems.

REFERENCES

• 1: T. Ball. A theory of predicate-complete test coverage and generation. In Proceedings of the Third International Symposium on Formal Methods for Components and Objects, Nov. 2004.
• 2: T. Ball and R. B. Jones, editors. Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science. Springer, 2006.
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 5: C. Barrett and S. Berezin. CVC Lite: A new implementation of the cooperating validity checker. In R. Alur and D. A. Peled, editors, CAV, Lecture Notes in Computer Science. Springer, 2004.
• 6: C. Barrett, S. Berezin, I. Shikanian, M. Chechik, A. Gurfinkel, and D. L. Dill. A practical approach to partial functions in CVC Lite. In PDPAR'04 Workshop, Cork, Ireland, July 2004.
• 7: Robert S. Boyer , Bernard Elspas , Karl N. Levitt, SELECT—a formal system for testing and debugging programs by symbolic execution, ACM SIGPLAN Notices, v.10 n.6, p.234-245, June 1975
• 8: 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
• 9: David Brumley , James Newsome , Dawn Song , Hao Wang , Somesh Jha, Towards Automatic Generation of Vulnerability-Based Signatures, Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P'06), p.2-16, May 21-24, 2006 [doi>10.1109/SP.2006.41]
• 10: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 11: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 12: C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Proceedings of the 12th International SPIN Workshop on Model Checking of Software, August 2005. A longer version of this paper appeared as Technical Report CSTR-2005-04, Computer Systems Laboratory, Stanford University.
• 13: Edmund Clarke , Daniel Kroening, Hardware verification using ANSI-C programs as a reference, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan [doi>10.1145/1119772.1119831]
• 14: B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In K. Etessami and S. K. Rajamani, editors, Proceedings of CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 296--300. Springer Verlag, 2005.
• 15: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 16: Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
• 17: SWAT: the Coverity software analysis toolset. http://coverity.com.
• 18: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 19: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 20: N. Een and N. Sorensson. An extensible SAT-solver. In Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing, pages 78--92, May 2003.
• 21: Roger Ferguson , Bogdan Korel, The chaining approach for software test data generation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.1, p.63-86, Jan. 1996 [doi>10.1145/226155.226158]
• 22: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 23: 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
• 24: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 25: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 26: 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
• 27: Arnaud Gotlieb , Bernard Botella , Michel Rueher, Automatic test data generation using constraint solving techniques, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.53-62, March 02-04, 1998, Clearwater Beach, Florida, United States
• 28: 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
• 29: R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference, Dec. 1992.
• 30: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 31: Gerard J. Holzmann, From Code to Models, Proceedings of the Second International Conference on Application of Concurrency to System Design, p.3, June 25-29, 2001
• 32: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003.
• 33: E. Larson and T. Austin. High coverage detection of input-related security faults. In Proceedings of the 12th USENIX Security Symposium, August 2003.
• 34: Barton P. Miller , Louis Fredriksen , Bryan So, An empirical study of the reliability of UNIX utilities, Communications of the ACM, v.33 n.12, p.32-44, Dec. 1990 [doi>10.1145/96267.96279]
• 35: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 36: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 37: N. Nethercote and J. Seward. Valgrind: A program supervision framework. Electronic Notes in Theoretical Computer Science, 89(2), 2003.
• 38: PCRE - Perl Compatible Regular Expressions. http://www.pcre.org/.
• 39: PCRE Regular Expression Heap Overflow. US-CERT Cyber Security Bulletin SB05-334. http://www.us-cert.gov/cas/bulletins/SB05-334.html#pcre.
• 40: O. Ruwase and M. S. Lam. A practical dynamic buffer overflow detector. In Proceedings of the 11th Annual Network and Distributed System Security Symposium, pages 159--169, 2004.
• 41: 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
• 42: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In The 2000 Network and Distributed Systems Security Conference. San Diego, CA, Feb. 2000.
• 43: 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
• 44: Y. Xie and A. Aiken. Saturn: A SAT-based tool for bug detection. In K. Etessami and S. K. Rajamani, editors, CAV, volume 3576 of Lecture Notes in Computer Science, pages 139--143. Springer, 2005.
• 45: Junfeng Yang , Can Sar , Paul Twohey , Cristian Cadar , Dawson Engler, Automatically Generating Malicious Disks using Symbolic Execution, Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P'06), p.243-257, May 21-24, 2006 [doi>10.1109/SP.2006.7]
• 46: J. Yang, P. Twohey, D. Engler, and M. Musuvathi. Using model checking to find serious file system errors. In Symposium on Operating Systems Design and Implementation, December 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

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

General Terms:
Languages, Reliability

Keywords:
attack generation, bug finding, constraint solving, dynamic analysis, symbolic execution, test case generation