angr 学习笔记

字数统计: 15k   |   阅读时长≈ 66 分钟

angr 学习笔记

学习过程取自github项目：angr_ctf

学习链接：https://github.com/jakespringer/angr_ctf

参考资料：https://www.anquanke.com/post/id/216504#h3-3

什么是angr

angr是一个多架构的用于分析二进制文件的python框架，它结合了静态和动态符号分析能力，使得它能胜任多种任务。

  • angr 的功能：

    • 控制流图恢复
    • 符号执行
    • 使用 angrop 自动构建ROP链
    • 使用 patcherex 自动进行二进制强化
    • 使用 rex 自动生成漏洞利用程序（用于DECREE和简单的Linux二进制程序）
    • 使用 angr-management（一个angr的GUI）来分析二进制程序

  • angr构成（模块）

    • 可执行文件和库的加载器：CLE。

      • CLE(CLE Load Everything) 负责装载二进制对象以及它所依赖的库，将自身无法执行的操作转移给angr的其它组件，最后生成地址空间，表示该程序已加载并可以准备运行。

    • 描述各种架构的库：archinfo。

    • 关于二进制代码转换VEX的python包装器 ：PyVEX。

      • angr需要处理不同的架构，所以它选择一种中间语言来进行它的分析，angr使用Valgrind的中间语言——VEX来完成这方面的内容。VEX中间语言抽象了几种不同架构间的区别，允许在他们之上进行统一的分析。

    • 中间语言VEX执行的模拟器：SimuVEX

      • 它允许你控制符号执行。

    • 抽象的约束求解包装器：Claripy。（大部分用法和Z3类似）

      • 这个模块主要专注于将变量符号化，生成约束式并求解约束式，这也是符号执行的核心所在。

    • 程序分析套件：angr。（上层封装好的接口）

angr_ctf

通过 ctf 里的angr解题的使用来深入理解 angr

00_angr_find

题目目录里有一个 c 源码，三个 py 文件。其中 scanffoldXXX.py 文件是一个需要补全的解决方案，generate.py 帮助我们生成本机的可执行文件。在这里我们直接使用 dist 文件夹中现成的可执行文件。这里的每一个可执行文件运行以后我们见到的格式都一样，为输入一串钥匙，然后得到正确与否的反馈。我们将 00_angr_find 文件拖入 IDA 里分析，并查看他的主函数：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
int __cdecl main(int argc, const char **argv, const char **envp)
{
  signed int i; // [esp+1Ch] [ebp-1Ch]
  char s1[9]; // [esp+23h] [ebp-15h]
  unsigned int v6; // [esp+2Ch] [ebp-Ch]

  v6 = __readgsdword(0x14u);
  printf("Enter the password: ");
  __isoc99_scanf("%8s", s1);
  for ( i = 0; i <= 7; ++i )
    s1[i] = complex_function(s1[i], i);
  if ( !strcmp(s1, "JACEJGCS") )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

可以看到最为关键的加密函数 *complex_function()*，我们进入函数：

1
2
3
4
5
6
7
8
9
int __cdecl complex_function(signed int a1, int a2)
{
  if ( a1 <= 64 || a1 > 90 )
  {
    puts("Try again.");
    exit(1);
  }
  return (3 * a2 + a1 - 65) % 26 + 65;
}

限制传入参数都为大写字符，并且返回一个经过 (3 * a2 + a1 - 65) % 26 + 65 此种加密的字符。最后在主函数中与比较字符串：JACEJGCS 比较。在学习angr库之前，这个题我们一般会采取常规的爆破解法：

1
2
3
4
5
6
7
8
9
10
11
flag = ''
compare_str = 'JACEJGCS'
def complex_function(a1, a2):
  return (3 * a2 + a1 - 65) % 26 + 65
if __name__ == "__main__":
    for i in range(len(compare_str)):
        for j in range(64,90):      
            if ord(compare_str[i]) == complex_function(j,i):
                flag += chr(j)
                break            
    print(flag)

但此题也是一个很标准的可以使用 angr 解题的题目：

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
import angr
import sys

def main(argv):
  path_to_binary = '/usr/Downloads/dist/00_angr_find'  # 获取文件路径
  project = angr.Project(path_to_binary)	# 将二进制文件装载成angr中指定的Project对象

  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )
 # factory提供了Project对象的一系列调用接口，entry_state()则是提供了一个程序的实例镜像(SimState对象)，
 # 模拟程序执行某个时刻的状态（记录一系列程序运行时信息，如内存/寄存器/文件系统数据），一般我们选择程序的入口
 # 状态entry_state()即可，程序会从main函数开始运行
  simulation = project.factory.simgr(initial_state)	# 通过simgr方法进行接受状态信息后的初始化

  print_good_address = 0x08048678	# 需要执行到的地址  
  simulation.explore(find=print_good_address)
	# 通过simgr的explore()函数实现查找，这里的地址使用ida中看到的Good Job对应的内存地址
  
  if simulation.found:
	# simgr会把找到的符合要求的路径存储在found中
    
    solution_state = simulation.found[0]
	# 取找到的第一个路径
  
    print(solution_state.posix.dumps(sys.stdin.fileno()).decode())
    # posix.dumps(sys.stdin.fileno())获取当前状态下stdin输入的数据，即程序的输入值
    
  else:
  
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

总体思路为我们找到打印 ‘Good job’ 的地址，我们只需要让 angr 想办法执行能够执行到那个地址的路径，然后获取输入即可。

接下来开始分析一个简单的angr脚本构成：

创建Project

1
2
path_to_binary = '/usr/Downloads/dist/00_angr_find'  
project = angr.Project(path_to_binary，auto_load_libs=False)

使用 angr的首要步骤就是创建Project加载二进制文件。angr的二进制装载组件是CLE，它负责装载二进制对象（以及它依赖的任何库）和把这个对象以易于操作的方式交给angr的其他组件。angr将这些包含在Project类中。一个Project类是代表了你的二进制文件的实体。你与angr的大部分操作都会经过它。

auto_load_libs 设置是否自动载入依赖的库，在基础题目中我们一般不需要分析引入的库文件，这里设置为否。

  • 如果auto_load_libs是True（默认值），真正的库函数会被执行。这可能正是也可能不是你想要的，取决于具体的函数。比如说一些libc的函数分析起来过于复杂并且很有可能引起path对其的尝试执行过程中的state数量的爆炸增长
  • 如果auto_load_libs是False，且外部函数是无法找到的，并且Project会将它们引用到一个通用的叫做ReturnUnconstrained的SimProcedure上去，它就像它的名字所说的那样：它返回一个不受约束的值

设置 state

1
2
3
4
initial_state = project.factory.entry_state(
  add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                  angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
)

state代表程序的一个实例镜像，模拟执行某个时刻的状态，就类似于快照。保存运行状态的上下文信息，如内存/寄存器等,我们这里使用project.factory.entry_state()告诉符号执行引擎从程序的入口点开始符号执行，除了使用.entry_state() 创建 state 对象, 我们还可以根据需要使用其他构造函数创建 state。

设置 Simulation Managers

1
simulation = project.factory.simgr(initial_state)

Project 对象仅表示程序一开始的样子，而在执行时，我们实际上是对SimState对象进行操作，它代表程序的一个实例镜像，模拟执行某个时刻的状态

SimState 对象包含程序运行时信息，如内存/寄存器/文件系统数据等。SM（Simulation Managers）是angr中最重要的控制接口，它使你能够同时控制一组状态(state)的符号执行，应用搜索策略来探索程序的状态空间。

运行，探索满足路径需要的值

符号执行最普遍的操作是找到能够到达某个地址的状态，同时丢弃其他不能到达这个地址的状态。SM为使用这种执行模式提供了.explore()方法

当使用find参数启动.explore()方法时，程序将会一直执行，直到发现了一个和find参数指定的条件相匹配的状态。find参数的内容可以是想要执行到的某个地址、或者想要执行到的地址列表、或者一个获取state作为参数并判断这个state是否满足某些条件的函数。当activestash中的任意状态和find中的条件匹配的时候，它们就会被放到found stash中，执行随即停止。之后你可以探索找到的状态，或者决定丢弃它，转而探索其它状态

获取执行结果

1
2
3
4
5
if simulation.found:
   solution_state = simulation.found[0]
   print(solution_state.posix.dumps(sys.stdin.fileno()).decode())
 else:
   raise Exception('Could not find the solution')

此时相关的状态已经保存在了simgr当中，我们可以通过simgr.found来访问所有符合条件的分支，这里我们为了解题，就选择第一个符合条件的分支即可

