首页
社区
课程
招聘
问答 CTF 排行榜 知识库 工具下载 峰会 看雪商城 证书查询
  1. 社区
  2. 外文翻译
    3. 发新帖
[翻译]利用逆向分析框架 Angr 分析一个代码混淆的样本
发表于: 2021-6-26 22:36 14653

[翻译]利用逆向分析框架 Angr 分析一个代码混淆的样本

dig_grave 活跃值
2021-6-26 22:36
14653

原文链接：https://napongizero.github.io/blog/Defeating-Code-Obfuscation-with-Angr

一、介绍

1
首先我将简要介绍一下Angr，因为我认为知道我们的工具如何工作是很重要的一件事情。

二、符号执行 - 简要介绍

Angr是一个python模块的，我将使用它作为二进制分析的框架。它是采用动态和静态结合的方式来进行符号分析的工作。这种工作方式被叫做“导向性随机测试”，虽然如此，但是大家基本叫它符号执行/分析引擎。

什么是符号执行？

1
符号执行就是通过用“符号”值替换程序的输入值来模拟程序的执行。随着执行模拟的进行，每当处理输入时，执行程序的约束条件都会被添加到“符号”值中。 当遇到分支条件时，模拟分为两条路径：一条路径分支条件评估为真，另一条路径评估为假。

通俗的说，就是用符号去替换输入的值。用符号值执行程序会建立起约束的边界。
看下面的一个例子：

1
2
3
4
// Assume a & b are controlled by the user
if (a > b)
  a = a - b;
else b = b - a;


也就是说，左分支的约束是 a>b，而右分支的约束是 a<=b。

 

真实世界的程序肯定不会如此简单，代码分支深处的约束会变得非常大、非常快。为了解决这些限制，Angr使用了微软的定理证明器Z3。Z3检查约束是否可满足 (SAT)。假设某个分支有可满足的约束，我们可以要求Angr给出一个满足约束的输入的例子。

三、Angr - 基础使用

下面是一个Angr基础使用的用法示例。在下面的例子中，我们将会添加约束条件，并让Angr去执行它。
考虑下面的代码片段：

1
2
3
4
5
6
7
8
9
10
11
#include <stdio.h>
#include <stdlib.h>
 
void main(int argc, char *argv[]){
    int a=atoi(argv[1]);
    int b=atoi(argv[2]);
    if (10 > a && a > 5 && 10 > b && b > 1 && 2*b - a == 10)
    {
        printf("[+] Math is hard... but not 4 u! \n");
    }
}

我们将会使用Angr手工的加上约束条件，然后使用内置的求解器（solver）进行求解。这与我们通常使用Angr的方式不同，它只是在我们深入研究复杂案例之前展示一下的例子。

 

带上注释一步一步的用iPython命令，

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
# Importing angr
In [1]: import angr
 
# A wrapper for Z3. Claripy is used for constraint-solving.
In [2]: import claripy
 
# Loading the binary to angr.
In [3]: p = angr.Project('./a.out')
WARNING | 2021-05-24 17:54:05,450 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
 
# Constructs a state ready to execute at the binary's entry point.
In [4]: state = p.factory.entry_state()
 
# Create a bitvector symbol named "a" of length 32 bits
In [5]: a = state.solver.BVS("a", 32)
 
# Create a bitvector symbol named "b" of length 32 bits
In [6]: b = state.solver.BVS("b", 32)
 
''' Adding constraints manually '''
In [7]: state.solver.add(10>a)
Out[7]: [<Bool a_39_32 < 0xa>]
 
In [8]: state.solver.add(a>5)
Out[8]: [<Bool a_39_32 > 0x5>]
 
In [9]: state.solver.add(b>1)
Out[9]: [<Bool b_40_32 > 0x1>]
 
In [10]: state.solver.add(b<10)
Out[10]: [<Bool b_40_32 < 0xa>]
 
In [11]: state.solver.add(2*b - a == 10)
Out[11]: [<Bool 0x2 * b_40_32 - a_39_32 == 0xa>]
 
# Evaluates the value of "a" by taking the current constraints into consideration.
In [12]: state.solver.eval(a)
Out[12]: 6
 
# Evaluates the value of "b" by taking the current constraints into consideration.
In [13]: state.solver.eval(b)
Out[13]: 8

现在我们有了这些基础之后，让我们转到主要的事情上：

四、逆向混淆的二进制文件

我们使用的二进制文件是“DarkCTF2020”的“Jack”

文件分析

首先收集一些二进制文件的基础信息：

执行下文件，并且使用ltrace去trace写库函数。

 

这为我们提供了一些关于我们面对的问题的有用的信息。
看来问题是找到程序的key（可能不止一个）。
接下来，我决定在 Ghidra 中加载二进制文件，以便更好地了解发生了什么。

 

