HEAPHOPPER Bringing Bounded Model Checking to Heap Implementation Security

Abstract

堆元数据攻击已成为攻击者利用内存损坏漏洞的主要方式之一。虽然堆实现开发人员已经引入了缓解来防止和检测损坏，但攻击者仍然可以解决这些问题。在某种程度上，这是因为这些缓解是在没有原则基础的情况下创建和评估的，因此在许多情况下会导致堆元数据防御的复杂，低效和无效尝试。在本文中，我们提出了HEAPHOPPER，一种基于模型检查和符号执行的自动化方法，用于分析存在内存损坏时堆实现的可利用性。使用HEAPHOPPER，我们能够对不同的，广泛使用的堆实现进行系统分析，找到它们中令人惊讶的弱点。例如，我们的结果显示了ptmalloc中新引入的缓存机制（大多数Linux发行版使用的堆分配器实现）如何显著削弱其安全性。此外，HEAPHOPPER指导我们实施和评估对ptmalloc安全性的改进，用有效防御替代最近无效的缓解特定形式的堆元数据损坏的尝试。

1. 简介

作者通过使用符号执行技术，自动化分析堆分配器，根据配置文件定义的情况可以自动生成不同exploitation primitive 的POC

2. 背景

当程序逻辑存在漏洞时可以攻击堆分配器拿到程序控制权。为了缓解这些攻击，各大堆分配器都在内部进行了安全检查，然而并没有一个标准能评估加入一个补丁是否能缓解攻击。

以glibc的补丁为例

 /* Take a chunk off a bin list */
 #define unlink(AV, P, BK, FD) {                                            \
+    if (__builtin_expect (chunksize(P) != prev_size (next_chunk(P)), 0))      \
+      malloc_printerr (check_action, "corrupted size vs. prev_size", P, AV);  \
     FD = P->fd;                                                                      \
     BK = P->bk;                                                                      \
     if (__builtin_expect (FD->bk != P || BK->fd != P, 0))

补丁作者加入了一个对size的检查，然而这可以被轻松的绕过，具体利用见

poison_null_byte.c

因此作者通过符号执行技术对堆的交互进行了建模，从而可以自动化的评估堆分配器在特定情况下达到exploitation primitive的条件。

3. 生成堆交互模型

3.1 堆事务

作者将会修改堆的状态的操作定义为事务，对堆的交互分为两种：直接交互和间接交互

直接交互指分配器功能，如malloc，free

间接交互指修改分配的内存区域，比如overflow

malloc(M)

HEAPHOPPER 通过传递一个符号化变量对malloc申请的大小进行建模。

一个不可约束的值可能会导致路径爆炸和约束复杂，因此将大小设置为了一个具体的范围，因此符号执行单元将会使用symbolic-but-constrained 变量作为传递给malloc的参数。

通常根据堆分配器不同的执行路径来确定大小，作者开发了一个工具根据libc的执行路径来确定大小选择（然而并没有看见这个工具，源码里面也有提及）。

free(F)

如果之前执行过多个malloc事务，HEAPHOPPER将会生成一个不同的序列将其中的每一个作为free事务的参数

overflow(O)

在模型中，一个overflow代表一个和堆的间接的交互。作者通过在malloc出的chunk的末尾插入符号内存来实现overflow。和free事务类似，HEAPHOPPER将会为先前分配的chunk创建一个不同的序列作为overflow的目标。和malloc同样的原因，需要限制溢出的长度。在这将会把overflow的大小作为symbolic-but-constrained 处理。HEAPHOPPER 还支持根据不同的场景将overflow的字节设定为特定的范围。

use-after-free (UAF)

我们通过将符号内存写入已经free的chunk作为UAF事务。和之前的事务相似，HEAPHOPPER需要为之前free过的chunk创建一个不同的序列，将有限的字节的数据写到内存中。

double-free (DF)

double-free被建模为对之前释放过的内存执行free

fake-free (FF)

fake-free是释放一个假的，攻击者自定义的chunk。它被建模为free一个完全符号化的内存区域。这个符号化区域的大小必须有个限制。如果可能的话，符号执行单元将会自动确定符号区域的值能通过堆分配器的检查。

堆交互模型

HEAPHOPPER 将结合之前描述的堆事务生成一个交互列表，每个交互对应着堆模型的一条路径。HEAPHOPPER 通过创建所有可能的事务序列的排列来生成交互列表。

在这一步主要关注如何减少生成的事务序列而不丢失会导致产生exploitation primitives 的事务序列。因此，我们假设至少一次对堆进行了误操作（直接或间接），并且假设对堆的良性使用不会产生任何问题。此外，还排除了只有一个间接交互作为事务序列结束的情况，因为间接交互无法修改堆本身，修改堆本身至少需要一个直接交互。两个会对同一区域放置符号内存的的事务之间必须有影响这片内存的事务。

4 模型检测

4.1 识别安全违规行为

Overlapping Allocation (OA)

HEAPHOPPER 使用 SMT求解程序去判断如下条件是否为真

∃B : ((A ≤ B)∧(A+sizeof(A) > B))∨((A ≥ B)∧(B+sizeof(B) > A))

A为申请的内存，B为已申请的内存

Non-Heap Allocation (NHA)

提前记录堆分配器使用brk和mmap返回的地址，从而确定堆的范围

Arbitrary Write (AW and AWC)

在调用malloc，free时通过检测符号内存区域是否有写入来判断是否有AW或AWC。具体来说,我们查询约束求解器检查是否可以指定的写入特定的内存区域。

5.局限性

5.1 模型限制

当前情况下需要手动指定攻击者可以执行的事务。HEAPHOPPER无法对可能发生但是HEAPHOPPER中没有实现的攻击场景进行推理。之前为了减少符号执行样本的数量加入了一些限制条件，这可能会导致HEAPHOPPER错过一些利用。其次一些攻击需要执行很多事务才能把堆设置为理想的状态