HeapHopper: Bringing Bounded Model Checking to Heap Implementation Security


Moritz Eckert, University of California, Santa Barbara; Antonio Bianchi, University of California, Santa Barbara / The University of Iowa; Ruoyu Wang, University of California, Santa Barbara / Arizona State University; Yan Shoshitaishvili, Arizona State University; Christopher Kruegel and Giovanni Vigna, University of California, Santa Barbara


Heap metadata attacks have become one of the primary ways in which attackers exploit memory corruption vulnerabilities. While heap implementation developers have introduced mitigations to prevent and detect corruption, it is still possible for attackers to work around them. 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.

In this paper, we present HeapHopper, an automated approach, based on model checking and symbolic execution, to analyze the exploitability of heap implementations in the presence of memory corruption. Using HeapHopper, we were able to perform a systematic analysis of different, widely used heap implementations, finding surprising weaknesses in them. Our results show, for instance, how a newly introduced caching mechanism in ptmalloc (the heap allocator implementation used by most of the Linux distributions) significantly weakens its security. Moreover, HeapHopper guided us in implementing and evaluating improvements to the security of ptmalloc, replacing an ineffective recent attempt at the mitigation of a specific form of heap metadata corruption with an effective defense.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {217488,
author = {Moritz Eckert and Antonio Bianchi and Ruoyu Wang and Yan Shoshitaishvili and Christopher Kruegel and Giovanni Vigna},
title = {{HeapHopper}: Bringing Bounded Model Checking to Heap Implementation Security},
booktitle = {27th USENIX Security Symposium (USENIX Security 18)},
year = {2018},
isbn = {978-1-931971-46-1},
address = {Baltimore, MD},
pages = {99--116},
url = {https://www.usenix.org/conference/usenixsecurity18/presentation/eckert},
publisher = {USENIX Association},
month = aug,

Presentation Video 

Presentation Audio