反编译主程序：

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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
bool main(void)
 
{
  uint uVar1;
  size_t sVar2;
  long in_FS_OFFSET;
  uint local_38;
  int local_34;
  int local_30;
  int local_2c;
  char local_28;
  char local_27;
  char local_26;
  char local_25;
  char local_24;
  char local_23;
  char local_22;
  char local_21;
  char local_20;
  char local_1f;
  char local_1e;
  char local_1d;
  char local_1c;
  char local_1b;
  char local_1a;
  char local_19;
  undefined local_18;
  long local_10;
 
  local_10 = *(long *)(in_FS_OFFSET + 0x28);
  puts("Enter your key: ");
  fgets(&local_28,0x11,stdin);
  local_18 = 0;
  sVar2 = strlen(&local_28);
  if (sVar2 != 0x10) {
    puts("Try Harder");
  }
  else {
    local_38 = local_25 * 0x1000000 + (int)local_28 + local_27 * 0x100 + local_26 * 0x10000;
    local_38 = local_38 ^ ((int)local_38 >> 3 & 0x20000000U) + local_38 * 0x20;
    local_38 = local_38 ^ local_38 << 7;
    local_38 = (local_38 >> 1 & 0xff) + local_38;
    local_38 = ((int)local_38 >> 3 & 0x20000000U) + local_38 * 0x20 ^ local_38;
    local_38 = local_38 ^ local_38 << 7;
    local_38 = local_38 + (local_38 >> 1 & 0xff);
    uVar1 = local_21 * 0x1000000 + (int)local_24 + local_23 * 0x100 + local_22 * 0x10000;
    uVar1 = uVar1 ^ ((int)uVar1 >> 3 & 0x20000000U) + uVar1 * 0x20;
    uVar1 = uVar1 ^ uVar1 << 7;
    uVar1 = (uVar1 >> 1 & 0xff) + uVar1;
    uVar1 = ((int)uVar1 >> 3 & 0x20000000U) + uVar1 * 0x20 ^ uVar1;
    uVar1 = uVar1 ^ uVar1 << 7;
    local_34 = uVar1 + (uVar1 >> 1 & 0xff);
    uVar1 = local_1d * 0x1000000 + (int)local_20 + local_1f * 0x100 + local_1e * 0x10000;
    uVar1 = uVar1 ^ ((int)uVar1 >> 3 & 0x20000000U) + uVar1 * 0x20;
    uVar1 = uVar1 ^ uVar1 << 7;
    uVar1 = (uVar1 >> 1 & 0xff) + uVar1;
    uVar1 = ((int)uVar1 >> 3 & 0x20000000U) + uVar1 * 0x20 ^ uVar1;
    uVar1 = uVar1 ^ uVar1 << 7;
    local_30 = uVar1 + (uVar1 >> 1 & 0xff);
    uVar1 = local_19 * 0x1000000 + (int)local_1c + local_1b * 0x100 + local_1a * 0x10000;
    uVar1 = uVar1 ^ ((int)uVar1 >> 3 & 0x20000000U) + uVar1 * 0x20;
    uVar1 = uVar1 ^ uVar1 << 7;
    uVar1 = (uVar1 >> 1 & 0xff) + uVar1;
    uVar1 = ((int)uVar1 >> 3 & 0x20000000U) + uVar1 * 0x20 ^ uVar1;
    uVar1 = uVar1 ^ uVar1 << 7;
    local_2c = uVar1 + (uVar1 >> 1 & 0xff);
    check_flag(&local_38);
  }
  if (local_10 == *(long *)(in_FS_OFFSET + 0x28)) {
    return sVar2 != 0x10;
  }
                    /* WARNING: Subroutine does not return */
  __stack_chk_fail();
}

看到这我们可以确定输入有16个字符长。

