使用Binary Ninja进行漏洞建模：自动化发现Heartbleed漏洞

本文详细介绍了如何利用Binary Ninja的中级中间语言（MLIL）和静态单赋值（SSA）形式，结合Z3定理证明器对二进制代码进行漏洞建模，以自动化检测类似Heartbleed的内存拷贝漏洞。

使用Binary Ninja进行漏洞建模

这是关于Binary Ninja中间语言（BNIL）系列文章的第三部分。在之前的文章中，我演示了如何利用低级中间语言（LLIL）编写架构无关的插件来反虚拟化C++虚函数。自那时起，Binary Ninja添加了许多新功能，特别是中级中间语言（MLIL）和静态单赋值（SSA）形式。本文将讨论这两者，并展示一个有趣的应用：自动化漏洞发现。

许多静态分析器可以对源代码执行漏洞发现，但如果你只有二进制文件呢？我们如何建模漏洞并检查二进制文件是否易受攻击？简短答案：使用Binary Ninja的MLIL和SSA形式。它们使得构建和求解方程组变得容易，通过定理证明器将二进制文件像炼金术一样转化为漏洞！

让我们以2014年备受关注的Heartbleed漏洞为例，逐步讲解这个过程。

像2014年一样黑客：寻找Heartbleed！

Heartbleed是OpenSSL 1.0.1至1.0.1f中的一个远程信息泄露漏洞，允许攻击者向使用TLS的服务发送特制的TLS心跳消息。该消息会欺骗服务响应最多64KB的未初始化数据，可能包含私密加密密钥或个人数据等敏感信息。这是因为OpenSSL使用攻击者消息中的字段作为malloc和memcpy调用的size参数，而没有先验证给定大小是否小于或等于要读取的数据大小。

以下是OpenSSL 1.0.1f中易受攻击的代码片段，来自tls1_process_heartbeat：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

/* Read type and payload length first */
hbtype = *p++;
n2s(p, payload);
pl = p;

/* Skip some stuff... */

if (hbtype == TLS1_HB_REQUEST)
{
    unsigned char *buffer, *bp;
    int r;

    /* Allocate memory for the response, size is 1 bytes
     * message type, plus 2 bytes payload length, plus
     * payload, plus padding
     */
    buffer = OPENSSL_malloc(1 + 2 + payload + padding);
    bp = buffer;
    
    /* Enter response type, length and copy payload */
    *bp++ = TLS1_HB_RESPONSE;
    s2n(payload, bp);
    memcpy(bp, pl, payload);
    bp += payload;
    /* Random padding */
    RAND_pseudo_bytes(bp, padding);

    r = ssl3_write_bytes(s, TLS1_RT_HEARTBEAT, buffer, 3 + payload + padding);

查看代码，我们可以看到size参数（payload）直接来自用户控制的TLS心跳消息，从网络字节序转换为主机字节序（n2s），然后传递给OPENSSL_malloc和memcpy，没有验证。在这种情况下，当payload的值大于pl处的数据时，memcpy将从pl开始的缓冲区溢出，并开始读取紧随其后的数据，泄露不应泄露的数据。

1.0.1g中的修复非常简单：

1
2
3
4
5

hbtype = *p++;
n2s(p, payload);
if (1 + 2 + payload + 16 > s->s3->rrec.length)
    return 0; /* silently discard per RFC 6520 sec. 4 */
pl = p;

这个新检查确保memcpy不会溢出到不同的数据中。

回到2014年，Andrew写了一篇关于编写clang分析器插件来查找类似Heartbleed漏洞的博客。但clang分析器插件运行在源代码上；如果我们没有源代码，如何在二进制文件中找到相同的漏洞？一种方法：通过将MLIL变量表示为一组约束并用定理证明器求解来构建漏洞模型！

用Z3将二进制代码建模为方程

定理证明器允许我们构建方程组并：

  • 验证这些方程是否相互矛盾。
  • 找到使方程成立的值。

例如，如果我们有以下方程：

1
2

x + y = 8
2x + 3 = 7

定理证明器可以告诉我们：a) 这些方程存在解，意味着它们不相互矛盾，b) 这些方程的解是x = 2和y = 6。

在本练习中，我将使用Microsoft Research的Z3定理证明器。使用z3 Python库，上述示例将如下所示：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
>>> s.add(x + y == 8)
>>> s.add(2*x + 3 == 7)
>>> s.check()
sat
>>> s.model()
[x = 2, y = 6]

