Skip to content
MemSight: Rethinking Pointer Reasoning in Symbolic Execution (ASE 2017)
Python Shell Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


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.

  • main script, line-by-line exploration
  • main script, non line-by-line exploration
  • executor/: common code to perform exploration
  • executor/ parser for executor config
  • memory/: some memory implememtations and their dependencies (data structures)
  • memory/ a wrapper around angr symbolic memory
  • memory/ memsight, an implementation of a fully symbolic memory (see: pseudocode)
  • other useful stuff
  • pitree/: page interval tree implementation
  • tests/: testing binaries


This code works with angr See build/

The docker container available on DockerHub contains an older version of MemSight that is based on angr 5.6.x (ASE paper).

How to run and can be used to run angr on a metabinary.

Line-by-line symbolic execution can be started with:

python <path-to-metabinary>

Or (non line-by-line exploration):

python <path-to-metabinary>

The implementation of the symbolic memory can be selected by adding a parameter when calling or For instance:

 python <id> <path-to-metabinary>

Where id can be:

  • 0:
  • 1: (memsight)

MetaBinary configuration

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
You can’t perform that action at this time.