1
2
3
4
if (sVar2 != 0x10) {
    puts("Try Harder");
  }
  else {

然后经过一连串的异或移位，加法，乘法之后，调用了check_flag

1
2
3
4
5
6
7
8
9
10
11
12
13
/* check_flag(unsigned int*) */
 
void check_flag(uint *param_1)
 
{
  if ((((*param_1 == 0xcb9f59b7) && (param_1[1] == 0x5b90f617)) && (param_1[2] == 0x20e59633)) &&
     (param_1[3] == 0x102fd1da)) {
    puts("Good Work!");
    return;
  }
  puts("Try Harder");
  return;
}

假设我们的目标是来到“Good Work!”这一行。我们需要找到程序的正确的输入，（也许这里有多个答案，因为这个移位操作）。

 

我们有以下的几个选择：

>暴力破解，16个字符，可能是字母符号数字...暴力太难了
>逆向-动态/静态分析，尽管逆向不是很有趣，我们也可以在运行时改变一下param_1的值通过hook的方式...
>打补丁，通过打补丁的方式让他到puts这里。但让我们假设我们不想做任何的改变。
>符号执行（Angr），我们今天的明显选择。另外，它为我们提供了一个实际有效的程序输入。

Angr

首先我们加载需要的库：

1
2
import angr
import claripy

接下来，我们将设置程序的基地址并通过 Angr 加载二进制文件。
我们会设置程序的基地址，并且设置"auto_load_libs"为false。
注意：设置"auto_load_libs"为false，将禁止CLE（Angr的二进制文件加载器）自动处理动态库依赖。我建议使用它，防止当某个动态库无法找到时，抛出异常。

1
2
3
4
# Ghidra loaded the binary to 0x00100000 (default Image Base)
base_addr = 0x00100000
 
proj = angr.Project('./jack', main_opts={'base_addr': base_addr}, load_options={"auto_load_libs": False})

填上我们收集的二进制文件信息：
我们知道我们的输入需要16个字符的长度，因此，我们需要为我们的16个字符创建一个符号位向量。在把它们链接到一起之前，我为每个输入字节创建一个位向量。

 

注意：位向量本质只是一串位序列，一个符号位向量只是一个符号变量，它在某种意义上不是保存具体的数值，而是保存一个符号。然后，使用该变量执行算术运算将产生一个运算树（根据编译器理论称为抽象语法树或 AST）。如示例中所示，AST 可以转换为约束。

1
2
3
4
5
6
input_length = 16
 
# claripy.BVS('x', 8) => Create an eight-bit symbolic bitvector "x".
# Creating a symbolic bitvector for each character:
input_chars = [claripy.BVS("char_%d" % i, 8) for i in range(input_length)]
input = claripy.Concat(*input_chars)

接下来，在将程序的输入设置为stdin的同时获取程序的入口状态。

1
entry_state = proj.factory.entry_state(args=["./jack"], stdin=input)

添加约束条件，以便每个字符都必须在可打印的 ascii 范围内。 这只是我的一个假设，我们不知道它是真是假。

1
2
for byte in input_chars:
    entry_state.solver.add(byte >= 0x20, byte <= 0x7e)

现在我们已经完成了设置，我们可以用符号模拟二进制的执行了。我们还需要关键的一个东西SimulationManager。有了它我们就可以控制多种状态，step() run()就像调试器一样。

1
2
# Establish the simulation with the entry state
simulation = proj.factory.simulation_manager(entry_state)

现在我们可以使用符号执行程序了，我们应该设置一些目标。我们可以设置Angr应该运行到哪，哪一个分支不用关心

1
2
3
4
5
success_addr = 0x00101489 # Address of "puts("Good Work!");"
failure_addr = 0x00101468 # Address of "puts("Try Harder");"
 
# Finding a state that reaches `success_addr`, while discarding all states that go through `failure_addr`
simulation.explore(find = success_addr, avoid = failure_addr)

检查我们是否执行到success_addr就很简单了：

1
2
3
4
5
6
7
# If at least one state was found
if len(simulation.found) > 0:
    # Take the first one and print what it evaluates to
    solution = simulation.found[0]
    print(solution.solver.eval(input, cast_to=bytes))
else:
    print("[-] no solution found :(")

在原来的程序上执行脚本的结果，

1
2
3
4
5
6
7
b'n0_5ymb0l1c,3x30'
 
❯ ./jack
Enter your key:
n0_5ymb0l1c,3x30
Good Work!
bye

六、结论

Angr在有些情况下，比如在上面的例子中，的确非常有用，你可以使用它作为一个单独的工具或者一些逆向工具的开源插件，例如：IDA，Ghidra，Binary Ninja或者更多。


[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)

收藏
免费 ・3
支持
分享
最新回复 (3)
erfze
雪    币： 1332
活跃值： (9481)
能力值： ( LV12，RANK：650 )
在线值：
发帖
回帖
粉丝
私信
2 楼
沙发
2021-6-27 18:43
0
babaa
雪    币： 20
能力值： ( LV1，RANK：0 )
在线值：
发帖
回帖
粉丝
私信
3 楼

 这个加载基地址有影响吗？

最后于 2021-7-9 14:25 被babaa编辑 ，原因：
2021-7-3 22:36
0
dig_grave
雪    币： 8203
活跃值： (2738)
能力值： ( LV5，RANK：65 )
在线值：
发帖
回帖
粉丝
私信
4 楼
babaa &nbsp;这个加载基地址有影响吗？
没有
2021-7-4 15:17
0
游客
登录 | 注册 方可回帖
回帖 表情 雪币赚取及消费
高级回复
返回
//