反向污点分析原理

在Trail of Bits暑期实习期间，我开发了KRFAnalysis工具集，用于分析系统调用故障注入工具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);
  fillBuffer(str, 16); // 未检查malloc是否失败
  free(str);
  return 0;
}

通过gdb分析核心转储：

1
2
3


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

逆向分析显示malloc的返回值未经检查就直接传递给fillBuffer，导致写入NULL指针时崩溃。

MLIL SSA形式分析

Binary Ninja的Medium Level IL(MLIL)转换为Static Single Assignment(SSA)形式后，变量追踪变得简单：

每个变量只被赋值一次
函数参数和返回值关系清晰可见
通过vars_read和get_ssa_var_definition方法可自动追踪数据流

自动化分析算法

创建空栈
将崩溃指令压入栈
当栈不为空时：
- 弹出指令
- 如果是函数调用：标记返回值可能为崩溃原因
- 否则：追踪所有SSA变量的定义

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)

工具集扩展

完整的KRFAnalysis包含三个组件：

main.py - 从核心转储提取信息并打包
analyze.py - 自动运行反向污点分析
krf.py - 核心分析逻辑（基于Binary Ninja API）

使用示例：

1
2
3
4
5


# 在KRF虚拟机
python3 main.py binary core

# 在Binary Ninja环境
python3 analyze.py analysis_package.tar.gz

结论

Binary Ninja API提供了强大的二进制分析能力，其SSA形式的中间语言显著简化了逆向分析过程。虽然LLVM框架在源码分析方面有优势，但Binary Ninja可以直接处理二进制文件，使其成为无源码情况下的理想选择。

工具集已开源，包含三个LLVM静态分析pass：

检测竞态条件(TOCTOU)
检测未检查的标准库调用错误
反向污点分析的LLVM实现

使用Binary Ninja进行反向污点分析 - 追踪程序崩溃根源

本文详细介绍如何利用Binary Ninja的API实现反向污点分析算法，自动追踪系统调用故障注入工具KRF产生的崩溃根源。通过SSA形式的中间语言分析，显著减少人工逆向工作量。