A segmented memory model for symbolic execution

Timotej Kapus, Cristian Cadar
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 18 March 2021

Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Tallinn, Estonia
Association for Computing Machinery
New York, NY, USA
Pages 774-784
Note(s): symbolic execution, KLEE verifier, symbolic memory
Papers: coppa:ase:2017

This paper provides a different solution to the problem in coppa:ase:2017: how to handle symbolic addresses during symbolic execution. Forking (the default behaviour of KLEE) every time the pointer target could refer to multiple objects (“multi-resolution”) causes a path explosion while treating the entire memory as a single flat object is inefficient.

Their solution is to use a pointer analysis to partition all objects/pointers into equivalence classes of objects that may alias. A separate segment with its own memory management (including its own free list) is created for each equivalence class and allocation is performed in the appropriate segment. They allow for possible bugs in the pointer analysis by performing a search in each segment: the performance benefit comes from the fact that only one will hit (in the absence of bugs).

They evaluate on the Apache Portable Runtime (a sort of portability middleware layer), GNU m4, GNU make and SQLite. The new model is (significantly?) slower than standard KLEE on benchmarks that do not suffer from multiresolution. An alternative model that (aggressively?) merges paths is competitive with segmented memory but it times out on some of the benchmarks. They evaluate the impact of pointer analysis precision – sometimes it matters.