Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program’s authentication. One approach would be to test the program using different, possibly random inputs. As the backdoor may only be hit for very specific program workloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution provides an elegant solution to the problem, by systematically exploring many possible execution paths at the same time without necessarily requiring concrete inputs. Rather than taking on fully specified input values, the technique abstractly represents them as symbols, resorting to constraint solvers to construct actual instances that would cause property violations. Symbolic execution has been incubated in dozens of tools developed over the last four decades, leading to major practical breakthroughs in a number of prominent software reliability applications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutions developed in the area, distilling them for a broad audience.

A Survey of Symbolic Execution Techniques / Baldoni, Roberto; Coppa, Emilio; D'Elia, Daniele Cono; Demetrescu, Camil; Finocchi, Irene. - In: ACM COMPUTING SURVEYS. - ISSN 0360-0300. - 51:3(2018), pp. 50:1-50:39. [10.1145/3182657]

A Survey of Symbolic Execution Techniques

Finocchi, Irene
2018

Abstract

Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program’s authentication. One approach would be to test the program using different, possibly random inputs. As the backdoor may only be hit for very specific program workloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution provides an elegant solution to the problem, by systematically exploring many possible execution paths at the same time without necessarily requiring concrete inputs. Rather than taking on fully specified input values, the technique abstractly represents them as symbols, resorting to constraint solvers to construct actual instances that would cause property violations. Symbolic execution has been incubated in dozens of tools developed over the last four decades, leading to major practical breakthroughs in a number of prominent software reliability applications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutions developed in the area, distilling them for a broad audience.
Symbolic execution; static analysis; concolic execution; software testing
A Survey of Symbolic Execution Techniques / Baldoni, Roberto; Coppa, Emilio; D'Elia, Daniele Cono; Demetrescu, Camil; Finocchi, Irene. - In: ACM COMPUTING SURVEYS. - ISSN 0360-0300. - 51:3(2018), pp. 50:1-50:39. [10.1145/3182657]
File in questo prodotto:
File Dimensione Formato  
Baldoni_A-Survey_2018.pdf

Solo gestori archivio

Tipologia: Versione dell'editore
Licenza: DRM non definito
Dimensione 1.3 MB
Formato Adobe PDF
1.3 MB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Caricamento 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: http://hdl.handle.net/11385/192577
Citazioni
  • Scopus 253
  • ???jsp.display-item.citation.isi??? 168
social impact