Information Technology Reference
In-Depth Information
at a program point have the value 5, it will infer
the invariant “The fields bar of all objects of type
struct foo have value 5.”
We had to make three key changes to adapt
Daikon to infer invariants over kernel data
structures.
init tasks->next task (here, init tasks is a
root symbol). The extractor names each
data structure as it is visited for the first
time.
In addition, Gibraltar also associates each
name with the virtual memory address of the data
structure that it represents in the snapshot. These
addresses are used during invariant inference,
where they help identify cases where the same
name may represent different data structures in
multiple snapshots. This may happen because of
deallocation and reallocation. For example, sup-
pose that the kernel deallocates (and reallocates,
at a different address) the head of the all-tasks
linked list. Because the name init tasks->next task
will be associated with different virtual memory
addresses before and after allocation, it represents
different data structures; Gibraltar ignores such
objects during invariant inference.
Inference over snapshots. Daikon is
designed to analyze multiple execution
traces obtained from instrumented pro-
grams and extract invariants that hold
across these traces. We cannot use Daikon
directly in this mode because the target's
kernel is not instrumented to collect ex-
ecution traces. Rather, we obtain values
of data structures by asynchronously ob-
serving the memory of the target kernel.
To adapt Daikon to infer invariants over
these data structures, we represent all the
data structures in one snapshot of the tar-
get's memory as a single Daikon trace. As
described in 3.2, the data structure extrac-
tor periodically reconstructs snapshots of
the target's memory. Multiple snapshots
therefore yield multiple traces. Daikon
processes all these traces and hypothesiz-
es properties that hold across all traces,
thereby yielding invariants over kernel
data structures
Linked data structures. Linked lists are
ubiquitous in the kernel and, as demon-
strated later in 4.2, can be exploited sub-
tly by rootkits. It is therefore important to
preserve the integrity of kernel linked lists.
Daikon, however, does not infer invariants
over linked lists. To overcome this short-
coming, we represented kernel linked lists
as arrays in Daikon trace files, and lever-
aged Daikon's ability to infer invariants
over arrays. We then converted the invari-
ants that Daikon inferred over these arrays
to invariants over linked lists.
Naming data structures. Because
Daikon analyzes instrumented programs,
it represents invariants using global vari-
ables and the local variables and formal
parameters of functions in the program.
However, because Gibraltar aims to infer
invariants on data structures reconstructed
from snapshots, the invariants output by
Gibraltar must be represented using the
root symbols. Gibraltar represents each
data structure in a snapshot using its name
relative to one of the root symbols. For
example, Gibraltar represents the head of
the all-tasks linked list, using the name
Daikon infers invariants that conform to 75 dif-
ferent templates (Ernst, 2006), and infers several
thousand invariants over kernel data structures
using these templates. In the discussion below,
and in the experimental results reported in section
4, we focus on five templates; in the templates
below, var denotes either a scalar variable or a
field of a structure.
Search WWH ::




Custom Search