利用Binary Ninja进行漏洞建模

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

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

回顾2014：寻找Heartbleed漏洞

Heartbleed是OpenSSL 1.0.1至1.0.1f中的一个远程信息泄露漏洞，允许攻击者发送特制的TLS心跳消息，诱使服务返回最多64KB的未初始化数据，可能包含敏感信息如私钥或个人数据。漏洞原因是OpenSSL使用攻击者消息中的字段作为malloc和memcpy调用的尺寸参数，而未验证该尺寸是否小于或等于要读取的数据大小。

修复版本1.0.1g添加了检查，确保memcpy不会溢出到其他数据。

用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]

我们可以将汇编指令建模为代数语句。例如，以下汇编代码：

1
2
3
4
5
6
7
8


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

可以建模为方程组：

1
2
3


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

使用Z3的BitVec类型（32位向量）可以处理整数溢出：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


>>> 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
>>> s.model()
[ebx = 2147483640, eax = 2147483648]

中级中间语言（MLIL）

MLIL在LLIL之上添加了另一层抽象，抽象了栈，将栈访问和寄存器访问都表示为变量。此外，MLIL在映射LLIL时消除了未引用的内存存储。MLIL还引入了类型系统，Binary Ninja启发式推断类型，用户可手动覆盖。

MLIL结构上类似LLIL，都是表达式树，但操作不同。MLIL没有LLIL_PUSH和LLIL_POP操作，而是使用MLIL_VAR和MLIL_SET_VAR。MLIL还支持结构操作，如MLIL_VAR_FIELD和MLIL_STORE_STRUCT。

MLIL接近反编译代码，使其非常适合翻译到Z3。

MLIL和API

在Binary Ninja API中处理MLIL与处理LLIL类似，但有一些区别。MLIL可以通过Function类的medium_level_il属性访问，但没有对应的get_low_level_il_at方法。要访问特定指令的MLIL，必须先查询LLIL。

MediumLevelILInstruction类引入了新便利属性，如vars_read和vars_written，简化了查询指令使用的变量列表。例如：

1
2
3
4


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

value和possible_values属性使用数据流分析计算MLIL表达式的值。

静态单赋值（SSA）形式

SSA形式是程序的一种表示，其中每个变量只定义一次。如果变量被赋予新值，则定义该变量的新“版本”。SSA还引入了Φ函数，表示控制流路径依赖的变量值。

在Binary Ninja中，SSA形式可通过API的ssa_form属性访问。MLIL_SET_VAR和MLIL_VAR操作被替换为MLIL_SET_VAR_SSA和MLIL_VAR_SSA，使用SSAVariable操作数。

SSA形式使得显式跟踪变量定义和使用变得容易，适合在Z3中建模变量赋值。

示例脚本：寻找Heartbleed

我们的方法类似于Andrew和Coverity的方法。字节交换操作是数据来自网络且用户控制的良好指标，因此我们使用Z3建模memcpy操作，确定尺寸参数是否是字节交换值。

步骤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数据流可以自行计算的尺寸参数：

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


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

    if possible_sizes.type != RegisterValueType.UndeterminedValue:
        return False

    model = ByteSwapModeler(size_param, bv.address_size)

    return model.is_byte_swap()

步骤3：跟踪尺寸依赖的变量

使用尺寸参数作为起点，通过静态向后切片跟踪代码，追踪尺寸参数依赖的所有变量。

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

遇到新的SSA变量时，识别负责定义该变量的指令，并将其添加到要访问的指令集中。然后生成Z3变量表示该SSA变量，并查询Binary Ninja的范围值分析，看该变量是否被约束为单个字节。

步骤5：识别尺寸参数的约束

确保在通向memcpy的执行路径上没有约束尺寸值的限制。检查branch_dependence属性，确定是否有基于字节交换中字节的决策。

步骤6：求解模型

如果尺寸未约束且依赖于字节变量，向Z3求解器添加最终方程，确保尺寸参数仅由先前识别的字节显式构造，并且尺寸参数的反向等于反向字节。

步骤7：发现漏洞

脚本在易受攻击的OpenSSL 1.0.1f上成功识别Heartbleed函数，在修复版本1.0.1g上不再标记。

结论

本文介绍了Heartbleed漏洞如何导致OpenSSL中的重大信息泄露错误，以及Binary Ninja的MLIL和SSA形式如何无缝转换为Z3等约束求解器。通过结合这些技术，可以准确建模二进制文件中的漏洞。

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

现在您知道如何利用IL进行漏洞分析，加入Binary Ninja Slack社区分享您自己的工具。如果您想了解更多关于BNIL、SSA形式和其他好东西，不要错过Infiltrate 2018的Binary Ninja研讨会。

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

[2] 目前这仅成立，因为Binary Ninja的数据流不计算不同值范围的联合，例如使用按位或连接两个字节（如字节交换中发生）。我相信这是速度的设计权衡。如果Vector 35实现了完整的代数求解器，这可能会改变，需要新的启发式方法。

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

页面内容 2014式黑客：寻找Heartbleed！用Z3将二进制代码建模为方程中级中间语言 MLIL结构 MLIL和API 静态单赋值（SSA）形式 Binary Ninja中的SSA形式示例脚本：寻找Heartbleed 步骤1：找到“接收点” 步骤2：消除已知非易受攻击的接收点步骤3：跟踪尺寸依赖的变量步骤4：识别可能是字节交换一部分的变量步骤5：识别尺寸参数的约束步骤6：求解模型步骤7：发现漏洞结论最近文章非传统创新者奖学金劫持您的PajaMAS中的多代理系统我们构建了MCP一直需要的安全层利用废弃硬件中的零日漏洞 Inside EthCC[8]：成为智能合约审计员 © 2025 Trail of Bits. 使用Hugo和Mainroad主题生成。