heaphopper: bounded model checking framework for Heap-implementations

HeapHopper is a bounded model checking framework for Heap-implementations.

HEAPHOPPER’s goal is to evaluate the exploitability of an allocator in the presence of memory corruption vulnerabilities
in the application using the allocator. Specifically, it detects if and how different heap-metadata corruption flaws can be
exploited in a given heap implementation to grant an attacker exploitation primitives. HEAPHOPPER works by analyzing
the compiled library implementing the heap allocation and deallocation functions (i.e., malloc and free).
Our choice of focusing on compiled binary code instead of source code was motivated by three main reasons. First of all,
using binary code allows us to analyze heap implementations for which the source code is not available. Secondly, the analysis of the source code may not be sufficient to realistically model the way in which memory is handled, since different
compilers and compilation options may result in different memory layouts, influencing the exact way in which a bug
corrupts memory. Additionally, for the problem we want to solve, the loss of semantic information induced by code compilation is not significant, since the only semantic information that our analysis needs is the location of the malloc
and free functions.
The input of HEAPHOPPER is a compiled binary library (in the format of a shared object file) implementing a heap and a configuration file specifying:

• List of transactions: A list of operations that an attacker is allowed to perform, such as malloc, free, buffer overflows, use-after-free, etc. For some of the transactions, further details can be specified, as we will explain in Section 4.1.
  
• Bound: The maximum number of transactions that an attacker can perform.
  
• List of security properties: A list of invalid states in which the attacker has reached the ability to perform specific
  exploitation primitives.
  

HEAPHOPPER works by automatically finding sequences of transactions that make the model of the analyzed heap implementation reach states where specific security properties are violated.

Install && Tutorial

Copyright (c) 2018, Moritz Eckert, Ruoyu Wang, Yan Shoshitaishvili, Arizona State University; Christopher Kruegel and Giovanni Vigna, Santa Barbara