HEAPHOPPER: Bringing bounded model CheckingtoHeap implementation security

Heap metadata attacks have become one of the primary ways in which attackers exploit memory corruption vulnerabilities. While heap implementation developers have introduced miti-gations to prevent and detect corruption, it isstill possible for attackers to work around them. In part, this is because these mitigations are created and evaluated without aprincipled foundation, resulting, in many cases, in complex, inefficient, and ineffective attemptsatheap metadata defenses. In this paper, we present HEAPHOPPER, anautomated approach, basedonmodel checking and symbolic execution, to analyze the exploitability of heap implementations in the presence of memory corruption. Using HEAPHOPPER, we were able to performa systematic analysis of different, widely used heap implementations, finding surprising weak-nessesinthem. Our results show, for instance, howa newly introduced caching mechanismin ptmalloc (the heap allocator implementation usedby most of the Linux distributions) significantly weakens its security. Moreover, HEAPHOPPER guidedus inimplementing and evaluating improvements to the security of ptmalloc, replacing an ineffective recent attempt at the mitigation of a specific form of heap metadata corruption withan effective defense.