Z3告诉我们方程可以满足，并提供值来求解它们。我们可以将这种技术应用于建模漏洞。事实证明，汇编指令可以建模为代数语句。以下汇编片段：

1
2
3
4
5
6
7
8

lea eax, [ebx+8]
cmp eax, 0x20
jle allocate
int3
allocate:
push eax
call malloc
ret

当我们将此汇编提升到Binary Ninja的LLIL时，我们得到以下图：

图1：LLIL使得识别有符号比较条件变得容易

在这段代码中，eax取ebx的值，然后加8。如果该值高于0x20，则引发中断。但是，如果该值小于或等于0x20，则该值传递给malloc。我们可以使用LLIL的输出将其建模为一组方程，如果整数溢出不可能，则这些方程应该是不可满足的（例如，ebx的值永远不应大于0x20但eax小于或等于0x20），这将如下所示：

1
2
3

eax = ebx + 8
ebx > 0x20
eax <= 0x20

如果我们将这些方程插入Z3会发生什么？不完全是我们所希望的。

1
2
3
4
5
6
7
8

>>> eax = Int('eax')
>>> ebx = Int('ebx')
>>> s = Solver()
>>> s.add(eax == ebx + 8)
>>> s.add(ebx > 0x20)
>>> s.add(eax <= 0x20)
>>> s.check()
unsat

应该有一个整数溢出，但我们的方程是unsat。这是因为Int类型（或z3术语中的“sort”）表示所有整数集合中的一个数字，其范围为-∞到+∞，因此溢出是不可能的。相反，我们必须使用BitVec sort，将每个变量表示为32位的向量：

1
2
3
4
5
6
7
8

>>> eax = BitVec('eax', 32)
>>> ebx = BitVec('ebx', 32)
>>> s = Solver()
>>> s.add(eax == ebx + 8)
>>> s.add(ebx > 0x20)
>>> s.add(eax <= 0x20)
>>> s.check()
sat

这是我们期望的结果！有了这个结果，Z3告诉我们eax可能溢出并使用意外值调用malloc。再多几行，我们甚至可以看到满足这些方程的可能值：

1
2
3
4

>>> s.model()
[ebx = 2147483640, eax = 2147483648]
>>> hex(2147483640)
'0x7ffffff8'

这对于寄存器非常有效，可以轻松表示为离散的32位变量。为了表示内存访问，我们还需要Z3的Array sort，它可以建模内存区域。然而，栈变量驻留在内存中，更难用约束求解器建模。相反，如果我们能在模型中像对待寄存器一样对待栈变量呢？我们可以使用Binary Ninja的中级中间语言轻松做到这一点。

中级中间语言

正如LLIL抽象了本地反汇编，中级中间语言（MLIL）在LLIL之上添加了另一层抽象。LLIL抽象了标志和NOP指令，而MLIL抽象了栈，将栈访问和寄存器访问都呈现为变量。此外，在将LLIL映射到MLIL的过程中，识别并消除了未被引用的内存存储。这些过程可以在下面的示例中观察到。注意没有栈访问（即push或pop指令），并且var_8根本没有出现在MLIL中。

图2a：x86中的示例函数 图2b：示例函数的LLIL 图2c：示例函数的MLIL

你可能在MLIL中注意到的另一个特征是变量是类型化的。Binary Ninja最初启发式地推断这些类型，但用户以后可以通过手动分配覆盖这些类型。类型通过函数传播，并在确定函数签名时帮助通知分析。

MLIL结构

在结构上，MLIL和LLIL非常相似；两者都是表达式树，并共享许多相同的操作表达式类型（有关IL树结构的更多信息，请参阅我的第一篇博客文章）。然而，有几个明显的差异。显然，MLIL没有类似于LLIL_PUSH和LLIL_PUSH的操作，因为栈已被抽象。LLIL_REG、LLIL_SET_REG和其他基于寄存器的操作被替换为MLIL_VAR、MLIL_SET_VAR和类似操作。除此之外，由于类型化，MLIL还具有结构的概念；MLIL_VAR_FIELD和MLIL_STORE_STRUCT表达式描述了这些操作。

图3：MLIL中的类型可以生成非常干净的代码

有些操作对LLIL和MLIL都是常见的，尽管它们的操作数不同。LLIL_CALL操作有一个操作数：dest，调用的目标。相比之下，MLIL_CALL操作还指定了output操作数，标识哪些变量接收返回值，以及params操作数，它包含描述函数调用参数的MLIL表达式列表。用户特定的调用约定，或基于变量在过程间使用的自动化分析确定的调用约定，确定这些参数和返回值。这允许Binary Ninja识别诸如在x86 PIC二进制文件中ebx寄存器用作全局数据指针的情况，或使用自定义调用约定的情况。

