Identifying Systemic Threats to Kernel Data - Advanced Operating Systems and Kernel Applications - page 59

linked lists, implemented in the Linux kernel us-
ing the list_head structure. In Linux, other kernel
data structures (called containers ) that must be
organized as a linked list simply include the list
head data structure. The kernel provides func-
tions to add, delete, and traverse list head data
structures. Such linked lists are problematic for
the data structure extractor. In particular, when it
encounters a list head structure, it will be unable
to identify the container data structure. To handle
such linked lists, we use the Container annotation.
The annotation explicitly specifies the type of the
container data structure and the field within this
type, to which the list head pointers refer. The
extractor uses this annotation and locates the
container data structure. In our experiments, we
annotated all 163 annotations of the list_head data
structure in the Linux-2.4.20 kernel.
In addition to linked lists, Gibraltar may
also require assistance to disambiguate opaque
pointers (void *), dynamically allocated arrays
and untagged unions. For example, the extractor
would require the length of dynamically-allocated
arrays in order to traverse and locate objects in
the array. We plan to add support for dynamic
arrays, opaque pointers and untagged unions in
future work.
Because the page fetcher obtains pages from
the target asynchronously (without halting the
target), it is likely that the data structure extractor
will encounter inconsistencies, such as pointers
to non-existent objects. Such invalid pointers are
problematic because the data structure extractor
will incorrectly fetch and parse the memory re-
gion referenced by the pointer (which will result
in more invalid pointers being added to the work
list of the traversal algorithm). To remedy this
problem, we currently place an upper bound on
the number of objects traversed by the extractor. In
our experiments, we found that on an idle system,
the number of data structures in the kernel varies
between 40,000 and 65,000 objects. We therefore
place an upper bound of 150,000; the data structure
extractor aborts the collection of new objects when

this threshold is reached. In our experiments, this
threshold was rarely reached, and even so, only
when the system was under heavy load.

the invariant generator

In the training mode, the output of the data struc-
ture extractor is used by the invariant generator,
which infers likely data structure invariants.
These invariants are used as specifications of data
structure integrity.
To extract data structure invariants, we adapted
Daikon (Ernst, 2006), a state of the art invariant
inference tool. Daikon was developed to dynami-
cally infer invariants for application programs.
An invariant is a property that holds at a certain
point or points in a program; these are often used
in assert statements and for formal specifications.
For application programs, invariants can be useful
mainly in program understanding. It can also be
used for generating test cases, predicting incom-
patibilities in component integration, automating
theorem proving and repairing inconsistent data
structures.
Daikon attempts to infer likely program
invariants by observing the values of variables
during multiple executions of a program. Daikon
first instruments the program to emit a trace that
contains the values of variables at selected pro-
gram points , such as the entry points and exits
of functions. It then executes the program on a
test suite, and collects the traces generated by the
program. Finally, Daikon analyzes these traces and
hypothesizes invariants—properties of variables
that hold across all the executions of the program.
The invariants produced by Daikon conform to one
of several invariant templates . For example, the
template x == const checks whether the value of
a variable x equals a constant value const (where
const represents a symbolic constant; if x has
the constant value 5, Daikon will infer x == 5 as
the invariant). Daikon also infers invariants over
collections of objects. For example, if it observes
that the field bar of all objects of type struct foo