Cristina Cifuentes
ABSTRACT
We present the design of Parfait, a static layered program analysis framework for bug checking, designed for scalability and precision by improving false positive rates and scale to millions of lines of code. The Parfait framework is inherently parallelizable and makes use of demand driven analyses.
In this paper we provide an example of several layers of analyses for buffer overflow, summarize our initial implementation for C, and provide preliminary results. Results are quantified in terms of correctly-reported, false positive and false negative rates against the NIST SAMATE synthetic benchmarks for C code.
- C. Artho and A. Biere. Applying static analysis to large-scale, multi-threaded Java programs. In Proceedings of the Australian Software Engineering Conference (ASWEC), pages 68--75, Canberra, ACT, Australia, August 2001. IEEE Press. Google Scholar
Digital Library
- C. Artho and K. Havelund. Applying Jlint to space exploration software. In Verification, Model Checking, and Abstract Interpretation, volume 2937/2003 of Lecture Notes in Computer Science, pages 297--308. Springer Berling / Heidelberg, 2004.Google Scholar
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings of the Workshop on Model Checking of Software (SPIN), LNCS 2057, pages 103--122, May 2001. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proceedings of the Principles of Programming Languages (POPL), pages 1--3. ACM Press, January 2002. Google ScholarDigital Library
- W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software---Practice & Experience, 30:775--802, 2000. Google ScholarDigital Library
- CWE list (draft 5). http://cwe.mitre.org/data/index.html, December 2006.Google Scholar
- M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI), pages 57--68, Berlin, Germany, June 2002. ACM Press. Google ScholarDigital Library
- D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report SRC-RR-159, COMPAQ Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, December 1998.Google Scholar
- A. Deutsch. Static verification of dynamic properties. PolySpace White Paper, February 2004.Google Scholar
- D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operating Systems Design and Implementation, pages 23--25, San Diego, CA, Oct. 2000. USENIX. Google ScholarDigital Library
- D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as deviant behavior: A general approach to inferring errors in systems code. In Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles, pages 57--72, Alberta, Canada, Oct. 2001. ACM Press. Google ScholarDigital Library
- D. Evans and D. Larochelle. Improving security using extensible lightweight static analysis. IEEE Software, pages 42--51, January/February 2002. Google ScholarDigital Library
- A. Fehnker, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Goanna---a static model checker. In L. Brim, B. Haverkort, M. Leucker, and J. Pol, editors, Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems, number 4346 in Lecture Notes in Computer Science, Bonn, Germany, Aug. 2006. Google ScholarDigital Library
- Fortify Static Code Analysis (SCA). http://www.fortify.com/products/sca/. Last accessed: 1 April 2008.Google Scholar
- GrammaTech CodeSonar. http://www.grammatech. com/products/codesonar/overview.html. Last accessed: 1 April 2008.Google Scholar
- K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer, 2(4), April 1999.Google Scholar
- D. Hovemeyer and W. Pugh. Finding bugs is easy. In Companion to the 19th annual ACM SIGPLAN Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), pages 92--106, Vancouver, BC, Canada, Oct. 2004. ACM Press. Google ScholarDigital Library
- R. Jhala. Lazy Abstraction. PhD thesis, University of California, Berkeley, Fall 2004.Google Scholar
- S. Johnson. Lint, a C program checker. Unix Programmer's Manual, AT&T Bell Laboratories, 1978.Google Scholar
- K. Kratkiewicz and R. 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.Google Scholar
- C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04), Palo Alto, California, March 2004. Google ScholarDigital Library
- W. Le and M. L. Soffa. Refining buffer overflow detection via demand-driven path-sensitive analysis. In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pages 63--68, San Diego, CA, June 2007. Google ScholarDigital Library
- S. Lu, Z. Li, F. Qin, L. Tan, P. Zhou, and Y. Zhou. BugBench: A benchmark for evaluating bug detection tools. In Proc. of Workshop on the Evaluation of Software Defect Detection Tools, June 2005.Google Scholar
- S. McPeak. Elsa/Oink/Cqual+. Talk at CodeCon, February 2006.Google Scholar
- NIST SAMATE -- software assurance metrics and tool evaluation. http://samate.nist.gov. Last accessed: January 2007.Google Scholar
- J. Pincus. Steering the pyramids: Tools, technology, and process in engineering at microsoft. Keynote at the International Conference on Software Maintenance (ICSM). Slides at http://research.microsoft.com/users/jpincus/icsm.ppt, 2002.Google Scholar
- B. Scholz, C. Zhang, and C. Cifuentes. User-input dependence analysis via graph reachability. Technical Report SMLI TR-2008-117, Sun Microsystems Laboratories, 16 Network Circle, Menlo Park, CA 94025, March 2008. Google ScholarDigital Library
- R. C. Seacord. Secure Coding in C and C++. SEI Series, A CERT Book. Addison-Wesley, Sept. 2005. Google ScholarDigital Library
- K. Tsipenyuk, B. Chess, and G. McGraw. Seven pernicious kingdoms: A taxonomy of software security errors. IEEE Security & Privacy, 3(6):81--84, November/December 2005. Google ScholarDigital Library
- Veracode website. http://www.veracode.com/. Last accessed: January 2007.Google Scholar
- M. Webster. Leveraging static analysis for a multidimensional view of software quality and security: Klocwork's solution. White paper, IDC, Framingham, MA, Sept. 2005.Google Scholar
- Y. Xie, A. Chou, and D. Engler. Archer: using symbolic, path-sensitive analysis to detect memory access errors. In ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, pages 327--336, New York, NY, USA, 2003. ACM Press. Google ScholarDigital Library
- M. Zitser, R. Lippmann, and T. Leek. Testing static analysis tools using exploitable buffer overflows from open source code. In SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering, pages 97--106, New York, NY, USA, 2004. ACM Press. Google ScholarDigital Library
Index Terms
- Parfait: designing a scalable bug checker
Recommendations
Program analysis for bug detection using parfait: invited talk
PEPM '09: Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulationThe 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 ...
WYSINWYX: What you see is not what you eXecute
Over the last seven years, we have developed static-analysis methods to recover a good approximation to the variables and dynamically allocated memory objects of a stripped executable, and to track the flow of values through them. The article presents ...
Scalable and systematic detection of buggy inconsistencies in source code
OOPSLA '10Software developers often duplicate source code to replicate functionality. This practice can hinder the maintenance of a software project: bugs may arise when two identical code segments are edited inconsistently. This paper presents DejaVu, a highly ...
Comments