sys.stdin.fileno()

在UNIX中，按照惯例，三个文件描述符分别表示标准输入、标准输出和标准错误

1
2
3
4
5
6
7
>>> import sys
>>> sys.stdin.fileno()
0
>>> sys.stdout.fileno()
1
>>> sys.stderr.fileno()
2

所以一般也可以写成：

1
solution = solution_state.posix.dumps(0)

01_angr_avoid

​ 运行目标文件，也是固定的输入字符串判断正确与否输出的格式。将其拖入 IDA 中分析，发现他的主函数由于太长了，无法被反编译成 C 语言代码，也无法以图的格式查看汇编代码。但由于我们在学习 angr，所以就想到我们只需要找到正确路径即可。这样想是没问题的，通过 IDA 字符串查找，我们找到了 “Good job” 的地址，只要和先前一样，写一个最简单的 angr 脚本即可跑出答案。但是这里没有考虑到关于开销的问题。如此冗长的主函数，我们让 angr 去符号执行的话一定要有很大的时间开销。所以在 scanffold.py 文件中给了我们提示，除了需要我们填写正确路径的地址以外，还有一个名为 will_not_succeed_address 的地址需要我们填写，他将在下面语句simulation.explore(find=print_good_address, avoid=will_not_succeed_address) 中的 avoid 参数中进行填写。先放上整体的解题代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
import angr
import sys

def main(argv):
  path_to_binary = '/usr/Downloads/dist/01_angr_avoid'
  project = angr.Project(path_to_binary)
  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )
  simulation = project.factory.simgr(initial_state)

  print_good_address = 0x080485E0	# 正确路径的地址
  will_not_succeed_address = 0x080485A8	# 需要避开的路径
  simulation.explore(find=print_good_address, avoid=will_not_succeed_address)

  if simulation.found:
    solution_state = simulation.found[0]
    print(solution_state.posix.dumps(sys.stdin.fileno()).decode())
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

avoid

当一个状态和avoid中的条件匹配时，它就会被放进avoided stash中，之后继续执行。这样就做到了用 avoid 避免重复执行一些无用的代码片段来增加程序开销。

02_angr_find_condition

老规矩将目标文件放入 IDA 中分析，可以发现起始同第一个题目几乎一模一样：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
vint __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+18h] [ebp-40h]
  int j; // [esp+1Ch] [ebp-3Ch]
  char s1[20]; // [esp+24h] [ebp-34h] BYREF
  char s2[20]; // [esp+38h] [ebp-20h] BYREF
  unsigned int v8; // [esp+4Ch] [ebp-Ch]

  v8 = __readgsdword(0x14u);
  for ( i = 0; i <= 19; ++i )
    s2[i] = 0;
  qmemcpy(s2, "VXRRJEUR", 8);
  printf("Enter the password: ");
  __isoc99_scanf("%8s", s1);
  for ( j = 0; j <= 7; ++j )
    s1[j] = complex_function(s1[j], j + 8);
  if ( !strcmp(s1, s2) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;

既然这样我们就看scanffold文件中想要我们做些什么吧。打开 py 文件，发现题目中多了两个函数，关注题目中最上方大段的注解：

# 能够搜索到达某个指令的状态是非常有用的。 但是，在某些情况下，您可能不知道要到达的特定指令的地址（或者可能没有单一的指令目标。）在这个挑战中，您不知道哪条指令可以让您成功。 相反，您只知道您想要找到二进制打印“Good Job”的状态。

# Angr 的强大之处在于它允许您搜索满足您在 Python 中指定的任意条件的状态，使用您定义为函数的谓词，该函数接受状态并在找到所需内容时返回 True， 否则为 False。

所以我们需要补全的两个函数即是在得到 正确 / 错误 系统输出时返回 true / false。

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
import angr
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)
  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )
  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output  # :boolean

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output # :boolean

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]
    print(solution_state.posix.dumps(sys.stdin.fileno()).decode())
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

所以此题是通过condition的方式来选择find和avoid的分支，之前我们一直是反编译之后手动填写相应的语句内存地址，实际上在选择分支的时候可以根据对应的输出结果来判断，在explore的时候传入函数，用于指定什么情况下选择该路径，什么时候跳过该路径，即定义：

  • is_successful(state): 进入分支的条件
  • should_abort(state): 跳过分支的条件

这样引入一个函数就可以动态的进行分析获取 state。

03_angr_symbolic_registers

​ 将目标文件拖入 IDA 里面分析，我们可以发现此题与之前最大的不同就是需要多个输入，这样就超出了 angr 所能支持的范围，但是幸好 angr 支持我们手动符号注入到寄存器中。所以讲白了这道题如果要用 angr 来求解的话，我们需要找到注入点去手动符号注入到相关寄存器中。那么与整个流程相关的输入，就成了最应该先被关注的点。

1
2
3
4
5
6
7
8
.text:0804896E                 push    offset aEnterThePasswo ; "Enter the password: "
.text:08048973                 call    _printf
.text:08048978                 add     esp, 10h
.text:0804897B                 call    get_user_input
.text:08048980                 mov     [ebp+var_14], eax
.text:08048983                 mov     [ebp+var_10], ebx
.text:08048986                 mov     [ebp+var_C], edx
.text:08048989                 sub     esp, 0Ch

get_user_input 即为我们的输入函数，那么在输入函数返回之后有三个 mov 操作，也就是将我们的输入的三个16进制数保存到对应的三个寄存器中，看到这欣喜的找到了注入点。接下来看 scanffold 文件，看看他指引我们怎么去构造 angr 脚本：

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x08048989    # :integer (probably hexadecimal)
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password0_size_in_bits = 32  # :integer
  password0 = claripy.BVS('password0', password0_size_in_bits)
  password1_size_in_bits = 32  
  password1 = claripy.BVS('password1', password1_size_in_bits)
  password2_size_in_bits = 32 
  password2 = claripy.BVS('password2', password2_size_in_bits)

  initial_state.regs.eax = password0
  initial_state.regs.ebx = password1
  initial_state.regs.edx = password2

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return "Good Job.".encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return "Try again.".encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)
    solution2 = solution_state.solver.eval(password2)

    solution = '{:x} {:x} {:x}'.format(solution0, solution1, solution2)  # :string
    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

状态预设

​ 首先我们需要填入 start_address 的地址，也就是我们的注入点。那既然我们是手动注入，那么我们预设的状态就不能是先前的 entry_state 了。正好 angr 为我们提供了一系列构造函数让我们根据需要创建 state：

名称 描述
.entry_state() 构造一个已经准备好从函数入口点执行的状态
.blank_state 构造一个“空状态”，它的大多数数据都是未初始化的。当使用未初始化的的数据时，一个不受约束的符号值将会被返回
.call_state 构造一个已经准备好执行某个函数的状态
.full_init_state 构造一个已经执行过所有与需要执行的初始化函数，并准备从函数入口点执行的状态。比如，共享库构造函数（constructor）或预初始化器。当这些执行完之后，程序将会跳到入口点

我们使用 blank_state() 方法，通过传递addr=start_address，我们有效地告诉blank_state()在该特定地址创建一个新状态。

位向量(bitvector)

​ 更应该准确的说是符号位向量，符号位向量是angr用于将符号值注入程序的数据类型。这些将是angr将解决的方程式的“ x”，也就是约束求解时的自变量。可以通过 BVV(value,size) 和 BVS( name, size) 接口创建位向量，也可以用 FPV 和 FPS 来创建浮点值和符号

​ 在这里我们使用claripy通过BVS()方法生成三个位向量。此方法有两个参数：第一个是angr用来引用位向量的名称，第二个是位向量本身的大小（以位为单位）。由于符号值存储在寄存器中，并且寄存器的长度为32位，因此位向量的大小将为32位

1
2
3
4
5
6
password0_size_in_bits = 32  
password0 = claripy.BVS('password0', password0_size_in_bits)
password1_size_in_bits = 32  
password1 = claripy.BVS('password1', password1_size_in_bits)
password2_size_in_bits = 32 
password2 = claripy.BVS('password2', password2_size_in_bits)

访问寄存器

get_user_input() 接受三个16进制输入并将其放入三个寄存器中，我们可以通过 state.regs 对象的属性访问以及修改寄存器的数据。

然后把我们之前创建的符号位向量（bitvectors）放入属于他们的地方：寄存器EAX，EBX和EDX。我们将修改initial_state之前创建的内容并更新寄存器的内容

