使用Binary Ninja进行反向污点分析：高效定位程序崩溃根源

本文详细介绍如何利用Binary Ninja的MLIL SSA功能实现反向污点分析，通过自动化脚本追踪系统调用故障的根本原因，大幅减少手动调试工作量。

使用Binary Ninja进行反向污点分析

背景

我们开源了一套静态分析工具KRFAnalysis，用于分析和分类系统调用（syscall）故障注入工具KRF的输出。现在，您可以轻松找出KRF导致程序崩溃的位置和原因。

在Trail of Bits的暑期实习期间，我致力于KRF项目——一个通过直接故障系统调用来引发崩溃的模糊测试工具。KRF效果显著，能大量生成核心转储文件。然而，由于单次运行可能包含数百个故障系统调用，确定具体是哪个故障系统调用导致崩溃十分困难。通过源代码或反汇编二进制文件手动追踪崩溃原因既繁琐又容易出错。

人工介入：传统调试方法

如何可靠地确定崩溃来源？首先，我们会查看堆栈跟踪以确定崩溃发生的位置。以下面这个易受攻击的示例程序为例：

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

#include <stdlib.h>

void fillBuffer(char *string, unsigned len) {
  for (unsigned i = 0; i < len; ++i) {
    string[i] = 'A'; // 如果string为NULL，无效写入会导致段错误
  }
}

int main() {
  char *str;
  str = (char *)malloc(16); // 如果malloc失败，str为NULL
  fillBuffer(str, 16); // 未检查malloc错误！
  free(str);
  return 0;
}

使用KRF测试该程序会引发故障。此时，我们可以轻松猜测崩溃原因：故障的brk或mmap导致malloc返回NULL，当fillBuffer尝试向NULL写入时产生段错误。但假设我们无法访问源代码，如何确定崩溃原因？

  1. 使用gdb查看核心转储的堆栈跟踪：

    1
2
3

    (gdb) bt
#0 0x00005555555546a8 in fillBuffer ()
#1 0x00005555555546e1 in main ()

  2. 查看进程的内存映射以定位二进制文件中的指令：

    1
2
3
4

    (gdb) info proc mappings
Mapped address spaces:
  Start Addr   End Addr       Size     Offset objfile
  0x555555554000 0x555555555000 0x1000    0x0 /vagrant/shouldve_gone_for_the_head

  3. 通过地址计算指令偏移量： 0x00005555555546a8 - 0x555555554000 + 0x0 = 0x6a8

在Binary Ninja中反汇编fillBuffer()函数，发现导致段错误的指令（红色高亮）将rax指向的字节设置为字符A的代码。因此，问题必然是rax的值无效。回溯发现，rax = rax + rdx，这两个寄存器分别设置为局部变量string和i。在指令0x68e处，string最初存储在rdi中，即函数的第一个参数。i初始化为零且仅递增，因此可忽略，因为它不可能被函数调用或参数污染。

引入MLIL静态单赋值

Binary Ninja可以将代码反编译为中级中间语言（MLIL），这是一种更易读的汇编形式。然后将其转换为静态单赋值（SSA）形式，其中每个变量仅被赋值一次。这非常有用，因为我们无需担心变量在其定义之外被修改。

例如，以下伪代码函数：

1
2
3
4
5
6

def f(a):
  if a < 5:
    a = a * 2
  else:
    a = a - 5
  return a

在SSA形式中变为：

1
2
3
4
5
6
7

def f(a0):
  if a0 < 5:
    a1 = a0 * 2
  else:
    a2 = a0 - 5
  a3 = Φ(a1, a2)  // 表示“a3是a1或a2”
  return a3

通过SSA MLIL重新分析fillBuffer，可以轻松追踪rax_2#4到rax_1#3 + rdx_1#2，然后追踪rax_1#3到string#1（即arg1）。同样，可以回溯i并发现其设置为0。再次确认fillBuffer的第一个参数是崩溃的根源。

查看main函数时，SSA MLIL的优势更加明显：它可以显示传递给fillBuffer的参数和malloc返回的值，使分析更加容易。通过追踪rdi#1的来源，再次发现malloc污染了fillBuffer的第一个参数，从而导致崩溃。

实现自动化分析

基于以上过程，编写算法并实现为代码：

  1. 创建一个空栈。
  2. 将崩溃指令压入栈中。
  3. 当栈不为空时：
  4. 从栈中弹出一条指令。
  5. 如果是MLIL函数调用指令：
  6. 该函数调用的返回值可能是崩溃的原因。
  7. 否则：
  8. 对于MLIL指令中使用的每个SSA变量：

  9.   如果未在此函数中赋值：

  10.     # 它是函数参数

  11.     需要向上追踪堆栈帧。

  12.     # 与发现arg1被污染后转到main相同

  13.  否则：

  14.    将分配SSA变量的指令添加到栈中。

使用Binary Ninja API在Python中实现该函数：

 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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

