This repository contains an implemenation of MemSight based on angr. The ideas behind MemSight have been presented in the paper "Rethinking Pointer Reasoning in Symbolic Execution" accepted at ASE 2017. A èreprint of the paper is available here.
explore.py: main script, line-by-line explorationrun.py: main script, non line-by-line explorationexecutor/: common code to perform explorationexecutor/executor_config.py: parser for executor configmemory/: some memory implememtations and their dependencies (data structures)memory/angr_symbolic_memory.py: a wrapper around angr symbolic memorymemory/range_fully_symbolic_memory.py: memsight, an implementation of a fully symbolic memory (see: pseudocode)utils.py: other useful stuffpitree/: page interval tree implementationtests/: testing binaries
This code works with angr 7.7.12.16. See build/install.sh.
The docker container available on DockerHub contains an older version of MemSight that is based on angr 5.6.x (ASE paper).
run.py and explore.py can be used to run angr on a metabinary.
Line-by-line symbolic execution can be started with:
python explore.py <path-to-metabinary>
Or (non line-by-line exploration):
python run.py <path-to-metabinary>
The implementation of the symbolic memory can be selected by adding a parameter when calling run.py or explore.py. For instance:
python explore.py <id> <path-to-metabinary>
Where id can be:
0:angr_symbolic_memory.py1:range_fully_symbolic_memory.py(memsight)
A metabinary is a: binary + executor configuration.
For each binary, a configuration script <binary>.py must exist. This script must define few python functions:
def start():
return <start_address>
def end():
return [<end_address>, ...]
def avoid():
return [<avoid_address>, ...]
def do_start(state):
# properly initialize the initial state
return stuff
def do_end(state, stuff):
# this is called when one of end targets is reached