Null dereference verification via over-approximated weakest pre-conditions analysis

Abstract

Null dereferences are a bane of programming in languages such as Java. In this paper we propose a sound, demand-driven, inter-procedurally context-sensitive dataflow analysis technique to verify a given dereference as safe or potentially unsafe. Our analysis uses an abstract lattice of formulas to find a pre-condition at the entry of the program such that a null-dereference can occur only if the initial state of the program satisfies this pre-condition. We use a simplified domain of formulas, abstracting out integer arithmetic, as well as unbounded access paths due to recursive data structures. For the sake of precision we model aliasing relationships explicitly in our abstract lattice, enable strong updates, and use a limited notion of path sensitivity. For the sake of scalability we prune formulas continually as they get propagated, reducing to true conjuncts that are less likely to be useful in validating or invalidating the formula. We have implemented our approach, and present an evaluation of it on a set of ten real Java programs. Our results show that the set of design features we have incorporated enable the analysis to (a) explore long, inter-procedural paths to verify each dereference, with (b) reasonable accuracy, and (c) very quick response time per dereference, making it suitable for use in desktop development environments.

References

1. T. Ball and S. Rajamani. Automatically validating temporal safety properties of interfaces. In Model Checking Software, volume 2057 of Lecture Notes in Computer Science, pages 102--122. Springer Berlin / Heidelberg, 2001.
2. M. Barnett, K. R. M. Leino, and W. Schulte. The spec# programming system: An overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, volume 3362 of Lecture Notes in Computer Science, pages 49--69. Springer Berlin / Heidelberg, 2005.
3. S. Chandra, S. J. Fink, and M. Sridharan. Snugglebug: a powerful approach to weakest preconditions. In PLDI '09: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 363--374, New York, NY, USA, 2009. ACM.
4. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '77, pages 238--252, New York, NY, USA, 1977. ACM.
5. E. W. Dijkstra. A Discipline of Programming. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1997.
6. I. Dillig, T. Dillig, and A. Aiken. Sound, complete and scalable path-sensitive analysis. In PLDI '08: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pages 270--280, 2008.
7. I. Dillig, T. Dillig, and A. Aiken. Fluid updates: Beyond strong vs. weak updates. In A. Gordon, editor, Programming Languages and Systems, volume 6012 of Lecture Notes in Computer Science, pages 246--266. Springer Berlin / Heidelberg, 2010.
8. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for java. In PLDI '02: Proc. SIGPLAN Conference on Programming Language Design and Implementation, pages 234--245, 2002.
9. P. Godefroid, N. Klarlund, and K. Sen. Dart: directed automated random testing. In PLDI 05: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 213--223, 2005.
10. B. Gulavani, T. Henzinger, Y. Kannan, A. Nori, and S. Rajamani. Synergy: An new algorithm for property checking. In FSE '06: Proc. ACM SIGSOFT Symp. on Foundations of Software Engineering, pages 117--127, 2006.
11. D. Hovemeyer, J. Spacco, and W. Pugh. Evaluating and tuning a static analysis to null pointer bugs. In PASTE '05: Proc. ACM SIGPLAN-SIGSOFT workshop on Program Analysis for Software Tools and Engineering, pages 13--19, 2005.
12. G. Kildall. A unified approach to global program optimization. In POPL '73: Proc. ACM Symposium on Principles of Programming Languages, pages 194--206, New York, NY, USA, 1973.
13. A. Loginov, E. Yahav, S. Chandra, S. Fink, N. Rinetzky, and M. Nanda. Verifying dereference safety via expanding-scope analysis. In ISSTA '08: Proc. International Symposium on Software Testing and Analysis, pages 213--224, New York, NY, USA, 2008. ACM.
14. M. G. Nanda, S. Mani, V. S. Sinha, and S. Sinha. Demystifying model transformations: an approach based on automated rule inference. In OOPSLA '09: Proc. ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, pages 341--360, 2009.
15. M. G. Nanda and S. Sinha. Accurate interprocedural null-dereference analysis for java. In ICSE '09: Proc. International Conference on Software Engineering, pages 133--143, Washington, DC, USA, 2009. IEEE Computer Society.
16. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. Logic in Computer Science, Symposium on, pages 55--74, 2002.
17. M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24:217--298, May 2002.
18. M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Application. Prentice Hall Professional Technical Reference, 1981.
19. F. Spoto. Precise null-pointer analysis. Software and Systems Modeling, 10:219--252, 2011. 10.1007/s10270-009-0132--5.
20. W. Visser, C. S. Pasareanu, and S. Khurshid. Test input generation with java pathfinder. In ISSTA '04: Proc. ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 97--107, 2004.
21. T.J. Watson Libraries for Analysis (WALA), http://wala.sf.net.

Index Terms

• Hardware

  • Hardware validation

    • Functional verification

      • Assertion checking

• Software and its engineering

  • Software creation and management

    • Software verification and validation

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Assertions

      • Program verification