Software often contains
many bugs. Fortunately, in the last half decade we have seen a
surge of work on automated bug-finding tools, such as those
based on static program analysis, that are adroit in finding
serious errors in real, multi-million line code bases.
Unfortunately, these tools are usually designed to look for bugs
violating generic invariants that may manifest in many systems (
e.g. do not dereference NULL), and have no knowledge of the
invariants and rules, or specification, that is specific to a
given system. The sad consequence is that these tools will miss
many important bugs that they could otherwise find if they only
had more knowledge of said specification.
This talk concerns the following question: how do we go about
automatically finding more system-specific bugs with our
bug-finding tools with as little human assistance as possible?
I will present a generic framework, based on probabilistic
graphical models and static program analysis, for inferring
specifications directly from systems code. Unlike previous
approaches, the technique provides a generic way of binding
together the arbitrary sources of information useful for
inferring specifications in a structured, non-ad hoc way. This
includes information gleamed from both analyzing the behavior of
a program as well as non-numeric insights such as suggestive
naming conventions, program structure, and the whole cadre of
information that lies dormant in code that in practice we as
coders exploit to reverse-engineer the semantics of code that is
foreign to us.
By tightly binding such information together, we can infer
specifications that can require an order of magnitude less data
than similar approaches, and using these specifications we have
found several serious bugs in code bases, such as the OS kernels
for Linux and Mac OS X, that would have otherwise remained
undetected. Moreover, we illustrate how inferring
specifications can be used as safety nets for our bug-finding
tools, as the inferred specifications can be used not only to
catch bugs in the programs we are analyzing, but also bugs in
our bug-finding tools.