Static detection of leaks in polymorphic containers

ABSTRACT

This paper presents the first practical static analysis tool that can find memory leaks and double deletions of objects held in polymorphic containers. This is especially important since most dynamically allocated objects are stored in containers.The tool is based on the concept of object ownership: every object has one and only one owning pointer. The owning pointer holds the exclusive right and obligation to either delete the object or to transfer the obligation. This paper presents a new type system that allows different instances of a polymorphic container to hold different types of elements, and to independently own or not own their elements.Our tool is sound: it will report all potential memory leaks and multiple deletions of pointers in a program. Our system automatically identifies the container implementation routines in an application. The user provides a short specification on the container structure and ownership constraints for these routines. The system then solves for the ownership constraints flow- and context-sensitively, and reports inconsistencies in ownership constraints as potential memory leaks and double deletions.We applied our tool to a suite of five large open-source and commercial C and C++ applications totaling one million lines of code. The tool successfully identified memory leaks in these programs and found double deletions of objects that could lead to program failures or security vulnerabilities.

REFERENCES

• 1: Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 2: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 3: John Boyland, Alias burying: unique variables without destructive reads, Software—Practice & Experience, v.31 n.6, p.533-553, May 2001 [doi>10.1002/spe.370]
• 4: 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]
• 5: D. Clarke. An object calculus with ownership and containment. In FOOL 2001, January 2001.
• 6: Dave Clarke , Sophia Drossopoulou, Ownership, encapsulation and the disjointness of type and effect, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 7: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 8: M. Corporation. CAN-2004-0416. Common Vulnerabilities and Exposures (CVE) (cve.mitre.org), 2004.
• 9: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 10: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Checking Cleanness in Linked Lists, Proceedings of the 7th International Symposium on Static Analysis, p.115-134, June 29-July 01, 2000
• 11: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 12: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.253-263, June 18-21, 2000, Vancouver, British Columbia, Canada
• 14: 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
• 15: David Gay , Alex Aiken, Language support for regions, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.70-80, June 2001, Snowbird, Utah, United States
• 16: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 17: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, ACM SIGPLAN Notices, v.40 n.1, p.310-323, January 2005
• 19: 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
• 20: David L. Heine , Monica S. Lam, Static memory leak detection, Stanford University, Stanford, CA, 2005
• 21: David L. Heine , Monica S. Lam, A practical flow-sensitive and context-sensitive C and C++ memory leak detector, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 22: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 23: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, The undecidability of the semi-unification problem, Information and Computation, v.102 n.1, p.83-101, Jan. 1993 [doi>10.1006/inco.1993.1003]
• 24: N. Nethercote and J. Seward. Valgrind: A program supervision framework. In Third Workshop on Runtime Verification (RV'03), July 2003.
• 25: James Noble , Jan Vitek , John Potter, Flexible Alias Protection, Proceedings of the 12th European Conference on Object-Oriented Programming, p.158-185, July 20-24, 1998
• 26: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 27: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 28: SUIF Group. The SUIF2 compiler system. http://suif.stanford.edu/suif/suif2/+.
• 29: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 30: P. Wadler. Linear types can change the world. In IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561--581, April 1990.
• 31: David Walker , J. Gregory Morrisett, Alias Types for Recursive Data Structures, Selected papers from the Third International Workshop on Types in Compilation, p.177-206, September 21, 2000
• 32: D. A. Wheeler. More than a gigabuck: Estimating gnu/linux's size, June 2001. http://www.dwheeler.com/sloc+.
• 33: Yichen Xie , Alex Aiken, Context- and path-sensitive memory leak detection, 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

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.3 Coding Tools and Techniques

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

General Terms:
Algorithms, Experimentation, Languages, Verification

Keywords:
error detection, memory leaks, memory management, program analysis, type systems