EXE: Automatically Generating Inputs of Death

ABSTRACT

This article 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 dhcpd DHCP server, the pcre regular expression library, and three Linux file systems.

REFERENCES

• 1: Ball, T. 2004. A theory of predicate-complete test coverage and generation. In Proceedings of the 3rd International Symposium on Formal Methods for Components and Objects (FMCO’04).
• 2: Ball, T. and Jones, R. B., eds. 2006. Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), Seattle, WA. Lecture Notes in Computer Science, vol. 4144. Springer.
• 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: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 6: Barrett, C., Berezin, S., Shikanian, I., Chechik, M., Gurfinkel, A., and Dill, D. L. 2004. A practical approach to partial functions in CVC Lite. In Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR’04), Cork, Ireland.
• 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, 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: Cadar, C. and Engler, D. 2005. Execution generated test cases: How to make systems code crash itself. In Proceedings of the 12th International SPIN Workshop on Model Checking of Software (SPIN’05). A longer version of this article appeared as Tech. rep. CSTR-2005-04, Computer Systems Laboratory, Stanford University.
• 13: 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]
• 14: 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]
• 15: Cook, B., Kroening, D., and Sharygina, N. 2005. Cogent: Accurate theorem proving for program verification. In Proceedings of the Conference on Computer-Aided Verification (CAV’05), K. Etessami and S. K. Rajamani Eds. Lecture Notes in Computer Science, vol. 3576. Springer Verlag, 296--300.
• 16: 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]
• 17: Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
• 18: Coverity. SWAT: the Coverity software analysis toolset. http://coverity.com.
• 19: 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
• 20: 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
• 21: Een, N. and Sorensson, N. 2003. An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT’03). 78--92.
• 22: 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]
• 23: 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
• 24: 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
• 25: 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
• 26: 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]
• 27: 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
• 28: 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
• 29: 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
• 30: Hastings, R. and Joyce, B. 1992. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference (USENIX’92).
• 31: 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]
• 32: 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
• 33: 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’03).
• 34: Eric Larson , Todd Austin, High coverage detection of input-related security facults, Proceedings of the 12th conference on USENIX Security Symposium, p.9-9, August 04-08, 2003, Washington, DC
• 35: 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]
• 36: 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
• 37: 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]
• 38: Nethercote, N. and Seward, J. 2003. Valgrind: A program supervision framework. Electron. Notes Theor. Comput. Sci. 89, 2.
• 39: PCRE. PCRE - Perl Compatible Regular Expressions. http://www.pcre.org/.
• 40: PCRE - CERT 2005. PCRE Regular Expression Heap Overflow. US-CERT Cyber Security Bulletin SB05-334. http://www.us-cert.gov/cas/bulletins/SB05-334.html#pcre.
• 41: Ruwase, O. and Lam, M. S. 2004. A practical dynamic buffer overflow detector. In Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS’04). 159--169.
• 42: 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
• 43: SMTLIB 2006. SMTLIB competition. http://www.csl.sri.com/users/demoura/smt-comp.
• 44: Wagner, D., Foster, J., Brewer, E., and Aiken, A. 2000. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of the Network and Distributed Systems Security Conference (NDSS’00). San Diego, CA.
• 45: 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
• 46: Xie, Y. and Aiken, A. 2005. Saturn: A SAT-based tool for bug detection. In Proceedings of the Conference on Computer-Aided Verification (CAV’05), K. Etessami and S. K. Rajamani Eds. Lecture Notes in Computer Science, vol. 3576. Springer, 139--143.
• 47: 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, p.243-257, May 21-24, 2006 [doi>10.1109/SP.2006.7]
• 48: Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.19-19, December 06-08, 2004, San Francisco, CA

INDEX TERMS

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