Testing for buffer overflows with length abstraction

ABSTRACT

We present Splat, a tool for automatically generating inputs that lead to memory safety violations in C programs. Splat performs directed random testing of the code, guided by symbolic execution. However, instead of representing the entire contents of an input buffer symbolically, Splat tracks only a prefix of the buffer symbolically, and a symbolic length that may exceed the size of the symbolic prefix. The part of the buffer beyond the symbolic prefix is filled with concrete random inputs. The use of symbolic buffer lengths makes it possible to compactly summarize the behavior of standard buffer manipulation functions, such as string library functions, leading to a more scalable search for possible memory errors. While reasoning only about prefixes of buffer contents makes the search theoretically incomplete, we experimentally demonstrate that the symbolic length abstraction is both scalable and sufficient to uncover many real buffer overflows in C programs. In experiments on a set of benchmarks developed independently to evaluate buffer overflow checkers, Splat was able to detect buffer overflows quickly, sometimes several orders of magnitude faster than when symbolically representing entire buffers. Splat was also able to find two previously unknown buffer overflows in a heavily-tested storage system.

REFERENCES

• 1: 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]
• 2: 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
• 3: James C. Foster , Vitaly Osipov , Nish Bhalla, Buffer Overflow Attacks, Syngress Publishing, 2005
• 4: V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV, 2007.
• 5: 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
• 6: 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
• 7: P. Godefroid, M. Y. Levin, and D. Molnar. Active property checking. Technical report, Microsoft, 2007.
• 8: P. Godefroid, M.Y. Levin, and D. Molnar. Automated whitebox fuzz testing. In NDSS, 2008.
• 9: Alex Groce , Gerard Holzmann , Rajeev Joshi, Randomized Differential Testing as a Prelude to Formal Verification, Proceedings of the 29th international conference on Software Engineering, p.621-631, May 20-26, 2007 [doi>10.1109/ICSE.2007.68]
• 10: R. Jones and P. Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. In Third International Workshop on Automated Debugging, 1997.
• 11: Pallavi Joshi , Koushik Sen , Mark Shlimovich, Predictive testing: amplifying the effectiveness of software testing, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287710]
• 12: Donald E. Knuth, The art of computer programming, volume 3: (2nd ed.) sorting and searching, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1998
• 13: 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
• 14: 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]
• 15: Nicholas Nethercote , Julian Seward, Valgrind: a framework for heavyweight dynamic binary instrumentation, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 16: O. Ruwase and M. Lam. A practical dynamic buffer overflow detector. In NDSS, 2004.
• 17: 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
• 18: Julian Seward , Nicholas Nethercote, Using Valgrind to detect undefined value errors with bit-precision, Proceedings of the annual conference on USENIX Annual Technical Conference, p.2-2, April 10-15, 2005, Anaheim, CA
• 19: Daniel Dominic Sleator , Robert Endre Tarjan, Self-adjusting binary search trees, Journal of the ACM (JACM), v.32 n.3, p.652-686, July 1985 [doi>10.1145/3828.3835]
• 20: Willem Visser , Corina S. Pǎsǎreanu , Radek Pelánek, Test input generation for java containers using state matching, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146243]
• 21: D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In NDSS, 2000.
• 22: 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
• 23: M. Zhivich, T. Leek, and R. Lippmann. Dynamic buffer overflow detection. In BUGS, 2005.
• 24: 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.5 Testing and Debugging

General Terms:
Reliability, Verification

Keywords:
buffer overflows, directed testing, length abstractions, testing c programs, underapproximation