Large-scale analysis of format string vulnerabilities in Debian Linux

ABSTRACT

Format-string bugs are a relatively common security vulnerability, and can lead to arbitrary code execution. In collaboration with others, we designed and implemented a system to eliminate format string vulnerabilities from an entire Linux distribution, using type-qualifier inference, a static analysis technique that can find taint violations.

We successfully analyze 66% of C/C++ source packages in the Debian 3.1 Linux distribution. Our system finds 1,533 format string taint warnings. We estimate that 85% of these are true positives, i.e., real bugs; ignoring duplicates from libraries, about 75% are real bugs.

We suggest that the technology exists to render format string vulnerabilities extinct in the near future.

REFERENCES

• 1: Build-Interceptor. Website, 2007. http://freshmeat.net/projects/build-interceptor/.
• 2: Elsa. Website, 2007. http://www.cs.berkeley.edu/¢ smcpeak/elkhound/sources/elsa/.
• 3: Oink. Website, 2007. http://freshmeat.net/projects/oink/.
• 4: Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 5: David P. Anderson, BOINC: A System for Public-Resource Computing and Storage, Proceedings of the Fifth IEEE/ACM International Workshop on Grid Computing, p.4-10, November 08-08, 2004 [doi>10.1109/GRID.2004.14]
• 6: Dzintars Avots , Michael Dalton , V. Benjamin Livshits , Monica S. Lam, Improving software security with a C pointer analysis, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062520]
• 7: Pete Broadwell , Matt Harren , Naveen Sastry, Scrash: a system for generating secure crash information, Proceedings of the 12th conference on USENIX Security Symposium, p.19-19, August 04-08, 2003, Washington, DC
• 8: 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]
• 9: Hao Chen, Drew Dean, and David Wagner. Model checking one million lines of c code. In Proc. of the 11th Annual Network and Distributed System Security Symposium (NDSS), 2004.
• 10: Crispin Cowan , Matt Barringer , Steve Beattie , Greg Kroah-Hartman , Mike Frantzen , Jamie Lokier, FormatGuard: automatic protection from printf format string vulnerabilities, Proceedings of the 10th conference on USENIX Security Symposium, p.15-15, August 13-17, 2001, Washington, D.C.
• 11: Alan DeKok. PScan: A limited problem scanner for C. Website, 2000. http://packages.debian.org/pscan.
• 12: Jeff Dike, User-mode Linux, Proceedings of the 5th annual conference on Linux Showcase & Conference, p.2-2, November 05-10, 2001, Oakland, California
• 13: David Evans , David Larochelle, Improving Security Using Extensible Lightweight Static Analysis, IEEE Software, v.19 n.1, p.42-51, January 2002 [doi>10.1109/52.976940]
• 14: Jeffrey Scott Foster , Alexander S. Aiken, Type qualifiers: lightweight specifications to improve software quality, University of California, Berkeley, 2002
• 15: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 16: Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006 [doi>10.1145/1186632.1186635]
• 17: 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
• 18: David Gay , Alex Aiken, Memory management with explicit regions, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.313-323, June 17-19, 1998, Montreal, Quebec, Canada
• 19: David Greenfieldboyce and Jeffrey S. Foster. Type qualifiers for Java. Technical report, University of Maryland, August 2007. http://www.cs.umd.edu/projects/PL/jqual/.
• 20: Samuel Guyer, Emery Berger, and Calvin Lin. Detecting errors with configurable whole-program dataflow analysis. Technical report, University of Texas at Austin, 2002. ftp://ftp.cs.utexas.edu/pub/emery/papers/detecting-errors.pdf.
• 21: 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
• 22: Rob Johnson , David Wagner, Finding user/kernel pointer bugs with type inference, Proceedings of the 13th conference on USENIX Security Symposium, p.9-9, August 09-13, 2004, San Diego, CA
• 23: Robert T. Johnson. Verifying Security Properties using Type-Qualifier Inference. PhD thesis, EECS Department, University of California, Berkeley, 2007.
• 24: Nenad Jovanovic , Christopher Kruegel , Engin Kirda, Pixy: A Static Analysis Tool for Detecting Web Application Vulnerabilities (Short Paper), Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P'06), p.258-263, May 21-24, 2006 [doi>10.1109/SP.2006.29]
• 25: Benjamin Robert Liblit , Alexander Aiken, Cooperative bug isolation, University of California at Berkeley, Berkeley, CA, 2004
• 26: V. Benjamin Livshits , Monica S. Lam, Finding security vulnerabilities in java applications with static analysis, Proceedings of the 14th conference on USENIX Security Symposium, p.18-18, July 31-August 05, 2005, Baltimore, MD
• 27: Scott McPeak and George C. Necula. Elkhound: A fast, practical GLR parser generator. In Proc. of the 13th International Conference on Compiler Constructor (CC), 2004.
• 28: A. Nguyen-Tuong, S. Guarnieri, D. Greene, J. Shirley, and D. Evans. Automatically hardening web applications using precise tainting. In 20th IFIP International Information Security Conference, 2005.
• 29: Michael F. Ringenburg , Dan Grossman, Preventing format-string attacks via automatic and efficient dynamic checking, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA [doi>10.1145/1102120.1102166]
• 30: Tim Robbins. Libformat, 2000. http://archives.neohapsis.com/archives/linux/lsap/2000-q3/0444.html.
• 31: Umesh Shankar , Kunal Talwar , Jeffrey S. Foster , David Wagner, Detecting format string vulnerabilities with type qaualifiers, Proceedings of the 10th conference on USENIX Security Symposium, p.16-16, August 13-17, 2001, Washington, D.C.
• 32: Saurabh Srivastava , Michael Hicks , Jeffrey S. Foster, Modular information hiding and type-safe linking for C, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190319]
• 33: Timothy Tsai and Navjot Singh. Libsafe 2.0: Detection of format string vulnerability exploits. Technical report, Avaya Labs, February 2001. http://pubs.research.avayalabs.com/pdfs/ALR-2001-018-whpaper.pdf.
• 34: John Viega, J. T. Bloch, Tadayoshi Kohno, and Gary McGraw. ITS4: A static vulnerability scanner for C and C++ code. ACM Transactions on Information and System Security, 5(2), 2002.
• 35: Common Vulnerabilities and Exposures. Format string vulnerabilities. Website, 2007. http://www.cve.mitre.org/cgi-bin/cvekey.cgi?keyword=format+string.
• 36: David Wagner, Jeffrey S. Foster, Eric A. Brewer, and Alexander Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proc. of the 7th Network and Distributed System Security Symposium (NDSS), 2000.
• 37: Yichen Xie , Alex Aiken, Static detection of security vulnerabilities in scripting languages, Proceedings of the 15th conference on USENIX Security Symposium, p.13-13, July 31-August 04, 2006, Vancouver, B.C., Canada
• 38: Junfeng Yang , Ted Kremenek , Yichen Xie , Dawson Engler, MECA: an extensible, expressive system and language for statically checking security properties, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948153]
• 39: 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
          Subjects: Invasive software (e.g., viruses, worms, Trojan horses)

General Terms:
Languages, Security

Keywords:
format string vulnerability, large-scale analysis, type-qualifier inference