Bugs as deviant behavior: a general approach to inferring errors in systems code

ABSTRACT

A major obstacle to finding program errors in a real system is knowing what correctness rules the system must obey. These rules are often undocumented or specified in an ad hoc manner. This paper demonstrates techniques that automatically extract such checking information from the source code itself, rather than the programmer, thereby avoiding the need for a priori knowledge of system rules.The cornerstone of our approach is inferring programmer "beliefs" that we then cross-check for contradictions. Beliefs are facts implied by code: a dereference of a pointer, p, implies a belief that p is non-null, a call to "unlock(1)" implies that 1 was locked, etc. For beliefs we know the programmer must hold, such as the pointer dereference above, we immediately flag contradictions as errors. For beliefs that the programmer may hold, we can assume these beliefs hold and use a statistical analysis to rank the resulting errors from most to least likely. For example, a call to "spin_lock" followed once by a call to "spin_unlock" implies that the programmer may have paired these calls by coincidence. If the pairing happens 999 out of 1000 times, though, then it is probably a valid belief and the sole deviation a probable error. The key feature of this approach is that it requires no a priori knowledge of truth: if two beliefs contradict, we know that one is an error without knowing what the correct belief is.Conceptually, our checkers extract beliefs by tailoring rule "templates" to a system --- for example, finding all functions that fit the rule template "a must be paired with b." We have developed six checkers that follow this conceptual framework. They find hundreds of bugs in real systems such as Linux and OpenBSD. From our experience, they give a dramatic reduction in the manual effort needed to check a large system. Compared to our previous work [9], these template checkers find ten to one hundred times more rule instances and derive properties we found impractical to specify manually.

REFERENCES

• 1: Alexander Aiken , Manuel Fähndrich , Zhendong Su, Detecting Races in Relay Ladder Logic Programs, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.184-200, March 28-April 04, 1998
• 2: 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
• 3: M. Bishop and M. Dilger. Checking for race conditions in file accesses. Computing systems, pages 131-152, Spring 1996.
• 4: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 6: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 7: D.L. Detlefs, R.M. Leino, G. Nelson, and J.B. Saxe. Extended static checking. TR SRC-159, COMPAQ SRC, December 1998.
• 8: Peter Harry Eidorff , Fritz Henglein , Christian Mossin , Henning Niss , Morten Heine Sørensen , Mads Tofte, AnnoDomini: from type theory to Year 2000 conversion tool, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292543]
• 9: D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of Operating Systems Design and Implementation (OSDI), September 2000.
• 10: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 11: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 12: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 13: R. W. Floyd. Assigning meanings to programs, pages 19- 32. J.T. Schwartz, Ed. American Mathematical Society, 1967.
• 14: D. Freedman, R. Pisani, and R. Purves. Statistics. W.W. Norton, third edition edition, 1998.
• 15: Gerard J. Holzmann , Margaret H. Smith, Software Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.481-497, October 05-08, 1999
• 16: G. Humpreys. Personal communication. Wasted days configuring a graphics card because of a missing error check in the driver., September 2000.
• 17: G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C.V. Lopes, J. Loingtier, and J. Irwin. Aspect-oriented programming. In European Conference on Object-Oriented Programming (ECOOP), June 1997.
• 18: David Lie , Andy Chou , Dawson Engler , David L. Dill, A simple method for extracting models for protocol code, Proceedings of the 28th annual international symposium on Computer architecture, p.192-203, June 30-July 04, 2001, Göteborg, Sweden
• 19: K.L. McMillan and J. Schwalbe. Formal verification of the gigamax cache consistency protocol. In Proceedings of the International Symposium on Shared Memory Multiprocessing, pages 242-51. Tokyo, Japan InL Process. Soc., 1991.
• 20: G. Nelson. Techniques for program verification. Available as Xerox PARC Research Report CSL-81-10, June, 1981, Stanford University, 1981.
• 21: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 22: Ulrich Stern , David L. Dill, Automatic verification of the SCI cache coherence protocol, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.21-34, October 02-04, 1995
• 23: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 24: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun ruinerabilities. In The 2000 Network and Distributed Systems Security Conference. San Diego, CA, February 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Debugging aids

General Terms:
Algorithms, Performance, Reliability