5
$\begingroup$

Looking at the DARPA’s Cyber Grand Challenge, it seems that (forward) Symbolic Execution (SE) is the tool of choice for all the top teams. For example:

  • Mayhem, the winner of the $2 millions prize
  • Driller, ranked 2nd or 3rd.

Maybe this is a stupid question, but if the purpose is to find the input that reach a location, e.g. the one that causes SIGSEGV, then intuitively going backward from that location is much easier that searching from forward. However, obviously those well-known scientists did not think so, and I wonder why.

Moreover, papers about forward SE appear in all software engineering conferences, and there is a survey every 2 or 3 years. But I don't remember the last time I read a paper about backward SE (that's why there is this possibly stupid question).

Are there any challenges that make backward SE either:

  • significantly more difficult to implement than forward SE, or
  • much less scalable than forward SE, or
  • ...
$\endgroup$
5
$\begingroup$

Forward SE is easier to implement, composes better with other testing methods, and thus is more scalable.

Usually, on industrial-scale workloads, it's not possible to enumerate all paths in the program under test -- there are simply too many paths. So we need some way to deal with this and sample only a subset of paths, while still having a reasonable chance of finding bugs. With forward SE, there is an easy way to deal with this: if you have a test case, you can run the program concretely for a while, then switch to forward SE partway through execution. Or, you can run the program concretely until it terminates, recording the path it took, and use SE to generate new inputs that will cause it to go down a similar but not identical path. The state-of-the-art tools tend to combine fuzzing (random testing) with SE, and this approach is a nice way to enable that sort of composition.

Second, forward SE has implementation benefits. Inevitably there are some kinds of operations that you can't or don't want to model symbolically (e.g., floating point, system calls, etc.). With forward SE, that's no problem: you just execute the program concretely and keep only part of the state symbolic, treating the results of those operations as concrete (you concretize by forcing their inputs to match the observed concrete value, and same for the outputs). It's usually not possible to do that concretization with backwards SE. So forward SE allows "concolic execution", where some of the state of the program is concrete (a single value) and some is treated as symbolic (represented by some variables that we accumulate constraints on).

Finally, many modern tools are path-based: they consider a single path through the program, and construct a path expression -- a set of constraints that characterize the set of inputs that will cause the program to follow that path. This is convenient for multiple reasons. When you take this approach, the differences between forward SE and backwards SE largely disappear, as there is no state merging; you only consider a single path at a time. So if you're taking this approach, in some sense you don't need to choose between the two, or the choice is inconsequential (both are basically equivalent) -- you can choose whichever you want based on which one you find a more convenient way to think about it.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.