Static error detection using semantic inconsistency inference

ABSTRACT

Inconsistency checking is a method for detecting software errors that relies only on examining multiple uses of a value. We propose that inconsistency inference is best understood as a variant of the older and better understood problem of type inference. Using this insight, we describe a precise and formal framework for discovering inconsistency errors. Unlike previous approaches to the problem, our technique for finding inconsistency errors is purely semantic and can deal with complex aliasing and path-sensitive conditions. We have built a nullde reference analysis of C programs based on semantic inconsistency inference and have used it to find hundreds of previously unknown null dereference errors in widely used C programs.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 3: D. Beyer, T. Henzinger, R. Jhala, and R. Majumdar. Checking memory safety with Blast. In Proc. of the Conf. on Fundamental Approaches to Software Engineering, pages 2--18, 2005.
• 4: Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
• 5: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 6: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
• 7: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 8: 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
• 9: 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
• 10: 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
• 11: Brian Hackett , Alex Aiken, How is aliasing used in systems software?, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181785]
• 12: David Hovemeyer , William Pugh, Finding bugs is easy, ACM SIGPLAN Notices, v.39 n.12, December 2004 [doi>10.1145/1052883.1052895]
• 13: David Hovemeyer , Jaime Spacco , William Pugh, Evaluating and tuning a static analysis to find null pointer bugs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 14: R. Jhala and K. McMillan. Interpolant-based transition relation approximation. In Proc. of the International Conf. on Computer Aided Verification, pages 39--51, 2005.
• 15: M. Naik and J. Palsberg. A type system equivalent to a model checker. In Proc. of the European Symp. on Prog., pages 374--388, 2005.
• 16: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 17: François Pessaux , Xavier Leroy, Type-based analysis of uncaught exceptions, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.276-290, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292565]
• 18: Kwangkeun Yi , Sukyoung Ryu, Towards a Cost-Effective Estimation of Uncaught Exceptions in SML Programs, Proceedings of the 4th International Symposium on Static Analysis, p.98-113, September 08-10, 1997

INDEX TERMS

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

General Terms:
Experimentation, Languages, Reliability, Verification

Keywords:
error detection, inconsistency, satisfiability, static analysis