A memoization extension for KLEE. With MoKlee, solver results can be re-used between executions and divergence detection ensures that re-executed paths are valid.

Overview

When symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. MoKlee can record an ongoing symbolic execution analysis to disk and selectively restore paths of interest later, making it possible to run symbolic execution indefinitely.

To be successful, our approach addresses several essential research challenges related to detecting divergences on re-execution, storing long-running executions efficiently, changing search heuristics during re-execution, and providing a global view of the stored execution. Our extensive evaluation of 93 Linux applications shows that our approach is practical, enabling these applications to run for days while continuing to explore new execution paths.

Artefact

The artefact page is available here.

Research Support

This research has received funding from the DSO National Laboratories, Singapore, and the EPSRC, UK through grants EP/R011605/1 and EP/N007166/1. This project has also received funding from European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 819141).

Publications