将所有这一切放在一起，MLIL非常接近反编译的代码。这也使得MLIL非常适合转换为Z3，因为它抽象了寄存器和栈变量，使用Binary Ninja的API。

MLIL和API

在Binary Ninja API中使用MLIL与使用LLIL类似，尽管有一些显著差异。像LLIL一样，函数的MLIL可以直接通过Function类的medium_level_il属性访问，但没有相应的MLIL方法来get_low_level_il_at。为了直接访问特定指令的MLIL，用户必须首先查询LLIL。LowLevelILInstruction类现在有一个medium_level_il属性，可以检索其中级中间语言形式。作为一行Python代码，这将看起来像current_function.get_low_level_il_at(address).medium_level_il。重要的是要记住，这有时可能是None，因为LLIL指令可能在MLIL中完全优化掉。

MediumLevelILInstruction类引入了LowLevelILInstruction类中不可用的新便利属性。vars_read和vars_written属性使得查询指令使用的变量列表变得简单，而无需解析操作数。如果我们重新访问我第一篇博客文章中的旧指令lea eax, [edx+ecx*4]，等效的MLIL指令将类似于LLIL。事实上，乍一看似乎是相同的。

1
2

>>> current_function.medium_level_il[0]
<il: eax = ecx + (edx << 2)>

但是，如果我们仔细看，我们可以看到区别：

1
2

>>> current_function.medium_level_il[0].dest
<var int32_t* eax>

与LLIL不同，其中dest将是表示寄存器eax的ILRegister对象，这里的dest操作数是一个类型化的Variable对象，表示名为eax的变量作为int32_t指针。

还为MLIL引入了其他几个新属性和方法。如果我们想提取此表达式读取的变量，这将很简单：

1
2

>>> current_function.medium_level_il[0].vars_read
[<var int32_t* ecx>, <var int32_t edx>]

branch_dependence属性返回基本块的条件分支，当只有真或假分支支配时，这些分支支配指令的基本块。这对于确定指令明确依赖的决策很有用。

两个属性使用数据流分析来计算MLIL表达式的值：value可以高效地计算常量值，而possible_values使用计算成本更高的路径敏感数据流分析来计算指令可以导致的值范围和不相交集合。

图5：路径敏感数据流分析识别可以到达特定指令的所有具体数据值

有了这些功能，我们可以建模寄存器、栈变量和内存，但还有一个我们需要解决的障碍：变量经常被重新分配依赖于先前赋值值的值。例如，如果我们正在迭代指令并遇到类似以下内容：

1
2

mov eax, ebx
lea eax, [ecx+eax*4]

在创建我们的方程时，我们如何建模这种重新分配？我们不能只是将其建模为：

1
2

eax = ebx
eax = ecx + (eax * 4)

这可能导致各种不可满足性，因为约束纯粹表达关于方程组中变量的数学真理，根本没有时间元素。由于约束求解没有时间概念，我们需要找到某种方法来弥合这一差距，转换程序以有效消除时间概念。此外，我们需要能够高效地确定先前值eax的来源。拼图的最后一块是通过Binary Ninja API可用的另一个功能：SSA形式。

静态单赋值（SSA）形式

与中级中间语言的发布同时，Binary Ninja还为BNIL家族中的所有表示引入了静态单赋值（SSA）形式。SSA形式是一种程序表示，其中每个变量定义一次且仅一次。如果变量被分配了新值，则定义该变量的新“版本”。一个简单的例子如下：

1
2
3

a = 1
b = 2
a = a + b

在SSA形式中变为：

1
2
3

a1 = 1
b1 = 2
a2 = a1 + b1

SSA形式引入的另一个概念是phi函数（或Φ）。当变量的值依赖于程序控制流所采取的路径时，例如if语句或循环，Φ函数表示该变量可以采取的所有可能值。该变量的新版本被定义为该函数的结果。下面是一个更复杂（和具体）的例子，使用Φ函数：

1
2
3
4
5
6

def f(a):
    if a > 20:
        a = a * 2
    else:
        a = a + 5
    return a

在SSA形式中变为：

1
2
3
4
5
6
7

def f(a0):
    if a0 > 20:
        a1 = a0 * 2
    else:
        a2 = a0 + 5
    a3 = Φ(a1, a2)
    return a3

