使用Binary Ninja进行反向污点分析 - Trail of Bits博客

人类参与循环

如何可靠确定崩溃来源？首先查看堆栈追踪确定崩溃位置。以这个易受攻击的程序为例：

 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;
}

通过GDB分析核心转储堆栈追踪：

1
2
3


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

通过内存映射定位二进制指令位置：0x00005555555546a8 - 0x555555554000 + 0x0 = 0x6a8

在Binary Ninja中查看反汇编，发现fillBuffer()函数中rax寄存器包含无效值。追踪发现rax来自rdi（函数第一个参数），而rdi又来自malloc的返回值。

进入MLIL静态单赋值

Binary Ninja可将代码反编译为中级中间语言（MLIL），并转换为静态单赋值（SSA）形式。SSA形式中每个变量仅被赋值一次，极大简化分析过程。

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中可清晰追踪rax_2#4 → rax_1#3 + rdx_1#2 → string#1（即arg1），确认fillBuffer的第一个参数是崩溃根源。

最终阶段

将分析过程转化为算法：

创建空栈
将崩溃指令压入栈
当栈非空时：
弹出指令
如果是MLIL函数调用指令：

该函数返回值可能是崩溃原因

否则：

对MLIL指令中使用的每个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


def checkFunction(self, inst_addr, bv):
  func = bv.get_functions_containing(inst_addr)[0].medium_level_il
  inst = func[func.get_instruction_start(inst_addr)].ssa_form
  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:
        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)

扩展脚本

提供一组Python脚本自动化分析：

main.py: 从核心转储提取信息并打包
gdb.py: 使用GDB Python API提取数据
analyze.py: 对打包文件自动运行反向污点分析
krf.py: 包含增强版分析代码（需要Binary Ninja API）

使用示例：

1
2
3
4
5


# Linux VM with KRF
$ python3 main.py shouldve_gone_for_the_head core

# Machine with Binary Ninja  
$ python3 analyze.py krfanalysis-shouldve_gone_for_the_head.tar.gz

结论

Binary Ninja API功能强大，支持直接对二进制文件进行自动分析，其中间语言易于使用和理解。LLVM是另一个静态分析框架，具有更好的调试信息访问能力，但需要源代码或LLVM IR。

KRFAnalysis仓库提供三个LLVM pass：

检测由系统状态检查引起的竞争条件（TOC/TOU）
检测标准库调用的未检查错误
重新实现反向污点分析

我的暑期：值得付出的代价

在Trail of Bits实习期间获得了宝贵的技术经验，包括：

将KRF移植到FreeBSD
为KRF添加按PID、GID、UID或打开文件定位进程的功能
编写LLVM pass进行静态分析
学习使用Binary Ninja及其API
获得安全行业认知

特别感谢导师Will Woodruff（@8x5clPW2）的指导。