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, ISEC 2022: 15th Innovations in Software Engineering Conference, Pages -
Handling Memory-Intensive Operations in Symbolic Execution (04b Atto di convegno in volume)
Borzacchiello Luca, Coppa Emilio, Demetrescu Camil