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

A major obstacle to nding program errors in a real sys-tem is knowing what correctness rules the system must obey. These rules are often undocumented or specied in an ad hoc manner. This paper demonstrates tech-niques that automatically extract such checking infor-mation from the source code itself, rather than the pro-grammer, thereby avoiding the need for a priori knowl-edge of system rules. The cornerstone of our approach is inferring pro-grammer \beliefs " that we then cross-check for contra-dictions. 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 be-liefs we know the programmer must hold, such as the pointer dereference above, we immediately ag contra-dictions as errors. For beliefs that the programmer may hold, we can assume these beliefs hold and use a sta-tistical analysis to rank the resulting errors from most to least likely. For example, a call to \spin lock " fol-lowed 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 tailor-ing rule \templates " to a system { for example, nding all functions that t the rule template \<a> must be paired with <b>. " 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 eort needed to check a large system. Com-pared 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 man-ually.