Bugs as Deviant Behavior : A General Approa hto Inferring Errors in Systems

A major obstacle to nding program errors in a real system is knowing what correctness rules the system must obey. These rules are often undocumented or speciied 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(l)" implies that l was locked, etc. For beliefs we know the programmer must hold, such as the pointer dereference above, we immediately ag 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, nding all functions that t the rule template \ must be paired with ." We have developed six checkers that follow this conceptual framework. They nd hundreds of bugs in real systems such as Linux and OpenBSD. From our experience, they give a dramatic reduction in the manual eeort needed to check a large system. Compared to our previous work 9], these template checkers nd ten to one hundred times more rule instances and derive properties we found impractical to specify manually. 1 Introduction We want to nd as many serious bugs as possible. In our experience, the biggest obstacle to nding bugs is not the need for sophisticated techniques nor the lack of either bugs or correctness constraints. Simple techniques nd many bugs and systems are lled with both rules and errors. Instead, the biggest obstacle to nd-ing many bugs is simply knowing what rules …