漏洞建模与Binary Ninja

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

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

让我们以过去备受关注的心脏出血漏洞（Heartbleed）为例，逐步了解这个过程。

像2014年一样黑客：让我们找到Heartbleed！

对于那些可能不记得或不熟悉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的中级中间语言（MLIL）轻松做到这一点。

中级中间语言（MLIL）

正如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识别诸如ebx寄存器在x86 PIC二进制文件中用作全局数据指针，或使用自定义调用约定等情况。

综上所述，MLIL非常接近反编译的代码。这也使得MLIL非常适合通过Binary Ninja的API转换为Z3，因为它抽象了寄存器和栈变量。

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属性，用于检索其MediumLevelILInstruction形式。作为一行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不同（在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）形式

与中级中间语言（MLIL）的发布相配合，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中查看，但默认情况下不可用。要查看它，您必须首先在首选项中选中“Enable plugin development debugging mode”框。如下所示的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：找到我们的“接收器”（sinks）

执行典型的从源到接收器的污点跟踪将非常耗时且昂贵，如前述文章所示。让我们反过来做；识别所有对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参数[2]，使用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参数作为起点，我们使用所谓的反向静态切片（static backwards slice）来向后追踪代码，并跟踪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对象，并根据指令的operation字段的值分派不同的方法。回顾一下，BNIL是一种基于树的语言，访问者方法将递归地调用指令操作数上的visit，直到到达树的终止节点。此时，它将为Z3模型生成一个变量或常量，该变量或常量将通过递归调用者传播回来，与第2部分中的vtable-navigator插件非常相似。

MLIL_ADD的访问者相当简单，递归生成其操作数，然后返回两者的和：

1
2
3
4
5
6

    def visit_MLIL_ADD(self, expr):
        left = self.visit(expr.left)
        right = self.visit(expr.right)

        if None not in (left, right):
            return left + right

步骤4：识别可能是字节交换一部分的变量

MLIL_VAR_SSA（描述SSAVariable的操作）是MLIL指令树的终止节点。当我们遇到一个新的SSA变量时，我们识别负责定义该变量的指令，并将其添加到我们要在向后切片时访问的指令集中。然后，我们生成一个Z3变量来表示我们模型中的这个SSAVariable。最后，我们查询Binary Ninja的范围值分析，看看这个变量是否被约束为单个字节（即在0 – 0xff范围内，起始偏移量是8的倍数）。如果是，我们继续在模型中约束此变量到该值范围。

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

    def visit_MLIL_VAR_SSA(self, expr):
        if expr.src not in self.visited:
            var_def = expr.function.get_ssa_var_definition(expr.src)
            if var_def is not None:
                self.to_visit.append(var_def)

        src = create_BitVec(expr.src, expr.size)

        value_range = identify_byte(expr, self.function)
        if value_range is not None:
            self.solver.add(
                Or(
                    src == 0,
                    And(src >= value_range.start, src <= value_range.end)
                )
            )

            self.byte_vars.add(expr.src)

        return src

我们访问的MLIL指令的父操作通常是MLIL_SET_VAR_SSA或MLIL_SET_VAR_PHI。在visit_MLIL_SET_VAR_SSA中，我们可以像往常一样递归地为src操作数生成模型，但MLIL_SET_VAR_PHI操作的src操作数是SSAVariable对象的列表，表示Φ函数的每个参数。我们将这些变量的定义站点添加到我们要访问的指令集中，然后为我们的模型编写一个表达式，说明dest == src0 || dest == src1 || … || dest == srcn：

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

        phi_values = []

        for var in expr.src:
            if var not in self.visited:
                var_def = self.function.get_ssa_var_definition(var)
                self.to_visit.append(var_def)

            src = create_BitVec(var, var.var.type.width)

            # ...

            phi_values.append(src)

        if phi_values:
            phi_expr = reduce(
                lambda i, j: Or(i, j), [dest == s for s in phi_values]
            )

            self.solver.add(phi_expr)

在visit_MLIL_SET_VAR_SSA和visit_MLIL_SET_VAR_PHI中，我们都跟踪被约束为单个字节的变量，以及它们被约束为哪个字节：

 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

        # If this value can never be larger than a byte,
        # then it must be one of the bytes in our swap.
        # Add it to a list to check later.
        if src is not None and not isinstance(src, (int, long)):
            value_range = identify_byte(expr.src, self.function)
            if value_range is not None:
                self.solver.add(
                    Or(
                        src == 0,
                        And(src >= value_range.start, src <= value_range.end)
                    )
                )

                self.byte_vars.add(*expr.src.vars_read)

                if self.byte_values.get(
                    (value_range.start, value_range.end)
                ) is None:
                    self.byte_values[
                        (value_range.start, value_range.end)
                    ] = simplify(Extract(
                                int(math.floor(math.log(value_range.end, 2))),
                                int(math.floor(math.log(value_range.start, 2))),
                                src
                            )
                    )