1
2
3
initial_state.regs.eax = password0
initial_state.regs.ebx = password1
initial_state.regs.edx = password2

约束求解

可以通过使用state.solver.eval(symbol)对各个断言进行评测来求出一个合法的符号值（若有多个合法值，返回其中的一个），我们根据eval()之前注入的三个符号值调用求解器引擎的方法。

1
2
3
4
solution0 = solution_state.solver.eval(password0)
solution1 = solution_state.solver.eval(password1)
solution2 = solution_state.solver.eval(password2)
solution = '{:x} {:x} {:x}'.format(solution0, solution1, solution2)

04_angr_symbolic_stack

​ 此题也是多个输入，但此题种种提示都告诉我们要使用 angr 对栈有关的操作。为什么上一提可以直接在寄存器传参处进行符号注入但是此题不行呢。讲白了就是他们参数传递的方式不同。上一题中，参数是通过寄存器传递，所以我们直接在涉及到与目标寄存器有关的 mov 指令处进行符号注入即可，但是此题值是通过栈传递。

1
2
3
4
5
6
call    ___isoc99_scanf
add     esp, 10h
mov     eax, [ebp+var_C]
sub     esp, 0Ch
push    eax
call    complex_function0

在完成调用 scanf 函数并且返回后，先 add esp, 10h 将栈帧还原，再将输入的第一个参数存放在 eax 寄存器中，再开辟栈帧将 eax 寄存器入栈，将参数保存在栈上，然后调用加密函数 complex_function0。对参数二的处理也是这样：

1
2
3
4
5
6
add     esp, 10h
mov     [ebp+var_C], eax
mov     eax, [ebp+var_10]
sub     esp, 0Ch	
push    eax
call    complex_function1

步骤仍然是还原栈帧，将加密后的值又重新存入了 var_10 中，然后输入的第二个参数保存在 eax 寄存器中，开辟栈帧，eax 入栈，进行第二个加密函数。

所以据此，我们在 scanffold 中构造我们需要的栈并符号执行：

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

start_address = 0x08048697
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

	initial_state.regs.ebp = initial_state.regs.esp

  password0 = claripy.BVS('password0', 32)
  password1 = claripy.BVS('password1', 32)

  padding_length_in_bytes = 8  
  initial_state.regs.esp -= padding_length_in_bytes

	initial_state.stack_push(password0)  
  initial_state.stack_push(password1)

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)

    solution = '{} {}'.format(solution0, solution1)
    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

注入点选择

​ 刚开始做的时候，对于注入点的选择很摸不着头脑，其实应该这么去理解，我们要构造栈帧，也就需要从栈稳定的状态去入手，而 scanf 调用后栈帧还原要在 esp 加8执行以后。而在 angr 中，我们对于初始状态的设置是在该地址处指令执行之前就设置好的，所以我们的注入点一定选在栈帧还原之后，也就是我们将输入的第一个参数存放于 eax 寄存器的操作的地址处。

填充位数

​ 我们构造栈的目的是为了开辟栈空间去存放自己的符号，又要让程序可以正常引用我们的符号去符号执行。首先我们构造栈帧肯定先将 ebp 指针抬升至 esp 处，接下来要抬升栈顶指针 esp。关于抬升的位数（也就是所谓的 padding），我们就需要参照后面程序对参数的引用。在 main 函数的开头就写到：

1
2
var_10           = dword ptr -10h
var_C            = dword ptr -0Ch

​ 所以 ebp+varX 其实就等于 ebp-X。所以对于参数的寻址也都是对 ebp 的减少。我们的输入为两个四字节无符号整数，如果想要能让程序正确的通过 ebp 来引用到我们的参数，就需要给栈顶指针 esp 一定的抬升，使得两个参数 push 以后与 ebp 的距离满足 0x10 和 0xC（push 的本质其实就是抬升栈顶指针，然后将目标数据保存在栈顶）。由于一个数据是四个字节，我们可以知道，var_10 占用的空间是 ebp-0x10 ~ ebp-0xC，var_C 占用的空间为 ebp-0xC~ebp-0x8。所以我们需要将 esp 抬升 8 个字节来接受参数的 push。

05_angr_symbolic_memory

​ 用 IDA 打开目标文件可以发现，我们的 scanf 输入的四个八位字符串被分别存储到了四个全局变量中，也就是我们只需要在合适的时候将符号注入到目标位置即可。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x08048601
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password0 = claripy.BVS('password0', 64)
  password1 = claripy.BVS('password1', 64)
  password2 = claripy.BVS('password2', 64)
  password3 = claripy.BVS('password3', 64)


  password0_address = 0x8134360
  initial_state.memory.store(password0_address, password0)
  initial_state.memory.store(password0_address + 0x8, password1)
  initial_state.memory.store(password0_address + 0x10, password2)
  initial_state.memory.store(password0_address + 0x18, password3)

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode()
    solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode()
    solution2 = solution_state.solver.eval(password2,cast_to=bytes).decode()
    solution3 = solution_state.solver.eval(password3,cast_to=bytes).decode()
    solution = '{} {}'.format(solution0, solution1, solution2, solution3)
    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

注入点选择

​ 跟上一个思路基本类似，我们需要对全局变量进行符号注入，就得在 1. 主函数对此空间进行 memset 初始化后，2. scanf 函数返回，栈帧还原后。

store

通过initial_state.memory.store 函数向我们指定的内存地址中进行符号注入。

cast_to=bytes

通过 eval 函数中 cast_to 参数，使得我们的求解结果返回能被 decode 成字符串的字节串。

06_angr_symbolic_dynamic_memory

拖入 IDA 分析，最大的特点就是使用 malloc 分配内存 ,但是我们并不能明确 malloc 分配的堆内存的地址。所以我们使用 angr 提供的函数 fake_heap_address，pointer_to_malloc_memory_address来假定一段可读写空内存给 malloc 去分配，然后我们即可以对该内存进行符号注入。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x8048699
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password0 = claripy.BVS('password0', 64)
  password1 = claripy.BVS('password1', 64)

  fake_heap_address0 = 0x0804A060
  pointer_to_malloc_memory_address0 = 0x0ABCC8A4	# buffer0 
  initial_state.memory.store(pointer_to_malloc_memory_address0, fake_heap_address0, endness=project.arch.memory_endness)
  fake_heap_address1 = 0x0804A29A 
  pointer_to_malloc_memory_address1 = 0x0ABCC8AC	# buffer1
  initial_state.memory.store(pointer_to_malloc_memory_address1, fake_heap_address1, endness=project.arch.memory_endness)

  initial_state.memory.store(fake_heap_address0, password0)
  initial_state.memory.store(fake_heap_address1, password1)

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode()
    solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode()
    solution = '{} {}'.format(solution0, solution1)

    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

fake_heap_address

通过 fake_heap_address 函数申请一个假定的但又固定地址的堆内存。

pointer_to_malloc_memory_address

通过 pointer_to_malloc_memory_address 分配一个指针指向我们申请的 fake 堆。

07_angr_symbolic_file

放入 IDA 中分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
int __cdecl __noreturn main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+Ch] [ebp-Ch]

  memset(buffer, 0, sizeof(buffer));
  printf("Enter the password: ");
  __isoc99_scanf("%64s", buffer);
  ignore_me((int)buffer, 0x40u);
  memset(buffer, 0, sizeof(buffer));
  fp = fopen("OJKSQYDP.txt", "rb");
  fread(buffer, 1u, 0x40u, fp);
  fclose(fp);
  unlink("OJKSQYDP.txt");
  for ( i = 0; i <= 7; ++i )
    *(_BYTE *)(i + 134520992) = complex_function(*(char *)(i + 134520992), i);
  if ( strncmp(buffer, "AQWLCTXB", 9u) )
  {
    puts("Try again.");
    exit(1);
  }
  puts("Good Job.");
  exit(0);
}

​ 我们可以看到文件相关的函数 fopen fread 等等。所以这题一定是要我们学习如何符号化一个文件的内容。通过 scanffold 的注释我们可以了解到，为了让此题的格式与其他题目保持一致，也就是输入，判断，输出结果此类格式，通过 ignore_me 函数实现将我们的输入写入文件。所以我们直接将该函数当作 input 函数即可，注入点选择在函数返回栈帧还原之后。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x080488D6
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  filename = 'OJKSQYDP.txt'  # :string
  symbolic_file_size_bytes = 64

  password = claripy.BVS('password', symbolic_file_size_bytes * 8)

  password_file = angr.storage.SimFile(filename, content=password, size=symbolic_file_size_bytes)
  
  initial_state.fs.insert(filename, password_file)

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = solution_state.solver.eval(password,cast_to=bytes).decode()

    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

