Static analysis for bug finding in systems software

Building systems such as OS kernels and embedded software is notoriously difficult. A primary source of this difficulty is the numerous rules that must obeyed. For example, interrupts cannot be disabled for “too long”; global variables must be protected by locks; and user pointers passed to OS code must be checked for safety before use. A single violation can crash the system, lead to data corruption, or expose a security hole. Yet typically these invariants are unchecked, existing only on paper or in the implementor's mind. The only real practical methods known for verifying such code are testing and simulation, but these methods rarely exercise even a small fraction of executable paths. This work attacks this problem by providing a framework called Metacompilation (MC) that makes it easy to write simple compiler extensions to pinpoint errors in the program source code. These extensions can be written by system implementors themselves and, by exploiting system-specific information, can detect errors unreachable with other methods. We evaluate the MC approach by applying it to four complex, real systems: Linux, OpenBSD, the Xok exokernel, and the FLASH machine's embedded software. This has led to the discovery of over 1000 errors and has resulted in numerous patches to these systems. In addition, these results allow us to investigate the nature of the errors in Linux and OpenBSD. Our approach differs from previous studies that consider errors found by manual inspection of logs, testing, and surveys because static analysis is applied uniformly to the entire kernel source, though our approach necessarily considers a less comprehensive variety of errors than previous studies. In addition, automation allows us to track errors over multiple versions of the kernel source to estimate how long errors remain in the system before they are fixed.