最后，一旦我们访问了变量的定义指令，我们将其标记为已访问，以便不会再次添加到to_visit中。

步骤5：识别size参数上的约束

一旦我们切片了size参数并定位了字节交换中可能使用的字节，我们需要确保在执行路径上 leading to the memcpy 没有任何约束会限制size的值。memcpy的MediumLevelILInstruction对象的branch_dependence属性标识了到达该指令所必需的强制控制流决策，以及必须采用哪个分支（真/假）。我们检查每个分支决策检查的变量，以及这些变量的依赖关系。如果基于我们确定在交换中的任何字节做出了决策，我们将假定此size参数受到约束并中止其分析。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

        for i, branch in self.var.branch_dependence.iteritems():
            for vr in self.function[i].vars_read:
                if vr in self.byte_vars:
                    raise ModelIsConstrained()
                vr_def = self.function.get_ssa_var_definition(vr)
                if vr_def is None:
                    continue
                for vr_vr in self.function[vr_def].vars_read:
                    if vr_vr in self.byte_vars:
                        raise ModelIsConstrained

步骤6：求解模型

如果size不受约束，并且我们发现size参数依赖于仅仅是字节的变量，我们需要向Z3求解器添加最后一个方程。为了识别字节交换，我们需要确保即使我们的size参数不受约束，size仍然仅由我们先前识别的字节显式构造。此外，我们还想确保size参数的反向等于识别的字节反向。但是，如果我们只是向模型添加一个具有这些属性的方程，它将不起作用。定理检查器只关心是否有任何值满足方程，而不是所有值，所以这带来了一个问题。

我们可以通过否定最终方程来克服这个问题。通过告诉定理求解器我们想要确保没有值满足否定并寻找unsat结果，我们可以找到满足原始（非否定）方程的所有值的size参数。所以如果我们在添加这个方程后我们的模型是不可满足的，那么我们已经找到了一个字节交换的size参数。这可能是一个错误！

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

           self.solver.add(
                Not(
                    And(
                        var == ZeroExt(
                            var.size() - len(ordering)*8,
                            Concat(*ordering)
                        ),
                        reverse_var == ZeroExt(
                            reverse_var.size() - reversed_ordering.size(),
                            reversed_ordering
                        )
                    )
                )
            )

            if self.solver.check() == unsat:
                return True

步骤7：查找错误

我在两个版本的OpenSSL上测试了我的脚本：首先是易受攻击的1.0.1f，然后是修复了漏洞的1.0.1g。我使用命令./Configure darwin-i386-cc在macOS上编译了两个版本以获得32位x86版本。当脚本在1.0.1f上运行时，我们得到以下结果：

图8. find_heartbleed.py成功识别1.0.1f中的两个易受攻击的Heartbleed函数。

然后，如果我们在打了补丁的版本1.0.1g上运行脚本：

图9. 易受攻击的函数在打了补丁的1.0.1g中不再被识别！

正如我们所看到的，消除了Heartbleed漏洞的打了补丁的版本不再被我们的模型标记！

结论

我现在已经介绍了Heartbleed缺陷如何导致OpenSSL中的重大信息泄露错误，以及Binary Ninja的中级中间语言（MLIL）和SSA形式如何无缝转换为像Z3这样的约束求解器。总而言之，我演示了如何准确地在二进制文件中建模诸如Heartbleed之类的漏洞。您可以在此处找到完整的脚本。

当然，这样的静态模型只能到此为止。对于更复杂的程序建模，例如过程间分析和循环，请探索使用符号执行引擎（如我们的开源工具Manticore）进行约束求解。

既然您知道如何利用IL进行漏洞分析，请加入Binary Ninja Slack并与社区分享您自己的工具，如果您有兴趣了解更多关于BNIL、SSA形式和其他好东西的信息。

最后，不要错过2018年Infiltrate的Binary Ninja研讨会。我将与Vector 35团队一起，帮助回答问题！

[1] 在第2部分之后，Jordan告诉我Rusty说过，“Josh真的可以使用SSA形式。”既然SSA形式现在已经可用，我在此处添加了文章脚本的重构和更简洁的版本！

[2] 目前这仅成立，因为Binary Ninja的数据流不计算不同值范围的并集，例如使用按位或将两个字节连接起来，就像在字节交换中发生的那样。我相信这是为了速度而做的设计权衡。如果Vector 35 ever implements a full algebraic solver，这可能会改变，并且将需要新的启发式方法。