Akademska digitalna zbirka SLovenije - logo
E-resources
Full text
Peer reviewed Open access
  • Testing concolic execution ...
    Coppa, Emilio; Izzillo, Alessio

    The Journal of systems and software, 20/May , Volume: 211
    Journal Article

    Symbolic execution is a well-known software testing technique that evaluates how a program runs when considering a symbolic input, i.e., an input that can initially assume any concrete value admissible for its data type. The dynamic twist of this technique is dubbed concolic execution and has been demonstrated to be a practical technique for testing even complex real-world programs. Unfortunately, developing concolic engines is hard. Indeed, an engine has to correctly instrument the program to build accurate symbolic expressions, which represent the program computation. Furthermore, to reason over such expressions, it has to interact with an SMT solver. Hence, several implementation bugs may emerge within the different layers of an engine. In this article, we consider the problem of testing concolic engines. In particular, we propose several testing strategies whose main intuition is to exploit the concrete state kept by the executor to identify inconsistencies within the symbolic state. We integrated our strategies into three state-of-the-art concolic executors (SymCC, SymQEMU, and Fuzzolic, respectively) and then performed several experiments to show that our ideas can find bugs in these frameworks. Overall, our approach was able to discover more than 12 bugs across these engines. •We identify the main steps carried out by recent concolic frameworks during their analysis, pinpointing where implementation bugs may emerge.•We propose a set of novel and practical ideas on how to identify implementation gaps in modern concolic executors.•We integrate our strategies into state-of-the-art concolic executors and perform experiments to show that our ideas can find bugs in these frameworks.