Full Program »
Paper ACM |
Presentation |
Systematic Comparison of Symbolic Execution Systems: Intermediate Representation and its Generation
Symbolic execution has become a popular technique for software testing and
vulnerability detection. Most implementations transform the program under
analysis to some intermediate representation (IR), which is then used as a basis
for symbolic execution. There is a multitude of available IRs, and even more
approaches to transform target programs into a respective IR.
When developing a symbolic execution engine, one needs to choose an IR, but it
is not clear which influence the IR generation process has on the resulting
system. What are the respective benefits for symbolic execution of generating IR
from source code versus lifting machine code? Does the distinction even matter?
What is the impact of not using an IR, executing machine code directly? We feel
that there is little scientific evidence backing the answers to those questions.
Therefore, we first develop a methodology for systematic comparison of different
approaches to symbolic execution; we then use it to evaluate the impact of the
choice of IR and IR generation. We make our comparison framework available to
the community for future research.