Home » Publication » 14502

Dettaglio pubblicazione

2017, ASE 2017 - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, Pages 613-618

Rethinking Pointer Reasoning in Symbolic Execution (04b Atto di convegno in volume)

Coppa Emilio, D'Elia Daniele Cono, Demetrescu Camil

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.
ISBN: 978-153862684-9; 978-1-5386-3976-4
Gruppo di ricerca: Cybersecurity
© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma