Symbolic memory

[Google Scholar]

Notes: symbolic execution, angr verifier
Papers: coppa:ase:2017

In symbolic execution tools, there is a choice about what to do with symbolic memory addresses. They can be concretized on all accesses, concretized on writes but not reads, on reads but not writes or kept symbolic. Additionally, they can be concretized if they fall outside a certain range angr verifier.

coppa:ase:2017 describes a fully symbolic approach and compares against other tools that use more concretization.

It is not clear whether this is worse for binary analysis tools since they have less type information to work with?

angr verifier

  • Rethinking pointer reasoning in symbolic execution [coppa:ase:2017]
  • A segmented memory model for symbolic execution [kapus:fse:2019]
  • Practical, low-effort equivalence verification of real code [ramos:cav:2011]