symbolic length symbolic execution

1 They generalize symbolic execution to examining more than one execution path at a time by introducing symbolic variables for the number of times each loop executes and linking it to features as variable-length or repeating fields (what is it?). They examine a class of paths at a time. Can we do this not only for loops? They use term single-path symbolic execution (SPSE) for the common concolic. They present loop-extended symbolic execution (LESE). It performs more detailed analysis to identify loop-dependent variables (e.g. which variables is a linear function of index).

2 Their tests is for binary code. They said, concolic is a combination between dynamic and static analysis (they refer to EXE, DART, CUTE).

while (input[ptr] != DELIMITER) {
    // do something
    index++; ptr++;
}
if (index > 8) {...}

Single-path exploration does not have enough information to reason about index value. Is it a implicit dependency? 3 In SPSE some concrete values indirectly dependent on the input because of loops. In LESE they are symbolic. They introduce new class of symbolic variables—trip count. Each loop has a trip count (number of times loop has executed). Construct relationships: input ↔ trip count ↔ symbolic variable. They are looking for linear functions of the trip counts (covers a lot). For input ↔ count connection they introduce auxiliary input variables for lengths and repetition counts.

LESE diagram

Sergey Vartanov, 2007–2020