Archive (Fall 2009)‎ > ‎One-Pagers‎ > ‎

OP7: Environment Be Damned !

Symbolically executing a program requires either isolating that program from the environment it runs in, or somehow incorporating environment interactions in the symbolic execution itself. The KLEE paper describes one approach to doing this, namely modeling the environment. The S2E paper offers a different perspective on the same problem: "simulate" the symbolic execution of the environment, i.e., give the symbolically executing program the illusion that the entire software stack is being symbolically executed.

This simulation approach is not easy to get right, if one wants to preserve the correctness and completeness of the program's symbolic execution. Identify one major challenge with the S2E approach, describe the problem clearly, and speculate on how it might be solved in the context of S2E. Support your problem description with concrete examples.