One of BAP’s biggest omissions is that it does not do CFG/code
recovery. CFG recovery (or code recovery) is the process of finding
what parts of an executable are code. If you have ever used IDA Pro,
when you first load a file, the initial analysis phase is actually
performing CFG recovery. For this, IDA Pro uses a combination of
recursive disassembly (if address `a`

is code and has `jmp 1234`

, then
`1234`

must be code too) and heuristics like looking for ```
push %ebp;
mov %esp, %ebp
```

.

A third approach to CFG recovery, besides recursive disassembly and
heuristics, is abstract interpretation. Abstract interpretation is a
method for analyzing programs in a sound way. One abstract
interpretation algorithm for recovering CFGs is called Value Set Analysis, or VSA for short. VSA works by overapproximating the values of variables by using strided intervals. A strided interval is a combination of an interval, like [1,3], which represents the set {1,2,3}, and an interval, which represents the step between each element. For instance, the strided interval 5[0,9] represents the set {0,4,9}. The idea in VSA is that once you can approximate program values in this way, you can then reason about (resolve) indirect jumps, and thus recover the CFG.

BAP has a partial implementation of VSA, but it needs some re-design
before we can use it for CFG recovery. First, we need to change the
type of CFG edges. Right now, CFG edges are of type `bool option`

,
since an edge can be an unconditional jump (`None`

), or be the taken
or non-taken edge of a conditional jump (`Some true`

or `Some false`

).
However, we need more expressive edges for two reasons. First, we
need to represent information about recovered indirect jumps. For
instance, we might find that `jmp (%eax)`

goes to address 10 when `%eax`

is 30, and to address 20 when `%eax`

is 100. Obviously we can’t
represent this using true and false; we need expression types. The
second reason we need more expressive edges is that some abstract
interpretation algorithms, like VSA, are defined for both program
statements *and* edge conditions.

This is best understood with an example. In the above program,
it’s easy to see that `x`

can only contain the values {0,1,2} coming
into BB 1. We know this, because `x`

starts with value 0, and if it
had a value above 3, control would transfer to BB 2. VSA can actually
determine this. BAP’s VSA does not take edge conditions into account
(after all, edges have no conditions!), and so BAP would be forced to
conclude that the range of `x`

is [0, ∞] coming into BB 1.

Okay, so we want to add conditions to CFG edges. BAP’s VSA
implementation uses the Single Static Assignment (SSA) form, so let’s
convert our program to that and see what it looks like.

What’s this `temp`

variable? Well, it’s a temporary variable introduced
because BAP’s SSA form is three address code (TAC). TAC ensures that each expression has no subexpressions. Instead, subexpressions must be computed with separate assignments. This makes some analyses simpler. For instance, Strongly
Connected Component Value Numbering (SCCVN) can easily identify common
subexpressions, since each subexpression gets its own assignment.

Unfortunately, TAC comes back to bite us in VSA. The edge ```
temp =
false
```

does not convey any information about `x`

to VSA, since VSA can
only relate edge conditions to data values syntactically, that is to
`temp`

. This is the major difference between abstract interpretation
and a symbolic analysis like symbolic execution. Symbolic analysis
can reason about the effect of an edge condition on a data value with
symbolic constraints. Abstract interpretation typically does not
involve constraint solving, and thus VSA does not know how an edge
condition affects a data value in the general case.

So, to make a long story short, I am going to adjust BAP’s SSA
representation so that TAC is not enforced by the type system.
Instead, we’ll have an option to lift to TAC, which we will use with
SCCVN. VSA, however, will use the non-TAC version of SSA. Once VSA
is fixed, it should be straight-forward to use the resulting
information to do CFG recovery.