def checkFunction(self, inst_addr, bv):
  # 获取包含指令的函数MLILFunction对象
  func = bv.get_functions_containing(inst_addr)[0].medium_level_il

  # 获取inst_addr处指令的MLILInstruction对象
  inst = func[func.get_instruction_start(inst_addr)].ssa_form

  # 将MLILFunction转换为SSA形式
  func = func.ssa_form

  # 跟踪已查看的指令
  visited_instructions = set()

  # 感兴趣的变量
  var_stack = []

  # 将第一条指令使用的变量添加到栈中
  for v in inst.vars_read:
    var_stack.append(v)

  # 当栈中有元素时持续运行分析
  while len(var_stack) > 0:
    var = var_stack.pop()
    if var not in visited_instructions:
      visited_instructions.add(var)

    # 获取变量声明
    decl = func.get_ssa_var_definition(var)

    # 检查是否为参数
    if decl is None:
      print("Argument " + var.var.name + " tainted from function call")
      continue

    # 检查是否为函数调用
    if decl.operation == MediumLevelILOperation.MLIL_CALL_SSA:
      # 直接调用
      if decl.dest.value.is_constant:
        # 从地址获取被调用函数的MLILFunction对象
        func_called = bv.get_function_at(decl.dest.value.value)
        print("Tainted by call to", func_called.name, "(" + hex(decl.dest.value.value) + ")")
      else:
        # 间接调用
        print("Tainted by indirect call at instruction", hex(decl.address))
      continue

    # 如果不是参数或调用，将指令中使用的变量添加到栈中。常量被过滤掉
    for v in decl.vars_read:
      var_stack.append(v)

SSA的强大功能体现在vars_read和get_ssa_var_definition方法中。MLIL通过decl.operation == MediumLevelILOperation.MLIL_CALL_SSA轻松检测调用。

扩展脚本

可以在多个方面进行扩展：错误处理、边缘情况、自动分析堆栈跟踪中的上一帧、自动从堆栈跟踪中提取信息等。幸运的是，我已经通过一组Python脚本实现了部分功能。

  • python3 main.py binary coredump1 [coredump2] …：自动从核心转储中提取所需信息，然后将这些信息和二进制文件插入到tarball中，以便复制到其他计算机，包括堆栈跟踪中调用的库。
  • gdb.py：使用GDB Python API从每个核心转储中提取数据。由main.py调用，因此它们必须在同一目录中。
  • python3 analyze.py tarball.tar.gz：获取main.py输出的tarball，并自动对其中的每个核心转储运行反向污点分析，自动将污染的参数级联到下一帧。它使用krf.py运行分析，因此它们必须在同一目录中。
  • krf.py包含分析代码，是本文所写脚本的功能增强版本（需要Binary Ninja API）。

测试二进制文件：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

$ # Linux VM with KRF
$ python3 main.py shouldve_gone_for_the_head core
Produced tar archive krfanalysis-shouldve_gone_for_the_head.tar.gz in /vagrant

$ # Machine with Binary Ninja
$ python3 analyze.py krfanalysis-shouldve_gone_for_the_head.tar.gz
Analyzing binary shouldve_gone_for_the_head
Done
Analyzing crash krfanalysis-shouldve_gone_for_the_head/cores/core.json
Tainted by call to malloc (0x560)
All paths checked

结论

编写此分析脚本让我体会到Binary Ninja API的强大功能。其多功能性和自动分析能力令人惊叹，尤其是它直接作用于二进制文件，其中间语言易于使用和理解。

我还想提到LLVM，另一个用于静态分析的框架，其API与Binary Ninja非常相似。它比Binary Ninja有许多优势，包括更好地访问调试和类型信息、免费、更成熟的代码库以及对调用约定的始终完美分析。其缺点是需要源代码或要分析内容的LLVM IR。

KRFAnalysis存储库中提供了三个LLVM传递来运行静态分析：一个检测由于在使用前检查系统状态而导致的竞争条件（即检查时间、使用时间或TOC/TOU），另一个检测标准库调用中未检查的错误，第三个重新实现反向污点分析。

实习收获

我非常感谢Trail of Bits的所有人给予我这次实习机会。我获得了宝贵的技术经验，并有机会与Linux内核、FreeBSD内核和LLVM合作——这些代码库我曾认为是神秘的。

一些亮点：

  • 将KRF移植到FreeBSD
  • 添加了KRF按PID、GID、UID或是否打开特定文件来定位进程的能力
  • 编写了用于静态分析的LLVM传递
  • 上游化了LLVM更改
  • 学会了如何使用Binary Ninja及其API
  • 掌握了良好的编码实践
  • 对安全行业有了更深入的了解

我还遇到了一些了不起的人。特别感谢我的导师Will Woodruff（@8x5clPW2），他总是愿意讨论实现、想法或审查我的拉取请求。我迫不及待地想要将我在Trail of Bits学到的东西应用到未来的职业生涯中。

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