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.

Testing concolic execution through consistency checks / Coppa, Emilio; Izzillo, A.. - In: THE JOURNAL OF SYSTEMS AND SOFTWARE. - ISSN 0164-1212. - 211:(2024), pp. 1-16. [10.1016/j.jss.2024.112001]

Testing concolic execution through consistency checks

Coppa E.;
2024

Abstract

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.
2024
Symbolic execution, Testing, Concolic execution
Testing concolic execution through consistency checks / Coppa, Emilio; Izzillo, A.. - In: THE JOURNAL OF SYSTEMS AND SOFTWARE. - ISSN 0164-1212. - 211:(2024), pp. 1-16. [10.1016/j.jss.2024.112001]
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S016412122400044X-main.pdf

Open Access

Descrizione: Articolo
Tipologia: Versione dell'editore
Licenza: Creative commons
Dimensione 794.93 kB
Formato Adobe PDF
794.93 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11385/239418
Citazioni
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
  • OpenAlex ND
social impact