Program analysis for bug detection using parfait: invited talk

ABSTRACT

The goal of the Parfait project is to find bugs in C source code in a scalable and precise way. To this end, Parfait was designed as a framework with layers of sound program analyses, multiple layers per bug type, to identify bugs in a program more quickly and accurately.

Parfait also aims to identify security bugs, i.e., bugs that may be exploited by a malicious user. To this end, an optional pre-processing step is available to reduce the scope of potential bugs of interest.

To evaluate Parfait's precision and recall, we have developed BegBunch, a bug benchmarking suite that contains existing synthetic benchmarks and samples of bugs ("bug kernels") taken from open source code.

REFERENCES

• 1: Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers. Addison-Wesley, 1986.
• 2: T. E. Cheatham , G. H. Holloway , J. A. Townley, Symbolic Evaluation and the Analysis of Programs, IEEE Transactions on Software Engineering, v.5 n.4, p.402-417, July 1979 [doi>10.1109/TSE.1979.234207]
• 3: Cristina Cifuentes , Bernhard Scholz, Parfait: designing a scalable bug checker, Proceedings of the 2008 workshop on Static analysis, p.4-11, June 12-12, 2008, Tucson, Arizona [doi>10.1145/1394504.1394505]
• 4: Cristina Cifuentes, Bernhard Scholz, Michael Mounteney, Erica Mealy, Nathan Keynes, and Lian Li. BegBunch: A benchmarker for C-source bug detection tools. Submitted for publication, January 2009.
• 5: Yoshihiko Futamura. Partial evaluation of computation process -- an approach to a compiler-compiler. Systems, Computers, Controls, 2: 45--50, 1971.
• 6: S.C. Johnson. Lint, a C program checker. Technical Report 65, Bell Laboratories, 1978.
• 7: Kendra Kratkiewicz and Richard Lippmann. Using a diagnostic corpus of C programs to evaluate buffer overflow detection by static analysis tools. In Proc. of Workshop on the Evaluation of Software Defect Detection Tools, June 2005.
• 8: Chris Lattner , Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.75, March 20-24, 2004, Palo Alto, California
• 9: Shan Lu, Zhenmin Li, Feng Qin, Lin Tan, Pin Zhou, and Yuanyuan Zhou. BugBench: A benchmark for evaluating bug detection tools. In Proc. of Workshop on the Evaluation of Software Defect Detection Tools, June 2005.
• 10: NIST. National Institute of Standards and Technology SAMATE Reference Dataset (SRD) project. http://samate.nist.gov/SRD, January 2006.
• 11: Bernhard Scholz, Chenyi Zhang, and Cristina Cifuentes. User-input dependence analysis via graph reachability. In Proceedings of the Eighth IEEE Working Conference on Source Code Analysis and Manipulation, pages 25--34, 28-29 September 2008.
• 12: ISO C 99 Standard -- TC2. ISO/IEC Working Group 14, 9899:TC2 edition, May 2005.
• 13: Misha Zitser , Richard Lippmann , Tim Leek, Testing static analysis tools using exploitable buffer overflows from open source code, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.8 Metrics

General Terms:
Algorithms

Keywords:
constant propagation, partial evaluation, symbolic analysis