SSA使得在整个程序生命周期中显式跟踪变量的所有定义和使用变得容易，这正是我们在Z3中建模变量赋值所需要的。

Binary Ninja中的SSA形式

IL的SSA形式可以在Binary Ninja中查看，但默认不可用。为了查看它，你必须首先在首选项中选中“启用插件开发调试模式”框。如下所示的SSA形式并不是真正用于视觉消费的，因为它比正常的IL图更难阅读。相反，它主要用于API。

图6：MLIL函数（左）及其对应的SSA形式（右）

任何中间语言的SSA形式都可以通过API中的ssa_form属性访问。此属性存在于函数（例如LowLevelILFunction和MediumLevelILFunction）和指令（例如LowLevelILInstruction和MediumLevelILInstruction）对象中。在这种形式中，诸如MLIL_SET_VAR和MLIL_VAR的操作被替换为新操作，MLIL_SET_VAR_SSA和MLIL_VAR_SSA。这些操作使用SSAVariable操作数而不是Variable操作数。SSAVariable对象是其对应Variable的包装器，但添加了它在SSA形式中表示的Variable版本的信息。回到我们之前的重新分配示例，MLIL SSA形式将输出以下内容：

1
2

eax#1 = ebx#0
eax#2 = ecx#0 + (eax#1 << 2)

这解决了重用变量标识符的问题，但仍然存在定位变量使用和定义的问题。为此，我们可以分别使用MediumLevelILFunction.get_ssa_var_uses和MediumLevelILFunction.get_ssa_var_definition（这些方法也是LowLevelILFunction类的成员）。

现在我们的工具包已经完成，让我们深入实际在Binary Ninja中建模一个真实世界的漏洞！

示例脚本：寻找Heartbleed

我们的方法将与Andrew的以及Coverity在其关于该主题的文章中使用的方法非常相似。字节交换操作是数据来自网络并由用户控制的一个很好的指标，因此我们将使用Z3建模memcpy操作并确定size参数是否是字节交换的值。

图7：OpenSSL 1.0.1f中tls1_process_heartbeat易受攻击的memcpy的size参数的后向静态切片，在MLIL中

步骤1：找到我们的“接收器”

执行典型的源到接收器污点跟踪将耗时且昂贵，如前述文章所示。让我们反过来做；识别所有对memcpy函数的代码引用并检查它们。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

memcpy_refs = [
    (ref.function, ref.address)
    for ref in bv.get_code_refs(bv.symbols['_memcpy'].address)
]

dangerous_calls = []

for function, addr in memcpy_refs:
    call_instr = function.get_low_level_il_at(addr).medium_level_il
    if check_memcpy(call_instr.ssa_form):
        dangerous_calls.append((addr, call_instr.address))

步骤2：消除我们知道不易受攻击的接收器

在check_memcpy中，我们可以快速消除Binary Ninja的数据流可以自行计算的任何size参数，使用MediumLevelILInstruction.possible_values属性。我们将建模剩下的任何东西。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

def check_memcpy(memcpy_call):
    size_param = memcpy_call.params[2]

    if size_param.operation != MediumLevelILOperation.MLIL_VAR_SSA:
        return False

    possible_sizes = size_param.possible_values

    # Dataflow won't combine multiple possible values from
    # shifted bytes, so any value we care about will be
    # undetermined at this point. This might change in the future?
    if possible_sizes.type != RegisterValueType.UndeterminedValue:
        return False

    model = ByteSwapModeler(size_param, bv.address_size)

    return model.is_byte_swap()

步骤3：跟踪size依赖的变量

使用size参数作为起点，我们使用所谓的静态后向切片向后追踪代码，并跟踪size参数依赖的所有变量。

1
2
3
4
5
6
7
8
9

var_def = self.function.get_ssa_var_definition(self.var.src)

# Visit statements that our variable directly depends on
self.to_visit.append(var_def)

while self.to_visit:
    idx = self.to_visit.pop()
    if idx is not None:
        self.visit(self.function[idx])

visit方法接受一个MediumLevelILInstruction对象，并根据指令操作字段的值分派不同的方法。回顾BNIL是一种基于树的语言，访问者方法将递归调用指令操作数上的visit，直到到达树的终止节点。此时，它将为Z3模型生成一个

comments powered by Disqus
© 2020 - 2025 qife
使用 Hugo 构建
主题 Stack 由 Jimmy 设计
本站总访问量次 本站访客数人次