Loop-extended symbolic execution on binary programs

ABSTRACT

Mixed concrete and symbolic execution is an important technique for finding and understanding software bugs, including security-relevant ones. However, existing symbolic execution techniques are limited to examining one execution path at a time, in which symbolic variables reflect only direct data dependencies. We introduce loop-extended symbolic execution, a generalization that broadens the coverage of symbolic results in programs with loops. It introduces symbolic variables for the number of times each loop executes, and links these with features of a known input grammar such as variable-length or repeating fields. This allows the symbolic constraints to cover a class of paths that includes different numbers of loop iterations, expressing loop-dependent program values in terms of properties of the input. By performing more reasoning symbolically, instead of by undirected exploration, applications of loop-extended symbolic execution can achieve better results and/or require fewer program executions. To demonstrate our technique, we apply it to the problem of discovering and diagnosing buffer-overflow vulnerabilities in software given only in binary form. Our tool finds vulnerabilities in both a standard benchmark suite and 3 real-world applications, after generating only a handful of candidate inputs, and also diagnoses general vulnerability conditions.

REFERENCES

• 1: Alfred V. Aho , Monica S. Lam , Ravi Sethi , Jeffrey D. Ullman, Compilers: Principles, Techniques, and Tools (2nd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 2: G. Balakrishnan and T. W. Reps. Analyzing memory accesses in x86 executables. In Compiler Construction, Apr. 2004.
• 3: G. Balakrishnan and T. W. Reps. DIVINE: DIscovering Variables IN Executables. In Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan. 2007.
• 4: BitBlaze: Binary analysis for computer security. http://bitblaze.cs.berkeley.edu/.
• 5: Nikolaj Bjørner , Nikolai Tillmann , Andrei Voronkov, Path Feasibility Analysis for String-Manipulating Programs, 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_27]
• 6: David Brumley , Juan Caballero , Zhenkai Liang , James Newsome , Dawn Song, Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation, Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium, p.1-16, August 06-10, 2007, Boston, MA
• 7: 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]
• 8: David Brumley , Pongsin Poosankam , Dawn Song , Jiang Zheng, Automatic Patch-Based Exploit Generation is Possible: Techniques and Implications, Proceedings of the 2008 IEEE Symposium on Security and Privacy, p.143-157, May 18-21, 2008 [doi>10.1109/SP.2008.17]
• 9: David Brumley , Hao Wang , Somesh Jha , Dawn Song, Creating Vulnerability Signatures Using Weakest Preconditions, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.311-325, July 06-08, 2007 [doi>10.1109/CSF.2007.17]
• 10: J. Caballero, Z. Liang, P. Poosankam, and D. Song. Towards generating high coverage vulnerability-based signatures with protocol-level constraint-guided exploration. Technical Report CMU-CyLab-08-009, Cylab, Carnegie Mellon University, June 2008.
• 11: Juan Caballero , Heng Yin , Zhenkai Liang , Dawn Song, Polyglot: automatic extraction of protocol message format using dynamic binary analysis, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA [doi>10.1145/1315245.1315286]
• 12: C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Model Checking Software, 12th SPIN Workshop, Aug. 2005.
• 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: Manuel Costa , Miguel Castro , Lidong Zhou , Lintao Zhang , Marcus Peinado, Bouncer: securing software by blocking bad input, Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, October 14-17, 2007, Stevenson, Washington, USA
• 15: Manuel Costa , Jon Crowcroft , Miguel Castro , Antony Rowstron , Lidong Zhou , Lintao Zhang , Paul Barham, Vigilante: end-to-end containment of internet worms, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom
• 16: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 17: Jedidiah R. Crandall , S. Felix Wu , Frederic T. Chong, Minos: Architectural support for protecting control data, ACM Transactions on Architecture and Code Optimization (TACO), v.3 n.4, p.359-389, December 2006 [doi>10.1145/1187976.1187977]
• 18: Weidong Cui , Marcus Peinado , Helen J. Wang , Michael E. Locasto, ShieldGen: Automatic Data Patch Generation for Unknown Vulnerabilities with Informed Probing, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.252-266, May 20-23, 2007 [doi>10.1109/SP.2007.34]
• 19: Nurit Dor , Michael Rodeh , Mooly Sagiv, CSSV: towards a realistic tool for statically detecting all buffer overflows in C, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 20: Vinod Ganapathy , Somesh Jha , David Chandler , David Melski , David Vitek, Buffer overrun detection using linear programming and static analysis, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948155]
• 21: V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Computer Aided Verification, July 2007.
• 22: ghttpd. http://gaztek.sf.net/ghttpd/.
• 23: 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
• 24: Patrice Godefroid , Adam Kiezun , Michael Y. Levin, Grammar-based whitebox fuzzing, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 25: 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
• 26: P. Godefroid, M. Y. Levin, and D. Molnar. Automated whitebox fuzz testing. In Network and Distributed System Security, Feb. 2008.
• 27: Sumit Gulwani , George C. Necula, Discovering affine equalities using random interpretation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.74-84, January 15-17, 2003, New Orleans, Louisiana, USA
• 28: IDA Pro. http://www.hex-rays.com/idapro/.
• 29: S. C. Johnson. Yacc: Yet another compiler-compiler. Technical Report (Computer Science) No. 32, Bell Laboratories, July 1975.
• 30: M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133--151, 1976.
• 31: Z. Lin, X. Jiang, D. Xu, and X. Zhang. Automatic protocol format reverse engineering through context-aware monitored execution. In Network and Distributed System Security, Feb. 2008.
• 32: Francesco Logozzo , Manuel Fähndrich, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil [doi>10.1145/1363686.1363736]
• 33: Rupak Majumdar , Ru-Gang Xu, Directed test generation using symbolic grammars, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321653]
• 34: Microsoft Corporation. Microsoft security bulletin MS07-046: Vulnerability in GDI could allow remote code execution, Aug. 2007.
• 35: Microsoft Corporation. SQL Server Resolution Protocol Specification, Jan. 2009. Revision 0.6.1.
• 36: Antoine Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, v.19 n.1, p.31-100, March 2006 [doi>10.1007/s10990-006-8609-1]
• 37: David Moore , Vern Paxson , Stefan Savage , Colleen Shannon , Stuart Staniford , Nicholas Weaver, Inside the Slammer Worm, IEEE Security and Privacy, v.1 n.4, p.33-39, July 2003 [doi>10.1109/MSECP.2003.1219056]
• 38: Markus Müller-Olm , Helmut Seidl, Analysis of modular arithmetic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.29-es, August 2007 [doi>10.1145/1275497.1275504]
• 39: J. Newsome and D. Song. Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software. In Network and Distributed System Security, Feb. 2005.
• 40: Prateek Saxena , R Sekar , Varun Puranik, Efficient fine-grained binary instrumentationwith applications to taint-tracking, Proceedings of the sixth annual IEEE/ACM international symposium on Code generation and optimization, April 05-09, 2008, Boston, MA, USA [doi>10.1145/1356058.1356069]
• 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: Dawn Song , David Brumley , Heng Yin , Juan Caballero , Ivan Jager , Min Gyung Kang , Zhenkai Liang , James Newsome , Pongsin Poosankam , Prateek Saxena, BitBlaze: A New Approach to Computer Security via Binary Analysis, Proceedings of the 4th International Conference on Information Systems Security, December 16-20, 2008, Hyderabad, India [doi>10.1007/978-3-540-89862-7_1]
• 43: Wireshark. http://www.wireshark.org.
• 44: G. Wondracek, P. M. Comparetti, C. Kruegel, and E. Kirda. Automatic network protocol analysis. In Network and Distributed System Security, Feb. 2008.
• 45: Yichen Xie , Andy Chou , Dawson Engler, ARCHER: using symbolic, path-sensitive analysis to detect memory access errors, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 46: 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]
• 47: 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.4 OPERATING SYSTEMS
      D.4.6 Security and Protection

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

General Terms:
Reliability, Security, Verification

Keywords:
loop summaries, vulnerability discovery and diagnosis