Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, FUZZY-SAT, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers.

Fuzzing Symbolic Expressions / Borzacchiello, Luca; Coppa, Emilio; Demetrescu, Camil. - (2021), pp. 711-722. (Intervento presentato al convegno 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE) tenutosi a Online) [10.1109/ICSE43902.2021.00071].

Fuzzing Symbolic Expressions

Borzacchiello, Luca
;
Coppa, Emilio
;
Demetrescu, Camil
2021

Abstract

Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, FUZZY-SAT, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers.
2021
2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)
Fuzzing; software testing; concolic execution; SMT solver;
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Fuzzing Symbolic Expressions / Borzacchiello, Luca; Coppa, Emilio; Demetrescu, Camil. - (2021), pp. 711-722. (Intervento presentato al convegno 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE) tenutosi a Online) [10.1109/ICSE43902.2021.00071].
File allegati a questo prodotto
File Dimensione Formato  
Borzacchiello_postprint_Fuzzing_2021.pdf

accesso aperto

Note: DOI: 10.1109/ICSE43902.2021.00071
Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 489.54 kB
Formato Adobe PDF
489.54 kB Adobe PDF
Borzacchiello_Fuzzing_2021.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 2.79 MB
Formato Adobe PDF
2.79 MB Adobe PDF   Contatta l'autore

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/11573/1553682
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 11
social impact