Sound, complete and scalable path-sensitive analysis

ABSTRACT

We present a new, precise technique for fully path- and context-sensitive program analysis. Our technique exploits two observations: First, using quantified, recursive formulas, path- and context-sensitive conditions for many program properties can be expressed exactly. To compute a closed form solution to such recursive constraints, we differentiate between observable and unobservable variables, the latter of which are existentially quantified in our approach. Using the insight that unobservable variables can be eliminated outside a certain scope, our technique computes satisfiability- and validity-preserving closed-form solutions to the original recursive constraints. We prove the solution is as precise as the original system for answering may and must queries as well as being small in practice, allowing our technique to scale to the entire Linux kernel, a program with over 6 million lines of code.

REFERENCES

• 1: Alex Aiken , Suhabe Bugrara , Isil Dillig , Thomas Dillig , Brian Hackett , Peter Hawkins, An overview of the saturn project, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.43-48, June 13-14, 2007, San Diego, California, USA [doi>10.1145/1251535.1251543]
• 2: Alexander Aiken , Edward L. Wimmers , Jens Palsberg, Optimal Representations of Polymorphic Types with Subtyping, Higher-Order and Symbolic Computation, v.12 n.3, p.237-282, October 1999 [doi>10.1023/A:1010056315933]
• 3: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 4: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 5: Thomas Ball , Sriram K. Rajamani, Bebop: a path-sensitive interprocedural dataflow engine, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.97-103, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379690]
• 6: R. Bloem, I. Moon, K. Ravi, and F. Somenzi. Approximations for fixpoint computations in symbolic model checking.
• 7: George Boole, An Investigation of the Laws of Thought, Dover Publications, Incorporated, 1958
• 8: Suhabe Bugrara , Alex Aiken, Verifying the Safety of User Pointer Dereferences, Proceedings of the 2008 IEEE Symposium on Security and Privacy (sp 2008), p.325-338, May 18-21, 2008 [doi>10.1109/SP.2008.15]
• 9: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 10: David L. Dill , Howard Wong-Toi, Verification of Real-Time Systems by Successive Over and Under Approximation, Proceedings of the 7th International Conference on Computer Aided Verification, p.409-422, July 03-05, 1995
• 11: 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
• 12: Isil Dillig , Thomas Dillig , Alex Aiken, Static error detection using semantic inconsistency inference, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 13: Javier Esparza , Stefan Schwoon, A BDD-Based Model Checker for Recursive Programs, Proceedings of the 13th International Conference on Computer Aided Verification, p.324-336, July 18-22, 2001
• 14: 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]
• 15: Fritz Henglein, Type inference and semi-unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.184-197, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62701]
• 16: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 17: F. Ivancic, Z. Yang, M.K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-soft:software verification platform. Lecture Notes in Computer Science, 3576/2005:301--306, 2005.
• 18: F. Lin. On strongest necessary and weakest sufficient conditions. In Proc. International Conference on Principles of Knowledge Representation and Reasoning, pages 143--159, April 2000.
• 19: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• 20: 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]
• 21: David A. Schmidt, A calculus of logical relations for over- and underapproximating static analyses, Science of Computer Programming, v.64 n.1, p.29-53, January, 2007 [doi>10.1016/j.scico.2006.03.008]
• 22: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. Program Flow Analysis: Theory and Applications, pages 189--234, 1981.
• 23: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, ACM SIGPLAN Notices, v.40 n.1, p.351-363, January 2005

INDEX TERMS

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

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

General Terms:
Experimentation, Languages, Reliability, Verification

Keywords:
path- and context-sensitive analysis, static analysis, strongest necessary/weakest sufficient conditons