search

moralismercatus / crete

Open source concolic testing tool for binaries
1 stars 1 forks source link

Taint analysis and execution tree erroneously cause traces to be marked as redundant #159

Closed moralismercatus closed 8 years ago

moralismercatus commented 8 years ago

Take the following program:

int counter = 0;
char in[100];
for (int i = 0; i < 100; ++i)
  if (in[i] == 'C')
    ++counter;
if (counter == 42)
  ...;

The loop has 2^100 unique paths through it. However, because TA only marks the TB for if (in[i] == 'C') as symbolic, the trace is effectively 100 of that single TB. Because the true-block ++counter; is not symbolic, it is never dumped, and thus, to the execution tree, it looks redundant.

One solution is to dump the TB sequence for constructing the execution tree separately from TA. Essentially, this amounts to a capture-all TB sequence which, in itself, can be troublesome. Firstly, the number is going to be huge. Secondly, interrupts will likely be a problem. By 'capturing all' we are more prone to being interrupted, and since interrupts are random, they will make each trace unique (not to mention possibly throw off the trace selection algorithm).

Another solution may be to not only use the TB address as a unique identifier, but also the result of the expression. If we limit the TBs to conditional branching TBs, we can actually embed the result of the expression along with the address to form a unique node in the graph. The main drawback here is that I'm not 100% certain that conditional branches are the only test-case generating TBs.

moralismercatus commented 8 years ago

The solution that we chose was to include the next TB after the last tainted TB each time we transition from a tainted to non-tainted TB, in the TB sequence for the graph.