# HEAPHOPPER: Bringing Bounded Model Checking to Heap Implementation Security

> Moritz Eckert1, Antonio Bianchi1,2, Ruoyu Wang1,3, Yan Shoshitaishvili3, Christopher Kruegel1, and Giovanni Vigna1
1University of California, Santa Barbara 2The University of Iowa 3Arizona State University
{m.eckert,chris,giovanni}@cs.ucsb.edu, [e-mail],{fishw,yans}@asu.edu

## Key Point

* focus on compiled binary code instead of source code
* try all possible permutations of transaction sequences
* symbolic execution to find violation

## Abstract

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 deallocationfunctions


## Contribution

* This paper develops a novel approach to performing bounded model checking of heap implementations to evaluate their security in the presence of metadata corruption.
* This paper demonstrates their tool’s capabilities by analyzing different versions of different heap implementations, showcasing both security improvements and security issues.
* This paper utilized the tool to analyze high-profile patches and changesinthe glibc allocator, resulting in improved patches that are awaiting final sign-off and merge into glibc.

## Analysis

### What is the problem solved?

Heap implementation developers have introduced miti- gations to prevent and detect corruption, it is still possible for attackers to work around them. And it is hard for developer to manually check if their implementation is secure or not. In part, this is because these mitigations are created and evaluated without a principled foundation, resulting, in many cases, in complex, inefficient, and ineffective attempts at heap metadata defenses.

### What is proposed? How does it work?

HeapHopper is propsed in this paper. It aims to evaluate an update or a patch for heap allocator. It gives a principled approach to verifying the behavior of heap implementations in the presence of software vulnerabilities.

**Work Flow**

graph LR

    transactions_permutations --> symbolic_execution_detector --> poc_generator

This paper firstly defined several transections:

* Usages
* malloc
* free
* Mis-Usages
* overflow
* use-after-free
* double-free
* fake-free

Then it tries to list all possible permutations of transections mentioned above. There are some constraints like: the maximum transection number, must contain one mis-usage transections and so forth. Then after this, it compiles this transections into binaries and symbolic execute them with the allocator library to detect if any violation states below is shown:
* overlapping allocation
* non-heap allocation
* arbitrary write

Finally, it generates corresponding POCs.

## Strength

* This paper presented HEAPHOPPER, a novel, fully automated tool, based on model checking and symbolic execution, to analyze, in a principled way, the exploitability of heap implementations, in the presence of memory corruption.
* Using HEAPHOPPER, we were able to identify both known and previously unknown weaknesses in the security of dif- ferent heap allocators.

## Limitation

* need to manually specify the types of transactions that an attacker can perform.
* we cannot reason about transactions that could be possible in specific attack scenarios, but were not imple- mented in HEAPHOPPER
* the bounds we set in our model may cause HEAPHOPPER to miss other exploita- tion opportunities.

* amount of transactions: an increase of this amount will result in an exponential increase in the number of permutations. However, certain known attack techniques, such as the poisoned NULL byte, require a large amount of transac- tions until they reach a malicious state in the heap.

## Future Work

In this case, techniques to “cache” already-explored paths (or part of a path) within our model could be used to both speed-up the symbolic execution and lower the memory consumption.