Vine: The BitBlaze Static Analysis Component
[Overview] [Publications] [Back to BitBlaze]
In order to reason about assembly (an in particular, x86 assembly),
it is necessary to accurately model the effects of each
instruction. However, this is a difficult task, since x86 consists of
hundreds of instructions. Compounding the problem is the fact that x86
has instruction with implicit side effects (e.g., setting the EFLAGS
register), complex instructions (e.g., single instruction loops using
"rep"), several register addressing modes, and even the semantics of
the instruction themselves may change depending on the operand (e.g.,
"shl" does not set EFLAGS when the shift amount is 0, else it does).
In order to address these problems, we have developed Vine, an
intermediate language (IL) for reasoning about assembly. We lift up
all x86 instructions to the Vine IL, which in a simple, RISC like
language that makes subsequent analysis possible. Our IL reduces the
hundreds of x86 instructions to about a dozen different
statements. Note our IL is not a decompilation: our goal is not to
recover a higher-level language representation of the code, but to
analyze assembly as a first class language.
Vine also provides an infrastructure for manipulating and performing
automated analysis on our IL. We current have the ability to:
- Build control flow graphs of the program.
- Perform dataflow analysis, such as constant propagation, global
value numbering, and dead code elimination.
- Create a program dependence graph consisting of control and data
dependencies.
- Create a chop of the graph where only those instructions which
are relevant to a user-specified source and sync are included.
- Translate our IL to C, and then compile back down to an
executable.
- Interface with a theorem prover. We currently interface with STP and CVC Lite.
Our Vine infrastructure consists of code written in C++ to lift x86 to
the ILA, and OCaml to then perform additional analysis.
- Vine Living Document
- by David Brumley. This is a living document on our IL. This is
intended to give a high level feel of Vine. For developers and the
exact semantics, developers should consult the online automatically
generated documentation.
Back to BitBlaze