Verifying dereference safety via expanding-scope analysis

ABSTRACT

This paper addresses the challenging problem of verifying the safety of pointer dereferences in real Java programs. We provide an automatic approach to this problem based on a sound interprocedural analysis. We present a staged expanding-scope algorithm for interprocedural abstract interpretation, which invokes sound analysis with partial programs of increasing scope. This algorithm achieves many benefits typical of whole-program interprocedural analysis, but scales to large programs by limiting analysis to small program fragments. To address cases where the static analysis of program fragments fails to prove safety, the analysis also suggests possible annotations which, if a user accepts, ensure the desired properties. Experimental evaluation on a number of Java programs shows that we are able to verify 90% of all dereferences soundly and automatically, and further reduce the number of remaining dereferences using non-nullness annotations.

REFERENCES

• 1: Barnett, M., Leino, K., and Shulte, W. The Spec# programming system: An overview. In CASSIS (2004).
• 2: 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]
• 3: Cok, D. R., and Kiniry, J. ESC/Java2: Uniting ESC/Java and JML. In CASSIS (2004).
• 4: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 5: Jeffrey Dean , David Grove , Craig Chambers, Optimization of Object-Oriented Programs Using Static Class Hierarchy Analysis, Proceedings of the 9th European Conference on Object-Oriented Programming, p.77-101, August 07-11, 1995
• 6: Amer Diwan , Kathryn S. McKinley , J. Eliot B. Moss, Type-based alias analysis, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.106-117, June 17-19, 1998, Montreal, Quebec, Canada
• 7: Nurit Dor , Michael Rodeh , Mooly Sagiv, Detecting memory errors via static pointer analysis (preliminary experience), Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.27-34, June 16-16, 1998, Montreal, Quebec, Canada
• 8: 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
• 9: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302467]
• 10: Manuel Fähndrich , K. Rustan M. Leino, Declaring and checking non-null types in an object-oriented language, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 11: Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146254]
• 12: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 13: 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
• 14: David Hovemeyer , William Pugh, Finding bugs is easy, ACM SIGPLAN Notices, v.39 n.12, December 2004 [doi>10.1145/1052883.1052895]
• 15: JSR 305: Annotations for software defect detection. http://jcp.org/en/jsr/detail?id=305.
• 16: Larus, J., Ball, T., Das, M., DeLine, R., Fahndrich, M., Pincus, J., Rajamani, S., and Venkatapathy, R. Righting software. IEEE Software (2004).
• 17: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 18: Atanas Rountev , Barbara G. Ryder , William Landi, Data-flow analysis of program fragments, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.235-252, September 06-10, 1999, Toulouse, France
• 19: 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]
• 20: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 21: Aaron Tomb , Guillaume Brat , Willem Visser, Variably interprocedural program analysis for runtime error detection, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273478]
• 22: Christopher Unkel , Monica S. Lam, Automatic inference of stationary fields: a generalization of java's final fields, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 23: WALA: The T. J. Watson Libraries for Analysis. http://wala.sourceforge.net.
• 24: Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007 [doi>10.1145/1232420.1232423]

INDEX TERMS

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

General Terms:
Algorithms, Reliability, Verification

Keywords:
abstract interpretation, specification inference, static analysis