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.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.