Dual analysis for proving safety and finding bugs

ABSTRACT

Program bugs remain a major challenge for software developers and various tools have been proposed to help with their localization and elimination. Most present-day tools are based either on over-approximating techniques that can prove safety but may report false positives, or on under-approximating techniques that can find real bugs but with possible false negatives. In this paper, we propose a dual static analysis that is based on only over-approximation. Its main novelty is to concurrently derive conditions that lead to either success or failure outcomes and thus we provide a comprehensive solution for both proving safety and finding real program bugs. We have proven the soundness of our approach and have implemented a prototype system that is validated by a set of experiments.

References

1. T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN Workshop, pages 103--122, 2001.
2. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI, 2003.
3. P. Cousot and R. Cousot. Modular static program analysis. In CC, 2002.
4. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In ACM POPL, pages 84--96, 1978.
5. J. J. Dongarra, P. Luszczek, and A. Petitet. The LINPACK benchmark: Past, present, and future. Concurrency and Computation: Practice and Experience, 15:1--18, 2003.
6. P. Godefroid. Model checking for programming languages using VeriSoft. In ACM POPL, 1997.
7. P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI, 2005.
8. B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. SYNERGY: A new algorithm for property checking. In ACM FSE, 2006.
9. S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint solving. In ACM PLDI, pages 281--292, 2008.
10. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In ACM POPL, 2002.
11. K. Ku, T. E. Hart, M. Chechik, and D. Lie. A buffer overflow benchmark for software model checkers. In ASE, 2007.
12. K. Marriott and H. Søndergaard. Bottom-up dataflow analysis of normal logic programs. J. Log. Program., 13(2&3), 1992.
13. G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In CC, 2002.
14. National Institute of Standards and Technology. Java SciMark benchmark for scientific computing. http://math.nist.gov/scimark2/.
15. C. S. Pasareanu, R. Pelánek, and W. Visser. Concrete model checking with abstract matching and refinement. In CAV, pages 52--66, 2005.
16. C. Popeea and W. N. Chin. Inferring disjunctive postconditions. In ASIAN CS Conference, 2006.
17. C. Popeea, D. N. Xu, and W. N. Chin. A practical and precise inference and specializer for array bound checks elimination. In ACM SIGPLAN PEPM, 2008.
18. W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102--114, 1992.
19. X. Rival. Understanding the origin of alarms in ASTRÉE. In SAS, 2005.
20. S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In SAS, 2006.
21. N. Suzuki and K. Ishihata. Implementation of an array bound checker. In ACM POPL, pages 132--143, 1977.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

      • Program verification

    • Program semantics