Exponential Analysis Speedup with State Merging

Symbolic execution can produce an exponential number of paths, considerably slowing down analysis. When S2E encounters a branch that depends on a symbolic condition and both outcomes are possible, S2E forks the current execution path in two. This process can repeat recursively, resulting in an exponential number of paths.

The following piece of code demonstrates the problem. It is a simplification of the ShiftInBits() function of the Intel e100bex NIC driver from the Windows WDK. It consists of a loop that reads a value from a hardware register bit-by-bit.

uint16_t ShiftInBits() {
    uint16_t value = 0;

    for (int i = 0; i < sizeof(value) * 8; ++i) {
        value <<= 1;

        if (read_register()) {
            value |= 1;
        }
    }

    return value;
}

On each iteration, read_register() returns a fresh symbolic value, causing a fork at the conditional statement. Since there are 16 iterations in total, this amounts to 65,536 execution states.

If we look closely, every forked path in the function above differs only by one bit, set to zero or one depending on the register value. If S2E could merge both paths back together while remembering that small difference, there would remain only one path at the end of the function, reducing by four orders of magnitude the number of paths to explore.

Using State Merging in S2E

To use state merging in S2E, first enable the MergingSearcher plugin.

-- File: config.lua
s2e = {
    kleeArgs = {
        -- needed to avoid merge failures due to different shared-concrete objects:
        "--state-shared-memory=true"
    }
}

plugins = {
    "BaseInstructions",
    "MergingSearcher"
}

Then, compile the following program, then run it in S2E:

#include <s2e/s2e.h>

uint16_t ShiftInBits() {
    uint16_t value = 0;
    int i;

    for (i = 0; i < sizeof(value) * 8; ++i) {
        value <<= 1;

        /* Simulates read_register() */
        uint8_t reg = 0;
        s2e_make_symbolic(&reg, sizeof(reg), "reg");

        s2e_disable_all_apic_interrupts();
        s2e_merge_group_begin();

        if (reg) {
            value |= 1;
        }

        s2e_merge_group_end();
        s2e_enable_all_apic_interrupts();
    }

    return value;
}

int main(int argc, char **argv) {
    uint16_t value = ShiftInBits();
    if (value == 0xabcd) {
        s2e_printf("found it\n");
    }

    return 0;
}

How many paths do you observe?
Comment out calls to s2e_merge_group_begin() and s2e_merge_group_end(). How does this affect the number of paths?

State Merging API

The S2E state merging API offers two calls: s2e_merge_group_begin() and s2e_merge_group_end().

The subtree that begins at s2e_merge_group_begin() and whose leaves end at s2e_merge_group_end() is merged into one path. The MergingSearcher behaves as follows:

The searcher suspends the first path (path A) that reaches s2e_merge_group_begin().

If path A did not fork any other path between s2e_merge_group_begin() and s2e_merge_group_end(), there is nothing to merge, and the searcher resumes path A normally.
If path A forked other paths (e.g., B and C), the searcher schedules another path. The scheduled path could be B, C, or any other path outside the subtree to be merged.
When path B reaches s2e_merge_group_end(), MergingSearcher merges it with A, then kills B.
When path C reaches s2e_merge_group_end(), MergingSearcher merges it with A+B, then kills C.

Limitations

It is not possible to nest pairs of s2e_merge_group_begin() and s2e_merge_group_end().
S2E must be running in concrete mode when merging states (s2e_merge_group_end() ensures that it is the case).
The set of symbolic memory objects must be identical in all states that are going to be merged. For example, there shouldn’t be calls to s2e_make_symbolic between s2e_merge_group_begin() and s2e_merge_group_end().
It is not possible to merge two states if their concrete CPU state differs (e.g., floating point or MMX registers, program counter, etc.).
s2e_disable_all_apic_interrupts() and s2e_enable_all_apic_interrupts() ensure that the concrete state is not clobbered needlessly by interrupts. The direct consequence is that the merged subtree cannot call into the environment (no syscalls, etc.). Not disabling interrupts will make merging much harder because the side effects of the interrupt handlers and those of the OS will have to be merged as well. If the side effects affected the concrete CPU state, merging will fail.