仿真文件系统

angr.storage.SimFile(filename, content= , size= )

​ 通过该函数可以创建一个符号文件，符号文件需要在初始化 state 的时候就注入，所以需要在创建之后把符号文件传递给初始化状态 state。使用 fs 的 insert 函数将该符号文件插入到初始化状态 state 中：initial_state.fs.insert(filename, password_file)

08_angr_constraints

​ 拖入 IDA 分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+Ch] [ebp-Ch]

  qmemcpy(&password, "AUPDNNPROEZRJWKB", 16);
  memset(&buffer, 0, 0x11u);
  printf("Enter the password: ");
  __isoc99_scanf("%16s", &buffer);
  for ( i = 0; i <= 15; ++i )
    *(i + 0x804A050) = complex_function(*(i + 0x804A050), 15 - i);
  if ( check_equals_AUPDNNPROEZRJWKB(&buffer, 0x10u) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

其他的流程都很常规，只是我们在主函数中看不到我们的比较过程了。我们跟进分析函数check_equals_AUPDNNPROEZRJWKB：

1
2
3
4
5
6
7
8
9
10
11
12
13
_BOOL4 __cdecl check_equals_AUPDNNPROEZRJWKB(int a1, unsigned int a2)
{
  int v3; // [esp+8h] [ebp-8h]
  unsigned int i; // [esp+Ch] [ebp-4h]

  v3 = 0;
  for ( i = 0; i < a2; ++i )
  {
    if ( *(i + a1) == *(i + 0x804A040) )
      ++v3;
  }
  return v3 == a2;
}

我们可以发现实际上我们的输入经过加密后是一个字节一个字节与比较字符串比较的，如果出现有一位比较错误都会返回 false。如果我们常规地使用 angr 求解，则会出现路径爆炸的问题：

所谓符号执行就是把程序中的变量符号化去模拟程序运行，搜集路径约束条件并使用约束求解器对其进行求解后得到结果。当一个程序存在循环结构时，即使逻辑十分简单也可能会产生规模十分巨大的执行路径。在符号执行的过程中，每个分支点都会产生两个实例，当程序中存在循环结构展开时，可能会导致程序分支路径数呈指数级增长，即路径爆炸问题。

​ check_equals_AUPDNNPROEZRJWKB()函数就是一个字符一个字符的比较，就会产生路径爆炸问题，原始也是每次调用循环中的if语句（16次）时，计算机都需要产生判断分支，从而导致2 ^ 16 = 65,536分支，这将花费很长时间来测试并获得我们的答案，这也就是 angr 路径爆炸的请况。所以我们的思路就是在执行到该比较函数的时候停止，我们手动添加约束条件求解，即可绕过计算量如此巨大的比较函数。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x08048625
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password = claripy.BVS('password', 16*8)

  password_address = 0x0804A050	# buffer
  initial_state.memory.store(password_address, password)

  simulation = project.factory.simgr(initial_state)

  address_to_check_constraint = 0x08048673	# 调用check_equals_AUPDNNPROEZRJWKB的地址
  simulation.explore(find=address_to_check_constraint)	# angr仅执行到此处

  if simulation.found:
    solution_state = simulation.found[0]

    constrained_parameter_address = 0x0804A050	# 约束参数的地址，也就是用于比较的buffer
    constrained_parameter_size_bytes = 16
    constrained_parameter_bitvector = solution_state.memory.load(
      constrained_parameter_address,
      constrained_parameter_size_bytes
    )

    constrained_parameter_desired_value = 'AUPDNNPROEZRJWKB' # :string (encoded)

    solution_state.add_constraints(constrained_parameter_bitvector == constrained_parameter_desired_value)

    solution = solution_state.solver.eval(password, cast_to=bytes)

    print(solution.decode())
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

加载约束变量

​ 我们令 angr 仅符号执行到 check_equals_AUPDNNPROEZRJWKB 函数执行前，而后我们将手动为其添加约束，那么我们就需要在约束求解之前从程序中提取出所需要的约束参数，也就是经过加密的我们注入的符号。 我们通过下面的函数加载约束常参数。 solution_state.memory.load(constrained_parameter_address, constrained_parameter_size_bytes)

约束求解

​ 在angr中提供了可以用加入一个约束条件到一个 state 中的方法（state.solver.add），将每一个符号化的布尔值作为一个关于符号变量合法性的断言。之后可以通过使用state.solver.eval(symbol)对各个断言进行评测来求出一个合法的符号值（若有多个合法值，返回其中的一个）。简单来说就是通过 .add 对 state 对象添加约束，并使用 .eval 接口求解，得到符号变量的可行解。所以我们通过函数 solution_state.add_constraints 添加了一个约束条件，并使用 solution = solution_state.solver.eval()求解。

像这个约束求解的知识点在 Z3 中经常使用，在这里 claripy 库其实就是对 Z3 库的一个封装。

09_angr_hooks

拖入 IDA 分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
int __cdecl main(int argc, const char **argv, const char **envp)
{
  _BOOL4 v3; // eax
  int i; // [esp+8h] [ebp-10h]
  int j; // [esp+Ch] [ebp-Ch]

  qmemcpy(password, "XYMKBKUHNIQYNQXE", 16);
  memset(buffer, 0, 0x11u);
  printf("Enter the password: ");
  __isoc99_scanf("%16s", buffer);
  for ( i = 0; i <= 15; ++i )
    *(_BYTE *)(i + 134520916) = complex_function(*(char *)(i + 134520916), 18 - i);
  equals = check_equals_XYMKBKUHNIQYNQXE(buffer, 16);
  for ( j = 0; j <= 15; ++j )
    *(_BYTE *)(j + 134520900) = complex_function(*(char *)(j + 134520900), j + 9);
  __isoc99_scanf("%16s", buffer);
  v3 = equals && !strncmp(buffer, password, 0x10u);
  equals = v3;
  if ( v3 )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

​ 我们可以看到该程序的整体结构为第一次读区输入缓冲区的 16 个字节进行加密，结果传入check_equals_XYMKBKUHNIQYNQXE函数进行逐字节比较，返回比较结果的布尔值。然后再进行第二次对输入缓冲区 16 个字节的读取，直接进行整体字符串的比较：strncmp，然后根据两次比较的布尔值的逻辑与输出结果。

​ 那么既然出现逐字节比较，就会出现 angr 的路径爆炸问题，所以我们需要想办法规避该函数。在上一题中我们使用手动添加约束求解，在这题中，我们使用 Hook 技术来直接跳过该函数。

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
# This level performs the following computations:
#
# 1. Get 16 bytes of user input and encrypt it.
# 2. Save the result of check_equals_AABBCCDDEEFFGGHH (or similar)
# 3. Get another 16 bytes from the user and encrypt it.
# 4. Check that it's equal to a predefined password.
#
# The ONLY part of this program that we have to worry about is #2. We will be
# replacing the call to check_equals_ with our own version, using a hook, since
# check_equals_ will run too slowly otherwise.

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  check_equals_called_address = 0x080486B3	# 想要hook的函数的调用地址

  instruction_to_skip_length = 5	# hook以后掠过的地址长度
  @project.hook(check_equals_called_address, length=instruction_to_skip_length)
  def skip_check_equals_(state):

    user_input_buffer_address = 0x0804A054 # buffer的地址
    user_input_buffer_length = 16	# 从buffer中读取的长度

    user_input_string = state.memory.load(
      user_input_buffer_address,
      user_input_buffer_length
    )

    check_against_string = 'XYMKBKUHNIQYNQXE' # 比较字符串

    state.regs.eax = claripy.If(
      user_input_string == check_against_string, 
      claripy.BVV(1, 32), 
      claripy.BVV(0, 32)
    )

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = solution_state.posix.dumps(0)
    print(solution.decode())
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

​ 我们使用 hook 技术将原本会导致路径爆炸的函数 hook 掉，并手动构造了一个与其功能一样但不会导致路径爆炸的函数，将返回值写入 eax 寄存器中（该函数通过 eax 寄存器传递返回值），之后便正常添加 avoid 条件，符号执行即可。

Hook

以下内容来自维基百科：

钩子编程（hooking），也称作“挂钩”，是计算机程序设计术语，指通过拦截软件模块间的函数调用、消息传递、事件传递来修改或扩展操作系统、应用程序或其他软件组件的行为的各种技术。处理被拦截的函数调用、事件、消息的代码，被称为钩子（hook）。

​ angr使用一系列引擎（SimEngine的子类）来模拟被执行代码对输入状态产生的影响。其中就有hook engine来处理hook的情况。默认情况下，angr 会使用 SimProcedures 中的符号摘要替换库函数，即设置 Hooking，这些 python 函数摘要高效地模拟库函数对状态的影响。

​ SimProcedure 其实就是 Hook 机制，可以通过 proj.hook(addr,hook) 设置，其中 hook 是一个 SimProcedure 实例。 通过 .is_hooked / .unhook / .hook_by 进行管理。将 proj.hook(addr) 作为函数装饰器，可以编写自己的 hook 函数。还可以通过 proj.hook_symbol(name,hook) hook 函数。

​ 在此题中我们通过 @project.hook(address, length=skip_length)hook 掉了check 函数，并自定义了一个函数来取代 check 函数，也就通过钩子钩取了函数的调用，以实现我们规避路径爆炸的问题。

约束求解中的 if

​ 在我们自定义的函数中，最后一步是返回比较的布尔值，但我们没有采用常规的 if-else。因为我们这里的函数实际上是在求解一个 z3 的约束求解的实例，所以得使用 claripy 中内置函数来处理：claripy.If(expression, ret_if_true, ret_if_false) 。

10_angr_simprocedures

拖入 IDA 中分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+20h] [ebp-28h]
  char s[17]; // [esp+2Bh] [ebp-1Dh] BYREF
  unsigned int v6; // [esp+3Ch] [ebp-Ch]

  v6 = __readgsdword(0x14u);
  memcpy(&password, "ORSDDWXHZURJRBDH", 0x10u);
  memset(s, 0, sizeof(s));
  printf("Enter the password: ");
  __isoc99_scanf("%16s", s);
  for ( i = 0; i <= 15; ++i )
    s[i] = complex_function(s[i], 18 - i);
  if ( check_equals_ORSDDWXHZURJRBDH(s, 16) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

​ 可以看出这题的逻辑跟前面两道题类似，同样我们需要规避掉会导致 angr 路径爆炸的 check 函数。但是我们可以发现此题的 check 函数的调用尤其恶心，我们查看交叉引用可以发现 check 函数有不下于上百次调用，这样我们就无法使用上一题的方法去针对某一个地址进行 hook 了，这就需要使用 SimProcedure 来编写我们的自定义 check 函数去集体替换源程序中的 check 函数。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  class ReplacementCheckEquals(angr.SimProcedure):

    def run(self, to_check, len):	# self后面的参数就是我们需要替换的函数所需的参数

      user_input_buffer_address = to_check
      user_input_buffer_length = len

      user_input_string = self.state.memory.load(
        user_input_buffer_address,
        user_input_buffer_length
      )

      check_against_string = 'ORSDDWXHZURJRBDH'

      return claripy.If(user_input_string == check_against_string, claripy.BVV(1, 32), claripy.BVV(0, 32))


  check_equals_symbol = 'check_equals_ORSDDWXHZURJRBDH' # :string
  project.hook_symbol(check_equals_symbol, ReplacementCheckEquals())	# 通过函数名称集体替换

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = solution_state.posix.dumps(0)
    print(solution.decode())
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

Hooking Symbols

​ 每一个程序都有一个符号表，angr可以确保从每个导入符号都可以解析出地址，可以使用angr提供的Project.hook_symbol的API来通过符号名来Hook函数所有的调用地址，这意味着可以用自己的代码替换函数。

​ 所以在此题中，我们如果使用上一题的方法去一个地址一个地址 hook 程序中的 check 函数显得过于低效。所以我们在定义好替换函数后，使用project.hook_symbol(func_symbol, Replacefunc())来通过函数的符号名集体替换。

11_angr_sim_scanf

拖入 IDA 分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+20h] [ebp-28h]
  char s[20]; // [esp+28h] [ebp-20h] BYREF
  unsigned int v7; // [esp+3Ch] [ebp-Ch]

  v7 = __readgsdword(0x14u);
  memset(s, 0, sizeof(s));
  qmemcpy(s, "SUQMKQFX", 8);
  for ( i = 0; i <= 7; ++i )
    s[i] = complex_function(s[i], i);
  printf("Enter the password: ");
  __isoc99_scanf("%u %u", buffer0, buffer1);
  if ( !strncmp(buffer0, s, 4u) && !strncmp(buffer1, &s[4], 4u) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

​ 可以看到这题与 03 那道题类似，angr 没法处理多组输入，在 03 中我们观察到输入的值被保存到寄存器中参与加密，所以我们对相应寄存器进行符号注入求解，此题我们使用 SimProcedure 重写我们的 scanf 函数来求解：

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  class ReplacementScanf(angr.SimProcedure):

    def run(self, format_string, scanf0_address, scanf1_address):
      scanf0 = claripy.BVS('scanf0', 32)
      scanf1 = claripy.BVS('scanf1', 32)

      self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
      self.state.memory.store(scanf1_address, scanf1, endness=project.arch.memory_endness)

      self.state.globals['solution0'] = scanf0
      self.state.globals['solution1'] = scanf1
      

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job.'.encode() in stdout_output

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again.'.encode() in stdout_output

  simulation.explore(find=is_successful, avoid=should_abort)

  if simulation.found:
    solution_state = simulation.found[0]

    stored_solutions0 = solution_state.globals['solution0']
    stored_solutions1 = solution_state.globals['solution1']
    solution = '{} {}'.format(solution_state.solver.eval(stored_solutions0), solution_state.solver.eval(stored_solutions1))

    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

​ scanf其实就是将输入写入内存，所以我们使用 self.state.memory.store()来实现 scanf 函数的功能。

globals

​ 这里的关键我们都知道Python的变量生存周期，在这里scanf0和scanf1是函数ReplacementScanf的局部变量，为了让函数外部也能获得我们输入的符号位向量，从而调用求解器获得答案，需要将这两个符号位向量变为全局变量，这里我们需要调用带有全局状态的globals插件中“保存”对我们的符号值的引用。globals插件允许使用列表，元组或多个键的字典来存储多个位向量.

1
2
3
4
self.state.globals['solution0'] = scanf0
self.state.globals['solution1'] = scanf1
    
self.state.globals['solutions'] = (scanf0, scanf1)

上面的写法皆可。在我们需要进行约束求解的时候就需要从 global 插件中取出所需元素参与求解：

1
2
stored_solutions0 = solution_state.globals['solution0']
stored_solutions1 = solution_state.globals['solution1']

12_angr_veritesting

拖入 IDA 分析：

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
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int v3; // ebx
  int v5; // [esp-14h] [ebp-60h]
  int v6; // [esp-10h] [ebp-5Ch]
  int v7; // [esp-Ch] [ebp-58h]
  int v8; // [esp-8h] [ebp-54h]
  int v9; // [esp-4h] [ebp-50h]
  const char **v10; // [esp+0h] [ebp-4Ch]
  int v11; // [esp+4h] [ebp-48h]
  int v12; // [esp+8h] [ebp-44h]
  int v13; // [esp+Ch] [ebp-40h]
  int v14; // [esp+10h] [ebp-3Ch]
  int v15; // [esp+10h] [ebp-3Ch]
  int v16; // [esp+14h] [ebp-38h]
  int i; // [esp+14h] [ebp-38h]
  int v18; // [esp+18h] [ebp-34h]
  _DWORD v19[9]; // [esp+1Ch] [ebp-30h] BYREF
  unsigned int v20; // [esp+40h] [ebp-Ch]
  int *p_argc; // [esp+44h] [ebp-8h]

  p_argc = &argc;
  v10 = argv;
  v20 = __readgsdword(0x14u);
  memset((char *)v19 + 3, 0, 0x21u);
  printf("Enter the password: ");
  ((void (__stdcall *)(const char *, char *, int, int, int, int, int, const char **, int, int, int, int, int, int, _DWORD))__isoc99_scanf)(
    "%32s",
    (char *)v19 + 3,
    v5,
    v6,
    v7,
    v8,
    v9,
    v10,
    v11,
    v12,
    v13,
    v14,
    v16,
    v18,
    v19[0]);
  v15 = 0;
  for ( i = 0; i <= 31; ++i )
  {
    v3 = *((char *)v19 + i + 3);
    if ( v3 == complex_function(75, i + 93) )
      ++v15;
  }
  if ( v15 != 32 || (_BYTE)v20 )
    puts("Try again.");
  else
    puts("Good Job.");
  return 0;
}

​ 对比之前我们可以发现路径爆炸的点：

1
2
3
4
5
6
for ( i = 0; i <= 31; ++i )
  {
    v3 = *((char *)v19 + i + 3);
    if ( v3 == complex_function(75, i + 93) )
      ++v15;
  }

​ 在之前我们是通过增加条件约束和Hook函数避免路径爆炸，我们也可以尝试一下使用之前的方法，但是这题我们启用了Veritesting就变得简单了很多，不用过多的手动设定太多参数。

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
import angr
import claripy
import sys

def main(argv):
    path_to_binary = argv[1]
    project = angr.Project(path_to_binary)

    initial_state = project.factory.entry_state(
        add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                        angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
    )
    simulation = project.factory.simgr(initial_state, veritesting=True)

    def is_successful(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return 'Good Job.'.encode() in stdout_output
    
    def should_abort(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return 'Try again.'.encode() in stdout_output

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]
        solution = solution_state.posix.dumps(sys.stdin.fileno())
        print(solution.decode())
    else:
        raise Exception('Could not find the solution')

if __name__ == '__main__':
    main(sys.argv)

Veritesting

动态符号执行（DSE）和静态符号执行（SSE）一个为路径生成公式，一个为语句生成公式。前者生成公式时会产生很高的负载，但生成的公式很容易解；后者生成公式很容易，公式也能覆盖更多的路径，但是公式更长更难解。方法上的区别在于DSE会摘要路径汇合点上两条分支的情况，而SSE为两条分支fork两条独立的执行路径

SSE目前还不能对大规模的程序分析（如Cloud9+state merging），问题主要在于循环的表示、方程复杂度、缺少具体状态、和对syscall等的模拟。Veritesting可以在SSE和DSE之间切换，减少负载和公式求解难度，并解决静态方法需要摘要或其他方法才能处理的系统调用和间接跳转

简单来说就是Veritesting结合了静态符合执行与动态符号执行，减少了路径爆炸的影响，在angr里我们只要在构造模拟管理器时，启用Veritesting了就行

1
simulation = project.factory.simgr(initial_state, veritesting=True)

13_angr_static_binary

​ 此题与第一题的代码完全相同，最大的变化就是此题所有的函数都被静态编译进了程序中，就导致 angr 没法使用 simprocedure 来替换标准的库函数，就需要我们手动 hook 所需的函数：

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
import angr
import claripy
import sys

def main(agrv):
    path = agrv[1]
    project = angr.Project(path)
    init_state = project.factory.entry_state()

    project.hook(0x804ed40, angr.SIM_PROCEDURES['libc']['printf']())
    project.hook(0x804ed80, angr.SIM_PROCEDURES['libc']['scanf']())
    project.hook(0x804f350, angr.SIM_PROCEDURES['libc']['puts']())
    project.hook(0x8048d10, angr.SIM_PROCEDURES['glibc']['__libc_start_main']())

    simulation = project.factory.simgr(init_state, veritesting=True)

    def success(state):
        std_out = state.posix.dumps(sys.stdout.fileno())
        return 'Good Job.'.encode() in std_out
    
    def avoid(state):
        std_out = state.posix.dumps(sys.stdout.fileno())
        return 'Try again.'.encode() in std_out

    simulation.explore(find=success, avoid=avoid)

    if simulation.found:
        solution_state = simulation.found[0]
        solution = solution_state.posix.dumps(sys.stdin.fileno())
        print(solution.decode())
    else:
        raise Exception('could not find the solution')

if __name__ == '__main__':
    main(sys.argv)

静态编译

​ 不同于动态编译是将应用程序需要的模块都编译成动态链接库，启动程序（初始化）时，这些模块不会被加载，运行时用到哪个模块就调用哪个。静态编译就是在编译时，把所有模块都编译进可执行文件里，当启动这个可执行文件时，所有模块都被加载进来，反映在现实中就是程序体积会相对大一些。

​ 通常，Angr会自动地用工作速度快得多的 simprocedure 代替标准库函数，但是这题中库函数都已经因为静态编译成了静态函数了，angr 没法自动替换。所以需要手动Hook所有使用标准库的C函数，angr已经在 simprocedure 中为我们提供了这些静态函数, 这里列举一些常用的函数：

1
2
3
4
5
6
7
8
9
10
11
12
angr.SIM_PROCEDURES['libc']['malloc']
angr.SIM_PROCEDURES['libc']['fopen']
angr.SIM_PROCEDURES['libc']['fclose']
angr.SIM_PROCEDURES['libc']['fwrite']
angr.SIM_PROCEDURES['libc']['getchar']
angr.SIM_PROCEDURES['libc']['strncmp']
angr.SIM_PROCEDURES['libc']['strcmp']
angr.SIM_PROCEDURES['libc']['scanf']
angr.SIM_PROCEDURES['libc']['printf']
angr.SIM_PROCEDURES['libc']['puts']
angr.SIM_PROCEDURES['libc']['exit']
angr.SIM_PROCEDURES['glibc']['__libc_start_main']

我们选择需要使用的静态函数，并使用如下格式进行 hook：

project.hook(0x804ed40, angr.SIM_PROCEDURES['libc']['printf']())

在编写 hook 时有一个函数比较容易被忽略，那就是__libc_start_main。一个 linux 的 c 程序的启动包括：

  1. execve 开始执行
  2. execve 内部会把bin程序加载后，就把.interp指定的 动态加载器加载
  3. 动态加载器把需要加载的so都加载起来，特别的把 libc.so.6 加载
  4. 调用到libc.so.6里的__libc_start_main函数，真正开始执行程序
  5. libc_start_main做了一些事后，调用到main()函数

所以程序是一定需要用到__libc_start_main的。在我们手动 hook 完毕这些静态函数后，就可以让 angr 正常搜索路径去符号执行了。

14_angr_shared_library

此题是一个关于共享库的题目，将其拖入 IDA 分析可以发现他的关键函数无法被解析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
int __cdecl main(int argc, const char **argv, const char **envp)
{
  char s; // [esp+1Ch] [ebp-1Ch]
  unsigned int v5; // [esp+2Ch] [ebp-Ch]

  v5 = __readgsdword(0x14u);
  memset(&s, 0, 0x10u);
  print_msg();
  printf("Enter the password: ");
  __isoc99_scanf("%8s", &s);
  if ( validate(&s, 8) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

validate是一个外部导入函数，其真正的二进制代码不在源程序里，在它所处的库文件lib14_angr_shared_library.so里面。

我们用 IDA 分析lib14_angr_shared_library.so：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
_BOOL4 __cdecl validate(char *s1, int a2)
{
  char *v3; // esi
  char s2[20]; // [esp+4h] [ebp-24h] BYREF
  int j; // [esp+18h] [ebp-10h]
  int i; // [esp+1Ch] [ebp-Ch]

  if ( a2 <= 7 )
    return 0;
  for ( i = 0; i <= 19; ++i )
    s2[i] = 0;
  qmemcpy(s2, "PVBLVTFT", 8);
  for ( j = 0; j <= 7; ++j )
  {
    v3 = &s1[j];
    *v3 = complex_function(s1[j], j);
  }
  return strcmp(s1, s2) == 0;
}

可以看到加密过程和比较字符串都在其中，这题就需要我们使用 angr 去处理外部导入函数。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]

  base = 0x4000000
  project = angr.Project(path_to_binary, load_options={
    'main_opts' : {
      'base_addr' : base
    }
  })

  buffer_pointer = claripy.BVV(0x3000000, 32)

  validate_function_address = base + 0x6D7
  initial_state = project.factory.call_state(
                    validate_function_address,
                    buffer_pointer,
                    claripy.BVV(8, 32)
                  )

  password = claripy.BVS('password', 64)
  initial_state.memory.store(buffer_pointer, password)
  
  simulation = project.factory.simgr(initial_state)

  check_constraint_address = base + 0x783
  simulation.explore(find=check_constraint_address)

  if simulation.found:
    solution_state = simulation.found[0]

    solution_state.add_constraints(solution_state.regs.eax != 0)
    solution = solution_state.solver.eval(password, cast_to=bytes)
    print(solution.decode())
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

动态链接

​ 在Linux下使用GCC将源码编译成可执行文件的过程可以分解为4个步骤，分别是预处理（Prepressing）、编译（Compilation）、汇编（Assembly）和链接（Linking）。

​ 动态链接的基本思想是把程序按照模块拆分成相对独立的部分，在程序运行时才将它们链接在一起形成一个完整的程序，而不是像静态链接一样把所有的程序模块都连接成一个单独的可执行文件。ELF动态链接文件被称为动态共享对象（DSO，Dynamic Shared Object），简称共享对象，它们一般都是.so为扩展名的文件。相比静态链接，动态链接有两个优势，一是共享对象在磁盘和内存只有一份，节省了空间；二是升级某个共享模块时，只需要将目标文件替换，而无须将所有的程序重新链接。

​ 共享对象的最终装载地址在编译时是不确定的，而是在装载时，装载器根据当前地址空间的空闲情况，动态分配一块足够大小的虚拟地址空间给相应的共享对象。为了能够使共享对象在任意地址装载，在连接时对所有绝对地址的引用不作重定位，而把这一步推迟到装载时再完成，即装载时重定位。

​ 此题我们简单理解共享库都是是用位置无关的代码编译的，我们需要指定基址。共享库中的所有地址都是base + offset，其中offset是它们在文件中的偏移地址。

pre-binary 选项

如果想要对一个特定的二进制对象设置一些选项，CLE也能满足你的需求在加载二进制文件时可以设置特定的参数，使用 main_opts 和 lib_opts 参数进行设置：

  • backend – 指定 backend
  • base_addr – 指定基址
  • entry_point – 指定入口点
  • arch – 指定架构
1
2
# 例如：
angr.Project(path, main_opts={'backend': 'blob', 'arch': 'i386'}, lib_opts={'libc.so.6': {'backend': 'elf'}})

参数main_opts和lib_opts接收一个以python字典形式存储的选项组。main_opts接收一个形如{选项名1：选项值1，选项名2：选项值2……}的字典，而lib_opts接收一个库名到形如{选项名1:选项值1，选项名2:选项值2……}的字典的映射。

lib_opts是二级字典，原因是一个二进制文件可能加载多个库，而main_opts指定的是主程序加载参数，而主程序一般只有一个，因此是一级字典。

这些选项的内容因不同的后台而异，下面是一些通用的选项：

  • backend —— 使用哪个后台，可以是一个对象，也可以是一个名字(字符串)
  • custom_base_addr —— 使用的基地址
  • custom_entry_point —— 使用的入口点
  • custom_arch —— 使用的处理器体系结构的名字

所以我们这么构造此题脚本的第一个部分：

1
2
3
4
5
6
7
8
9
def main(argv):
  path_to_binary = argv[1]

  base = 0x4000000
  project = angr.Project(path_to_binary, load_options={
    'main_opts' : {
      'base_addr' : base
    }
  })

​ 接下来调用的是使用.call_state创建 state 对象，构造一个已经准备好执行validate函数的状态，所以我们需要设定好需要传入的参数（_BOOL4 __cdecl validate(char *s1, int a2)）。

​ 我们可以通过 BVV(value,size) 和 BVS( name, size) 接口创建位向量，先创建一个缓冲区buffer作为参数char *s1，因为设定的缓冲区地址在0x3000000，又因为32位程序里int类型为4字节，即32比特，故得：

1
buffer_pointer = claripy.BVV(0x3000000, 32)

从 IDA 中得到 validate的偏移量为0x6D7，然后因为需要比较的字符串长度为8，故利用BVV传入参数int a2，最后得到

1
2
3
buffer_pointer = claripy.BVV(0x3000000, 32)
validate_function_address = base + 0x6d7
initial_state = project.factory.call_state(validate_function_address, buffer_pointer, claripy.BVV(8, 32))

然后利用BVS创建一个符号位向量，作为符号化的传入字符串传入我们之前设定好的缓冲区地址中，这里继续利用memory.store接口:

1
2
password = claripy.BVS('password', 64)
initial_state.memory.store(buffer_pointer, password)

接下来题目注释里给出判断路径正确的方法有两种：

  1. hook 判断部分
  2. 搜索函数返回的地址去约束传递返回值的寄存器 eax

我们选择第二种：

1
2
3
4
5
6
7
 check_constraint_address = base + 0x783
 simulation.explore(find=check_constraint_address)

···

 solution_state.add_constraints(solution_state.regs.eax != 0)
 solution = solution_state.solver.eval(password, cast_to=bytes)

15_angr_arbitrary_read

拖入 IDA 分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
int __cdecl main(int argc, const char **argv, const char **envp)
{
  char v4; // [esp+Ch] [ebp-1Ch] BYREF
  char *s; // [esp+1Ch] [ebp-Ch]

  s = try_again;
  printf("Enter the password: ");
  __isoc99_scanf("%u %20s", &key, &v4);
  if ( key == 36134347 || key != 41810812 )
    puts(try_again);
  else
    puts(s);
  return 0;
}

​ 乍一看没有入手点，偷看一波武林秘籍，这十几道题都有一个统一的流程，就是正确的输入让他打印”Good Job.”但是此题却打印的是s。赶忙查看字符串窗口发现我们的”Good Job.”静静躺在 0x484F4A47那里。那么我们的目的就很明确了，就是让 s 所存储的地址指向该字符串，但是我们的输入是存储在 v4 的，难道 v4 与 s 有什么关系吗。我们查看他们的地址，发现 s 的地址刚好比 v4 的地址大 16 个字节，也就是说，我们可以利用栈溢出的特性去覆盖 s 的四字节数据（int 指针刚好四字节）。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary, auto_load_libs=False)
  initial_state = project.factory.entry_state()

  class ReplacementScanf(angr.SimProcedure):
    def run(self, format_string, param0, param1):
      scanf0 = claripy.BVS('scanf0', 32)      
      scanf1 = claripy.BVS('scanf1', 20*8)
      for char in scanf1.chop(bits=8):
        self.state.add_constraints(char >= 0x21, char <= 126)
      scanf0_address = param0
      self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
      scanf1_address = param1
      self.state.memory.store(scanf1_address, scanf1)
      self.state.globals['solutions'] = (scanf0, scanf1)

  scanf_symbol = '__isoc99_scanf'  # :string
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  def check_puts(state):

    puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=project.arch.memory_endness)

    if state.solver.symbolic(puts_parameter):
      good_job_string_address = 0x594e4257 # :integer, probably hexadecimal

      is_vulnerable_expression = puts_parameter == good_job_string_address # :boolean bitvector expression

      copied_state = state.copy()
      copied_state.add_constraints(is_vulnerable_expression)

      if copied_state.satisfiable():
        state.add_constraints(is_vulnerable_expression)
        return True
      else:
        return False
    else: # not state.solver.symbolic(???)
      return False

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    puts_address = 0x8048370
    if state.addr == puts_address:
      return check_puts(state)
    else:
      return False

  simulation.explore(find=is_successful)

  if simulation.found:
    solution_state = simulation.found[0]
    (scanf0, scanf1) = solution_state.globals['solutions']
    solution0 = (solution_state.solver.eval(scanf0))
    solution1 = (solution_state.solver.eval(scanf1,cast_to=bytes))
    print("{0} {1}".format(solution0, solution1.decode()))
  
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

​ 此题中，scanf 是多组输入，之前我们采用寄存器符号注入的方式来规避 angr 在此方面的短板，在此题中，我们直接使用 hook 技术，来用我们自定义的功能类似的函数代替 scanf 函数执行。

​ 这题我们需要确保字符串中的每个字符都是可打印的，这就需要我们添加新的条件约束，即约束每个字节的范围在ASCII码中，同时因为一个字符是8比特，故我们需要将scanf1这个符号位向量按8比特一组切分为一个字节一个字节。

1
2
for char in scanf1.chop(bits=8):
   self.state.add_constraints(char >= 0x21, char <= 126)

引入project.arch.memory_endness将符号位向量设置为小端序，并设置解集：

1
2
3
4
5
scanf0_address = param0
self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
scanf1_address = param1
self.state.memory.store(scanf1_address, scanf1)
self.state.globals['solutions'] = (scanf0, scanf1)

​ 我们需要一个验证函数求证我们求解出的状态是正确的输出状态，所以需要编写一个check_puts函数进行检查，我们主要是在检查puts函数调用时传入的参数s的值，这里有一个独特的地方我们检查的puts地址是PLT地址，因为有两个地方都调用了puts函数，而puts是一个外部导入函数，每次调用本质上都需要访问PLT表，所以我们直接捕获运行到puts的PLT地址的state做检查就行

获取数据段存放函数地址的那一小段代码称为PLT（Procedure Linkage Table）过程链接表

存放函数地址的数据段称为GOT（Global Offset Table）全局偏移表

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
def check_puts(state):

    puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=project.arch.memory_endness)

    if state.solver.symbolic(puts_parameter):
      good_job_string_address = 0x594e4257 # :integer, probably hexadecimal

      is_vulnerable_expression = puts_parameter == good_job_string_address # :boolean bitvector expression

      copied_state = state.copy()
      copied_state.add_constraints(is_vulnerable_expression)

      if copied_state.satisfiable():
        state.add_constraints(is_vulnerable_expression)
        return True
      else:
        return False
    else: # not state.solver.symbolic(???)
      return False

