Yannis Klonatos

An execution consistency model, as defined in the S2E paper, governs the transition from the concrete to the symbolic domain and back. In this OP I propose the use of a new consistency model motivated by ``what-if'' questions, like ``how bad would things get in my code if this totally unexpected (and possibly infeasible in practice for the given hardware) sequence S of events was to take place''. To answer such questions, one would ideally like to completely examine all inconsistent scenarios, an approach that is very computationally expensive. However, in practice there are occasions where we are only interested in estimating the ``badness'' of the outcome, but we do not care about all possible paths leading to this bad outcome. As a result of the above statements, the consistency model I propose is both incomplete (since we do not exhaustively search all paths) and inconsistent (since we search for unrealistic paths, like what would happen if most components of a distributed system were to fail at the same time). This model corresponds to the Venn diagram depicted on the right.

To begin with, each time we need to make a transition between the symbolic and the concrete domains (in either way), we ``flip a coin'' and we either make the transition to the opposite domain or not, according to the outcome. By doing so, we end up symbolically analyzing in part all three components of the system (kernel, libraries and application), and not just the unit (as was happening in the S2E paper). This approach results in the tree being expanded in depth and height by all three components, but not always (the ``when" is governed by the coin). By doing so, we give the user the possibility to acquire some (thus not total) knowledge about what could go wrong in the whole system.

There are several optimizations that can be made to this approach. First, the ``flipping of the coin'' does not necessarily have to be completely random. We can adjust a threshold during execution, depending on how much time symbolic analysis take. By doing so, if we see that in general the symbolic analysis takes too long, we can ``flip a coin'' that favors, e.g., two out of three times the concrete execution and one time the symbolic analysis. Secondly, if we see that the symbolic analysis ``gets stuck'' somewhere (e.g., in the case where unbounded symbolic variables are encountered in loops) we can fall back to the last switching point, and concretely execute the corresponding loop. Moreover, we can keep statistics about the symbolic execution of the system functions. By doing so, we can keep track of which functions take long to symbolically analyze, and decide that we will concretely execute those functions from now on, while ``keeping the coin'' for other functions and code segments that can be quickly symbolically analysed. As a final idea, we could also use information from the API specifications of specific functions (when such information is available) to govern the switching between concrete and symbolic modes.