HeapHopper: Bringing Bounded Model Checking to Heap Implementation Security
HeapHopper: Bringing Bounded Model Checking to Heap Implementation Security
复制标题
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Moritz Eckert;Antonio Bianchi;Ruoyu Wang;Yan Shoshitaishvili;Christopher Krügel;Giovanni Vigna
中科院分区：
文献类型：
--
作者：
Moritz Eckert;Antonio Bianchi;Ruoyu Wang;Yan Shoshitaishvili;Christopher Krügel;Giovanni Vigna
堆元数据攻击已成为攻击者利用内存腐败漏洞的主要方式之一。尽管堆的实施者已经引入了缓解和检测腐败的缓解，但攻击者仍然有可能围绕他们进行工作。在某种程度上，这是因为这些缓解措施是在没有原则基础的情况下创建和评估的，因此在许多情况下，对堆元数据的防御量进行了复杂，效率低下且无效的尝试。在本文中，我们提出了基于模型检查和符号执行的自动化方法，以分析在存在内存损坏的情况下堆实现的可剥削性。使用Hephopper，我们能够对不同，广泛使用的堆实现进行系统分析，从而发现了令人惊讶的弱点。例如，我们的结果表明，新近引入的ptmalloc（大多数Linux分布使用的堆分配器实现）如何显着削弱其安全性。此外，Hephopper指导我们实施和评估PTMALLOC安全性的改进，取代了最近尝试减轻特定形式的堆元数据腐败的尝试，并具有有效的辩护。
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.