​ 这里我们需要对当前状态做一个拷贝，方便操作状态而不对原来的状态产生影响干扰，然后给状态添加约束条件，如果地址相等则返回正确。

1
2
3
4
5
6
7
8
9
10
copied_state = state.copy()
      copied_state.add_constraints(is_vulnerable_expression)

      if copied_state.satisfiable():
        state.add_constraints(is_vulnerable_expression)
        return True
      else:
        return False
    else: # not state.solver.symbolic(???)
      return False

16_angr_arbitrary_write

拖入 IDA 分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
int __cdecl main(int argc, const char **argv, const char **envp)
{
  char s[16]; // [esp+Ch] [ebp-1Ch] BYREF
  char *dest; // [esp+1Ch] [ebp-Ch]

  dest = unimportant_buffer;
  memset(s, 0, sizeof(s));
  strncpy(password_buffer, "PASSWORD", 0xCu);
  printf("Enter the password: ");
  __isoc99_scanf("%u %20s", &key, s);
  if ( key == 11604995 )
    strncpy(dest, s, 0x10u);
  else
    strncpy(unimportant_buffer, s, 0x10u);
  if ( !strncmp(password_buffer, "NDYNWEUJ", 8u) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

​ 跟上题类似，我们的输入似乎影响不到最后的判断，那就说明我们需要借助栈溢出的手段去更改指针，我们查看地址发现：password_buffer和key就差 16 个字节，也就是跟上题同理，栈溢出使得password_buffer指向比较字符串NDYNWEUJ即可。

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
75
76
77
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  initial_state = project.factory.entry_state()

  class ReplacementScanf(angr.SimProcedure):
    def run(self, format_string, param0, param1):
      scanf0 = claripy.BVS('scanf0', 32)

      scanf1 = claripy.BVS('scanf1', 20*8)

      for char in scanf1.chop(bits=8):
        self.state.add_constraints(char >= 0x21, char <= 126)

      scanf0_address = param0
      self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
      scanf1_address = param1
      self.state.memory.store(scanf1_address, scanf1)

      self.state.globals['solutions'] = (scanf0, scanf1)

  scanf_symbol = '__isoc99_scanf'  # :string
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  def check_strncpy(state):

    strncpy_dest = state.memory.load(state.regs.esp + 4, 4, endness=project.arch.memory_endness)
    strncpy_src = state.memory.load(state.regs.esp + 8, 4, endness=project.arch.memory_endness)	#获取地址
    strncpy_len = state.memory.load(state.regs.esp + 12, 4, endness=project.arch.memory_endness)

    src_contents = state.memory.load(strncpy_src, strncpy_len)	# 通过地址获取值

    if state.solver.symbolic(src_contents) and state.solver.symbolic(strncpy_dest):

      password_string =  'DVTBOGZL' # :string
      buffer_address = 0x4655544c # :integer, probably in hexadecimal

      does_src_hold_password = src_contents[-1:-64] == password_string	# 小端序

      does_dest_equal_buffer_address = strncpy_dest == buffer_address

      if state.satisfiable(extra_constraints=(does_src_hold_password, does_dest_equal_buffer_address)):
        state.add_constraints(does_src_hold_password, does_dest_equal_buffer_address)
        return True
      else:
        return False
    else: # not state.solver.symbolic(???)
      return False

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    strncpy_address = 0x8048410
    if state.addr == strncpy_address:
      return check_strncpy(state)
    else:
      return False

  simulation.explore(find=is_successful)

  if simulation.found:
    solution_state = simulation.found[0]
    (scanf0, scanf1) = solution_state.globals['solutions']
    solution0 = solution_state.solver.eval(scanf0)
    solution1 = solution_state.solver.eval(scanf1, cast_to=bytes)
    solution = '{} {}'.format(solution0, solution1.decode())
    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

17_angr_arbitrary_jump

拖入 IDA 分析：

1
2
3
4
5
6
7
int __cdecl main(int argc, const char **argv, const char **envp)
{
  printf("Enter the password: ");
  read_input();
  puts("Try again.");
  return 0;
}

​ 看到 scanf，并发现输入并不能直观地打印”Good Job”，所以我们很自然而然地想到使用栈溢出漏洞。我们在 Functions 视图里看到有一个函数名为：print_good，点进去一看，果然可以打印”Good Job”，那么目的一下就明确了，就是栈溢出覆盖返回地址使得程序去执行我们所需的函数。

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
import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  symbolic_input = claripy.BVS("input", 64*8)

  initial_state = project.factory.entry_state(
          stdin=symbolic_input,
          add_options = {
              angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
              angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
              }
          )

  simulation = project.factory.simgr(
    initial_state,
    save_unconstrained=True,
    stashes={
      'active' : [initial_state],
      'unconstrained' : [],
      'found' : [],
      'not_needed' : []
    }
  )

  def has_found_solution():
    return simulation.found

  def has_unconstrained_to_check():
    return simulation.unconstrained

  def has_active():
    return simulation.active

  while (has_active() or has_unconstrained_to_check()) and (not has_found_solution()):
    for unconstrained_state in simulation.unconstrained:

      simulation.move('unconstrained', 'found')

    simulation.step()

  if simulation.found:
    solution_state = simulation.found[0]

    solution_state.add_constraints(solution_state.regs.eip == 0x4d4c4749)

    for byte in symbolic_input.chop(bits=8):
      solution_state.add_constraints(
              byte >= 0x21,
              byte <= 126
      )

    solution = solution_state.solver.eval(symbolic_input,cast_to=bytes).decode()
    print(solution)
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

​ 当一条指令有太多可能的分支时，就会出现无约束状态。当指令指针完全是符号指针时，就会发生这种情况，这意味着用户输入可以控制计算机执行的代码的地址，例如此题存在的栈溢出漏洞就可以让我们的程序进入无约束状态。一般情况下，当Angr遇到不受约束的状态时，它会将其抛出。我们改变Angr的模拟引擎的默认设置，参数save_unconstrained=True时指定Angr不抛出不受约束的状态。相反，它会将它们移动到名为simul.com unconstrained的stashes 中。此外，我们将使用一些默认情况下不包含的stashes ，如’found’和’not_needed’。

  • active：程序仍能进一步执行
  • deadended：程序结束
  • errored：Angr执行中出现错误的状态
  • unconstrained：不受约束的状态
  • found：找到路径答案的状态
  • not_needed：所有其它情况
1
2
3
4
5
6
7
8
9
10
simulation = project.factory.simgr(
    initial_state,
    save_unconstrained=True,
    stashes={
      'active' : [initial_state],
      'unconstrained' : [],
      'found' : [],
      'not_needed' : []
    }
  )

接下来我们将定义四个函数来获得我们想要获得的程序状态

1
2
3
4
5
6
7
8
9
10
11
12
#检查无约束状态是否可利用
def check_vulnerable(state):
    return state.solver.symbolic(state.regs.eip)

def has_found_solution():
    return simulation.found
#检查是否还有未受约束的状态需要检查
def has_unconstrained_to_check():
    return simulation.unconstrained
#active是可以进一步探索的所有状态的列表
def has_active():
    return simulation.active

​ 我们之前一直使用的simulation.explore方法并不适合我们现在这种情况，因为find参数指定的方法不会在无约束状态下被调用，想要自己探索未约束情况下的二进制代码，我们需要自己编写解决方案:

1
2
3
4
5
6
while (has_active() or has_unconstrained_to_check()) and (not has_found_solution()):
    for unconstrained_state in simulation.unconstrained:

      simulation.move('unconstrained', 'found')

    simulation.step()
  • 版权声明： 本博客所有文章除特别声明外，著作权归作者所有。转载请注明出处！

扫一扫，分享到微信

微信分享二维码
  • Copyrights © 2022-2023 Syclover.Kama
  • 访问人数: | 浏览次数:

请我喝杯咖啡吧~

支付宝
微信