24-11-2012, 06:33 PM
Static Error Detection using Semantic Inconsistency Inference
1Static Error Detection.pdf (Size: 229.44 KB / Downloads: 18)
Abstract
Inconsistency checking is a method for detecting software errors
that relies only on examining multiple uses of a value. We propose
that inconsistency inference is best understood as a variant of the
older and better understood problem of type inference. Using this
insight, we describe a precise and formal framework for discovering
inconsistency errors. Unlike previous approaches to the problem,
our technique for finding inconsistency errors is purely semantic
and can deal with complex aliasing and path-sensitive conditions.
We have built a null dereference analysis of C programs
based on semantic inconsistency inference and have used it to find
hundreds of previously unknown null dereference errors in widely
used C programs.
Introduction
Much recent work in static analysis focuses on source-sink properties:
For safety policy S, if S is violated when a value constructed
at location l1 is consumed at location l2, then is there a feasible
path from l1 to l2? If the answer is “yes,” then the program has a
bug (violates policy S). Some typical specifications are:
• Does a null value assigned to a pointer or reference reach a
pointer dereference?
• Does any closed file reach a file read?
• Does a tainted input reach a security critical operation?
Guards
To allow for path-sensitivity in our static analysis, we construct
guards that express program constraints. We use boolean satisfiability
(SAT) as the underlying decision procedure for solving constraints;
hence guards are represented as boolean formulas. In this
section, we describe how to compute two kinds of guards:
• statement guards that describe the conditions under which a
statement executes,
• constructor guards that describe the condition under which a
variable x at a given program point evaluates to a constructor
Ci. In addition, a constructor guard also encodes the source of
the value Ci
Error Detection
In this section we present techniques for identifying source-sink
and inconsistency errors using the machinery developed in Section
2. Only intraprocedural techniques are discussed here; Section
4 extends the approach across function boundaries.
Source-Sink Errors
Source-sink errors arise when a value constructed at one program
point reaches an unexpected destructor at a different program point.
Most errors uncovered by model checking tools, and particularly
model checkers based on counter-example driven refinement, are
source-sink errors. This class of errors includes, for example, typestate
properties, such as errors that arise from dereferencing a
pointer that has been assigned to null, or using a tainted input in
a security critical operation.
Intersection of Source-Sink and Inconsistency Errors
Our discussion so far highlights that source-sink and inconsistency
error detection techniques are fundamentally different: First, detection
of source-sink errors involves reasoning about a single program
path, while the detection of inconsistencies can require reasoning
about multiple paths. Second, source-sink error detection
requires the source to be explicit in the source code, while inconsistency
detection infers errors only from usage sites, i.e., sinks,
and can therefore find errors even when the source comes from the
environment.
Function Summaries
A function summary describes the preconditions on the execution
of a function that, if satisfied, may lead to errors. Computing sound
and very precise preconditions is easy in our framework; the disjunction
of all the failure conditions for every check statement in
a function characterizes exactly the condition under which some
check will fail. Unfortunately, propagating such precise information
interprocedurally is prohibitively expensive; the formulas grow
very rapidly as conditions are propagated through a series of function
calls.
We take a different approach to function summaries that is
designed to scale while still expressing all the possible conditions
under which a check in a function may fail. The price we pay is
a loss of precision in the general case; one can construct examples
for which our summaries greatly overestimate the precondition for
failure. However, our summaries do precisely summarize the failure
precondition of the vast majority of functions we have observed in
practice.
A Null Dereference Analysis
In this section, we apply our approach to the problem of detecting
null dereference errors in C programs.We first present an encoding
of the null dereference problem in our framework and then discuss
extensions needed to analyze C.
To apply the techniques in Sections 2-4 to the problem of detecting
unsafe null dereferences, we need only define the constructors
and an appropriate congruence relation. Null dereference analysis
is about understanding what pointers can be null, which in turn requires
a reasonably precise model of all the possible values of all
pointers in a program. Our C implementation incorporates a sound
context-, flow- and partially path-sensitive points-to analysis for C
[11]. Most points-to analyses compute a graph where the nodes V
are the set of abstract locations and there is an edge (v, v0) 2 E
if location v may point to v0. The points-to analysis we use labels
each points-to edge with a guard (v, v0)g, where g is a formula
specifying under what conditions v points to v0. The value NULL is
treated as a node in the graph, so (v, NULL)g means that v may be
a NULL pointer whenever guard g is satisfied.
For the congruence relation, given a guarded
Results
We have run our null dereference analysis on seven widely used
open source projects and identified 616 null dereference issues with
149 false positive reports (an overall 19.5% false positive rate).
These projects receive regular source code checking from multiple
commercial bug-finding tools, and so we sought to learn whether
these bugs had been previously reported. Developers for the Samba
project confirmed that none of the Samba bugs had been previously
found. For the other projects we did not receive such an explicit
acknowledgment that the bugs were new; however, we judge from
the fact that fixes were released quickly for many of the bugs shortly
after our reports were filed that at least the majority of the bugs we
found were previously unknown. The large majority of these bugs,
518, were found by our inconsistency analysis.
We ran our null dereference analysis on a compute cluster.
Analyzing the Linux kernel with over 6 MLOC required about 4
hours using 30 CPU’s, which was by far the longest time required
for any of the projects. The smallest project we analyzed was
OpenSSH, which took 2 minutes and 33 seconds to analyze on
the same cluster. Our system makes many calls to a boolean SAT
solver to test the satisfiability of the various predicates used in
our analyses, and for Linux the number of SAT queries numbers
in the millions. We impose a 60 second time limit for analyzing
any individual function; if the analysis of a function times out, its
function summary is incomplete.
RelatedWork
The various program analysis traditions appear to have equivalent
power; for example, there is an equivalence between type systems
and model checking [15]. However, these results are for closed programs.
We observe that for open programs techniques that search
only for a single source-sink path cannot express inconsistency errors
requiring simultaneous reasoning about multiple distinct paths.
We view semantic inconsistency checking as complementary to
source-sink error detection; inconsistency checking can find bugs
where there are multiple sinks but no sources, while source-sink
checking can detect bugs between a single source and a single sink.
Our choice of the terms constructor and destructor is inspired
by work on detecting uncaught exceptions in functional programs
[18, 17] and soft typing [4, 1]. A core issue in both bodies of
work is tracking which datatype constructors a program value may
actually have at run-time. Null dereference analysis is a special case
where there are only two constructors NULL and NON-NULL; our
techniques could be adapted to give very precise analysis for these
other applications as well.