Cross Checking Implementations for Bugs

Using static analysis to analyze large source bases for errors can be difficult because the correctness rules in the system are often numerous and undocumented. In order to check those systems, a human would have to enumerate those rules at the cost of weeks or years of effort. Engler et. al [7] introduced techniques to infer many of those rules from the source itself, saving much of the human effort. This thesis leverages some of those techniques to cross check implementations for consistency.
If there are multiple implementations of the same interface (i.e. device drivers all implement open, close, read, write), we can analyze the actions of those implementations to infer the correct behavior. For example, if most of the implementations check the first argument of open for NULL before dereferencing it, it is likely that all of the implementations should check that argument for NULL before dereferencing it. The implementations missing the checks are assumed to be in error.
To demonstrate the flexibility and capability of our technique, we use static analysis to infer the rules for four classes of bugs and apply them to the Linux kernel. We found dozens of errors with relatively little user effort in spite of the kernel's size and lack of documentation.