Symbolic execution is a popular software testing technique that can help developers identify complex bugs in real-world applications. Unfortunately, symbolic execution may struggle at analyzing programs containing memory-intensive operations, such as memcpy and memset, whenever these operations are carried out over memory blocks whose size or address is symbolic, i.e., input-dependent. In this paper, we devise MInt, a memory model for symbolic execution that can support reasoning over such operations. The key new idea behind our proposal is to make the memory model aware of these memory-intensive operations, deferring any symbolic reasoning on their effects to the time where the program actually manipulates the symbolic data affected by these operations. We show that a preliminary implementation of MInt based on the symbolic framework angr can effectively analyze applications taken from the DARPA Cyber Grand Challenge.

Handling Memory-Intensive Operations in Symbolic Execution / Borzacchiello, Luca; Coppa, Emilio; Demetrescu, Camil. - ISEC 2022: 15th Innovations in Software Engineering Conference, (2022), pp. - (15th Innovations in Software Engineering Conference (ISEC 2022), Gandhinagar, India, 23-25 febbraio 2022). [10.1145/3511430.3511453].

Handling Memory-Intensive Operations in Symbolic Execution

Emilio Coppa
;
2022

Abstract

Symbolic execution is a popular software testing technique that can help developers identify complex bugs in real-world applications. Unfortunately, symbolic execution may struggle at analyzing programs containing memory-intensive operations, such as memcpy and memset, whenever these operations are carried out over memory blocks whose size or address is symbolic, i.e., input-dependent. In this paper, we devise MInt, a memory model for symbolic execution that can support reasoning over such operations. The key new idea behind our proposal is to make the memory model aware of these memory-intensive operations, deferring any symbolic reasoning on their effects to the time where the program actually manipulates the symbolic data affected by these operations. We show that a preliminary implementation of MInt based on the symbolic framework angr can effectively analyze applications taken from the DARPA Cyber Grand Challenge.
2022
9781450396189
symbolic execution, software testing
File in questo prodotto:
File Dimensione Formato  
Borzacchiello_Handling_2022.pdf

Solo gestori archivio

Tipologia: Versione dell'editore
Licenza: Tutti i diritti riservati
Dimensione 582.83 kB
Formato Adobe PDF
582.83 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/236304
Citazioni
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
  • OpenAlex ND
social impact