Hi,
This is to present to you a new extension to JPF, concolic execution,
and a fuzzing tool built on the extension, jFuzz.
The goal is to create effective test inputs for programs that read
(binary or text) files.
The concolic extension can be used separately from jFuzz and used for
other purposes.
In short, during concolic execution, the program runs as usual but
also keeps track of the precise way the inputs influences the control
path. The result is a logical fomula, path condition, that describes
the input and, importantly, the set of all inputs that would drive the
program execution along the same control-flow path. Concolic execution
is similar to symbolic execution in that it collects constraints and
marks inputs as symbolic, but concolic execution is different in that
the original program execution is not affected, the exact same
concrete values are used, and that only 1 execution path is taken (as
opposed to the whole execution tree in symbolic execution).
jFuzz is a fuzzer build on concolic execution. It's goal is to create
program inputs (files) that exercise many distinct execution path in
the program under test. jFuzz works by running JPF in concolic mode
many times. First time jFuzz runs, it collects the path condition.
Then, jFuzz negates each path of the path condition systematically,
and by solving them using a constraint sover, jFuzz creates
additional program inputs, each designed to exercise a unique path.
The code is in the 'concolic' source folder. The Readme.html in that
folder gives additional information.
The readme is duplicated here http://people.csail.mit.edu/dharv/jfuzz/
Over the next months, we will work on improvements to concolic and
jFuzz: caching for constraints, input selection heuristics and
parallelization. If you're interested in helping out - write me an
email (ak...@cs...)
The concolic extension and jFuzz were developed by David Harvison and
Adam Kiezun at MIT, with guidance from Corina Pasareanu and Peter
Dillinger from NASA.
./adam
|
