Symbolic execution is a popular program analysis technique that allows seeking for bugs by reasoning over multiple alternative execution states at once. As the number of states to explore may grow exponentially, a symbolic executor may quickly run out of space. For instance, a memory access to a symbolic address may potentially reference the entire address space, leading to a combinatorial explosion of the possible resulting execution states. To cope with this issue, state-of-the-art executors concretize symbolic addresses that span memory intervals larger than some threshold. Unfortunately, this could result in missing interesting execution states, e.g., where a bug arises. In this paper we introduce MemSight, a new approach to symbolic memory that reduces the need for concretization, hence offering the opportunity for broader state explorations and more precise pointer reasoning. Rather than mapping address instances to data as previous tools do, our technique maps symbolic address expressions to data, maintaining the possible alternative states resulting from the memory referenced by a symbolic address in a compact, implicit form. A preliminary experimental investigation on prominent benchmarks from the DARPA Cyber Grand Challenge shows that MemSight enables the exploration of states unreachable by previous techniques.

Rethinking Pointer Reasoning in Symbolic Execution / Coppa, Emilio; D'Elia, Daniele Cono; Demetrescu, Camil. - STAMPA. - (2017), pp. 613-618. (Intervento presentato al convegno 32nd IEEE/ACM International Conference on Automated Software Engineering tenutosi a Urbana, Illinois, USA nel 30 October 2017 through 3 November 2017) [10.1109/ASE.2017.8115671].

Rethinking Pointer Reasoning in Symbolic Execution

Coppa, Emilio;D'Elia, Daniele Cono;Demetrescu, Camil
2017

Abstract

Symbolic execution is a popular program analysis technique that allows seeking for bugs by reasoning over multiple alternative execution states at once. As the number of states to explore may grow exponentially, a symbolic executor may quickly run out of space. For instance, a memory access to a symbolic address may potentially reference the entire address space, leading to a combinatorial explosion of the possible resulting execution states. To cope with this issue, state-of-the-art executors concretize symbolic addresses that span memory intervals larger than some threshold. Unfortunately, this could result in missing interesting execution states, e.g., where a bug arises. In this paper we introduce MemSight, a new approach to symbolic memory that reduces the need for concretization, hence offering the opportunity for broader state explorations and more precise pointer reasoning. Rather than mapping address instances to data as previous tools do, our technique maps symbolic address expressions to data, maintaining the possible alternative states resulting from the memory referenced by a symbolic address in a compact, implicit form. A preliminary experimental investigation on prominent benchmarks from the DARPA Cyber Grand Challenge shows that MemSight enables the exploration of states unreachable by previous techniques.
2017
32nd IEEE/ACM International Conference on Automated Software Engineering
Symbolic execution; testing; computer security
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Rethinking Pointer Reasoning in Symbolic Execution / Coppa, Emilio; D'Elia, Daniele Cono; Demetrescu, Camil. - STAMPA. - (2017), pp. 613-618. (Intervento presentato al convegno 32nd IEEE/ACM International Conference on Automated Software Engineering tenutosi a Urbana, Illinois, USA nel 30 October 2017 through 3 November 2017) [10.1109/ASE.2017.8115671].
File allegati a questo prodotto
File Dimensione Formato  
Coppa_Preprint-Rethinking_2017.pdf

accesso aperto

Tipologia: Documento in Pre-print (manoscritto inviato all'editore, precedente alla peer review)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 480.99 kB
Formato Adobe PDF
480.99 kB Adobe PDF
Coppa_Rethinking_2017.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 325.77 kB
Formato Adobe PDF
325.77 kB 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/1072937
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 18
  • ???jsp.display-item.citation.isi??? 13
social impact