Angr 初学笔记

符号执行是什么？

符号执行（Symbolic Execution）是一种程序分析技术，它可以通过分析程序来得到让特定代码区域执行的输入。顾名思义，使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。[2]

符号执行，是一个可以遍历程序中所有可能路径的系统。

可能路径是什么，例如如下程序（攻防世界-Re-lucknum）：

这里的判断条件有两个可能路径，判断成立了走左边的路径，判断失败了走右边的路径，选择我们想要前往的可能路径，这条路径就是目标路径

那么符号是什么？

有点类似数学方程中的变量x，是一个变量而非一个确切的数值：x2 + 2x + 3 = 4

x的值取决于等式中的约束（constrain），符号的值则取决于执行路径（executeion path）中的约束

例如上例程序中的scanf输入的值就可以当成一个符号γ（符号注入），在执行路径中，我们想要到达目标路径（左边），得到的相应的约束就是γ=7，对约束进行求解，得到的答案就是前往目标路径的触发值

一个复杂点的情况的示例[1]：

要到达返回1的点，寻找执行路径，构造等式，就可以进行求解：

等式（约束，constrain）：

SECRET = 100
   input >= SECRET+88 
∧ input > SECRET+100
∧ input == SECRET68
∧ input < SECRET
∧ input <= SECRET+78
∧ input & 0x1
∧ input & 0x2
∧ input & 0x4

求出来的解，就是满足该执行路径的输入

简单来说，符号执行的过程就是：

注入符号：触发目标路径的变量
确定目标分支：目标路径所在地址
求解符号：收集前往目标路径的所有和符号相关的约束进行求解，拿到触发目标路径的输入值

Angr 执行路径

Angr是一个符号执行引擎，可以走遍程序中的每一个分支，可用于求解给定路径（和其他）约束的符号变量，搜索符号给定条件的程序状态

符号执行的两大基础：1. 执行路径，2. 符号

执行路径（寻找目标路径）

执行路径：程序可能从某个地方开始执行，到某个地方结束运行

在Angr里，执行路径的节点由一个SimState对象表示，该对象保存程序的状态和状态的历史记录，将状态链接在一起，就是执行路径

Angr使用simulation manager来保存和处理给定程序的一组可能路径，simulation manger提供了遍历程序生成可能路径or状态的功能

创建一组路径的过程：

Angr启动程序（在你指定的地方启动），这是第一个active的状态
在每一个active的状态里执行指令，直到到达分支点或者状态结束
每一个分支点，分割状态为多个状态，并添加到avtive状态里
重复2->4步骤直到我们找到目标路径，或所有状态全都结束

paths

状态爆炸（避免无用路径）

符号执行最大的问题之一就是状态爆炸

每次遇到一个if语句，可能的分支数就会翻倍，增长呈现指数级

当if语句过多时，要处理的状态数量就会变得极其巨大，以至于运行效率变得非常低

一个处理办法就是，避免一些状态，如下图

设置我们不想进入的分支，告诉程序走这里没用，不要从这里向下探索了，这样就能一定程度缓解状态爆炸的问题

避免状态就像寻找目标状态一样，当到达该路径，直接结束状态，让该状态不再继续使用

总结：Algorithm for Find and Avoid

载入二进制程序
指定开始执行的位置，创建simulation manager
当我们没有到达目标路径时：
1. 步进所有avtive的状态
2. 在每个active的状态上，判断我们的寻找条件（“should_accept_state”）是否成立，成立说明我们就找到了目标路径的状态，退出循环
3. 在每个active的状态上，判断我们的避免条件（“should_avoid_state”）是否成立，成立的话，将其状态标记为终止
4. 从avtive集合里移除标记为终止的状态

在Angr里完成这个事情只需要调用一个explore函数即可：（可以写指令地址，也可以写函数来判断是否是想要到达的地方）

simulation.explore(find=should_accept_path, avoid=should_avoid_path)
simulation.explore(find=0x80430a, avoid=0x9aa442)

该方法会将找到的路径添加到列表simulation.found里

示例：条件分支

示例程序反编译：

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

目标是要到达输出Good Job.的分支，避免到达Try again.的分支

脚本的编写：

import angr
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)
  initial_state = project.factory.entry_state()
  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

  # 让angr去探索状态，探索标准输出stdout会返回good job的，避免会返回try again的状态，成功的状态会保存在found列表里
  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)

Angr 符号

在一些示例中，Angr会在用户输入（stdin）时自动注入符号，我们也可以手动注入符号

Angr里的符号，使用Bitvectors来表示，bitvectors有一个大小（所表示内容的位的数量），可以表示为任何类型，常见的是表示为n位的整数或字符串

bitvectors和传统变量的区别就是，传统变量存储的是一个单一的值，bitvectors存储的是任何一个值（就像数学方程中的x）

例如：

对于8位的bitvector λ，有：( λ > 0, λ ≤ 4, λ mod 2 = 0 ) ∨ ( λ = 1 )

λ也会被如此保存起来，如果要具体化bitvector，可以拿到满足要求的值：1，2，4

关于符号的一些定义：

固定值的bitvector：只能表示1个值
符号化的bitvector：可以表示超过1个的值
不满足的bitvector：表示不了任何值
不固定的bitvector：可以表示任何值

约束求解

Angr内部使用z3（开源的约束求解器），具有这些功能：

找到bitvector的可能的多个值，最大值，最小值
确定bitvector是否是可满足的（是否有解）

我们注入的符号bitvector的大小需要和变量的大小一致，约束会被引擎通过给定路径来自动生成，约束也可以手动添加

就像编译器优化程序会进行常量传播一样，符号也会进行传播，当符号的值被传递给其他变量时，该变量也会被符号化（符号所有的约束也会跟着传播，约束也可以反向传播：约束可以添加给符号最后计算的结果上）

符号注入

对于简单的输入形式，angr可以自动完成符号注入

对于复杂的输入，需要手动进行操作，例如：复杂格式的字符串，文件，网络，UI交互等

示例：符号注入--寄存器

执行路径的初始状态里可以设置寄存器的初值，示例程序：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  __int64 user_input; // rax
  int v5; // [esp+4h] [ebp-14h]
  int v6; // [esp+8h] [ebp-10h]
  int v7; // [esp+Ch] [ebp-Ch]
  int v8; // [esp+Ch] [ebp-Ch]

  printf("Enter the password: ");
  user_input = get_user_input();
  v7 = HIDWORD(user_input);
  v5 = complex_function_1(user_input);
  v6 = complex_function_2();
  v8 = complex_function_3(v7);
  if ( v5 || v6 || v8 )
    puts("Try again.");
  else
    puts("Good Job.");
  return 0;
}

因为要跳过用户输入，从用户输入后面开始执行，所以需要分析给哪个寄存器赋哪个符号，查看反汇编：

main()
sub     esp, 0Ch
push    offset aEnterThePasswo ; "Enter the password: "
call    _printf
add     esp, 10h
call    get_user_input
mov     [ebp+var_14], eax
mov     [ebp+var_10], ebx
mov     [ebp+var_C], edx

get_user_input()
lea     ecx, [ebp+var_10]
push    ecx
lea     ecx, [ebp+var_14]
push    ecx
lea     ecx, [ebp+var_18]
push    ecx
push    offset aXXX     ; "%x %x %x"
call    ___isoc99_scanf
add     esp, 10h
mov     ecx, [ebp+var_18]
mov     eax, ecx
mov     ecx, [ebp+var_14]
mov     ebx, ecx
mov     ecx, [ebp+var_10]
mov     edx, ecx

可以看到这里通过scanf输入的数值依次被保存到了eax，ebx，edx里

编写脚本：

import angr
import claripy
import sys

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

  # 设置启动地址为执行完call get_user_input之后
  start_address = 0x80488c7  # :integer (probably hexadecimal)
  initial_state = project.factory.blank_state(addr=start_address)

  # 创建三个符号（bitvectors）
  password0_size_in_bits = 32  # :integer
  password0 = claripy.BVS('password0', password0_size_in_bits)

  password1_size_in_bits = 32  # :integer
  password1 = claripy.BVS('password1', password1_size_in_bits)

  password2_size_in_bits = 32  # :integer
  password2 = claripy.BVS('password2', password2_size_in_bits)

  # 将符号赋值给初始状态的寄存器
  initial_state.regs.eax = password0
  initial_state.regs.ebx = password1
  initial_state.regs.edx = password2

  # 创建simgr
  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]

    # 存在多个解，只要一个解的话，使用eval进行求解
    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)
    solution2 = solution_state.solver.eval(password2)

    # Aggregate and format the solutions you computed above, and then print
    # the full string. Pay attention to the order of the integers, and the
    # expected base (decimal, octal, hexadecimal, etc).
    solution = ' '.join(map('{:x}'.format, [ solution0, solution1, solution2 ]))  # :string
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

示例：符号注入--全局内存

符号位于全局内存的话，可以跳过用户输入，直接给这个内存赋值为符号来进行符号执行

示例程序：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+Ch] [ebp-Ch]

  memset(user_input, 0, 0x21u);
  printf("Enter the password: ");
  __isoc99_scanf("%8s %8s %8s %8s", user_input, &unk_A1BA1C8, &unk_A1BA1D0, &unk_A1BA1D8);
  for ( i = 0; i <= 31; ++i )
    *(_BYTE *)(i + 169583040) = complex_function(*(char *)(i + 169583040), i);
  if ( !strncmp(user_input, "NJPURZPCDYEAXCSJZJMPSOMBFDDLHBVN", 0x20u) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

求解脚本：

import angr
import sys


def main(argv):
    bin_path = argv
    p = angr.Project(bin_path)

    # 跳过scanf函数的开始地址
    start_address = 0x08048601
    init_state = p.factory.blank_state(addr=start_address)

    # symbolic memory，创建符号
    p1 = init_state.solver.BVS('p1', 64)
    p2 = init_state.solver.BVS('p2', 64)
    p3 = init_state.solver.BVS('p3', 64)
    p4 = init_state.solver.BVS('p4', 64)

    # 变量所在的内存
    p1_addr = 0x0A1BA1C0
    p2_addr = 0x0A1BA1C8
    p3_addr = 0x0A1BA1D0
    p4_addr = 0x0A1BA1D8

    # 将符号填入指定内存
    init_state.memory.store(p1_addr, p1)
    init_state.memory.store(p2_addr, p2)
    init_state.memory.store(p3_addr, p3)
    init_state.memory.store(p4_addr, p4)

    sm = p.factory.simgr(init_state)

    isgood = lambda x:b"Good" in x.posix.dumps(1)
    isbad = lambda x:b"Try" in x.posix.dumps(1)

    sm.explore(find=isgood, avoid=isbad)
    if sm.found:
        found_state = sm.found[0]
        passwd1 = found_state.solver.eval(p1, cast_to=bytes).decode('utf-8')
        passwd2 = found_state.solver.eval(p2, cast_to=bytes).decode('utf-8')
        passwd3 = found_state.solver.eval(p3, cast_to=bytes).decode('utf-8')
        passwd4 = found_state.solver.eval(p4, cast_to=bytes).decode('utf-8')
        print("soluation: {} {} {} {}".format(passwd1, passwd2, passwd3, passwd4))


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

示例：符号注入--栈

对于栈，需要我们手动创建栈帧，来向栈里填充符号

示例程序：

int handle_user()
{
  int v1; // [esp+8h] [ebp-10h] BYREF
  int v2[3]; // [esp+Ch] [ebp-Ch] BYREF

  __isoc99_scanf("%u %u", v2, &v1);
  v2[0] = complex_function0(v2[0]);
  v1 = complex_function1(v1);
  if ( v2[0] == 1999643857 && v1 == -1136455217 )
    return puts("Good Job.");
  else
    return puts("Try again.");
}

关键部分反汇编：

.text:08048682 lea     eax, [ebp+var_10]
.text:08048685 push    eax
.text:08048686 lea     eax, [ebp+var_C]
.text:08048689 push    eax
.text:0804868A push    offset aUU      ; "%u %u"
.text:0804868F call    ___isoc99_scanf
.text:08048694 add     esp, 10h
.text:08048697 mov     eax, [ebp+var_C]
.text:0804869A sub     esp, 0Ch
.text:0804869D push    eax

可以看到，变量所在位置是ebp+c，ebp+10的地方

解题脚本：

import angr
import sys


def main(argv):
    bin_path = argv
    p = angr.Project(bin_path)

    # 开始地址
    start_address = 0x08048697
    init_state = p.factory.blank_state(addr=start_address)

    # symbolic stack
    # 初始化栈，让栈顶的位置指向变量
    padding_size = 8
    init_state.stack_push(init_state.regs.ebp)
    init_state.regs.ebp = init_state.regs.esp
    init_state.regs.esp -= padding_size
  
    # 创建符号，将符号参数push到栈里
    pass1 = init_state.solver.BVS('pass1', 32)
    pass2 = init_state.solver.BVS('pass2', 32)

    init_state.stack_push(pass1)
    init_state.stack_push(pass2)

    sm = p.factory.simgr(init_state)

    isgood = lambda x: b"Good" in x.posix.dumps(1)
    isbad = lambda x: b"Try" in x.posix.dumps(1)

    sm.explore(find=isgood, avoid=isbad)
    if sm.found:
        found_state = sm.found[0]
        passwd1 = found_state.solver.eval(pass1)
        passwd2 = found_state.solver.eval(pass2)
        print("soluation: {} {}".format(passwd1, passwd2))


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

示例：符号注入--动态内存

对于动态内存申请，每次申请得到的地址都是变化的，没法在运行前得到该地址

但是可以跳过动态内存申请，修改指向该内存的指针，指向我们设置的内存区域，来模拟动态内存

示例：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  char *v3; // ebx
  char *v4; // ebx
  int v6; // [esp-10h] [ebp-1Ch]
  int i; // [esp+0h] [ebp-Ch]

  buffer0 = (char *)malloc(9u);
  buffer1 = (char *)malloc(9u);
  memset(buffer0, 0, 9u);
  memset(buffer1, 0, 9u);
  printf("Enter the password: ");
  __isoc99_scanf("%8s %8s", buffer0, buffer1, v6);
  for ( i = 0; i <= 7; ++i )
  {
    v3 = &buffer0[i];
    *v3 = complex_function(buffer0[i], i);
    v4 = &buffer1[i];
    *v4 = complex_function(buffer1[i], i + 32);
  }
  if ( !strncmp(buffer0, "UODXLZBI", 8u) && !strncmp(buffer1, "UAORRAYF", 8u) )
    puts("Good Job.");
  else
    puts("Try again.");
  free(buffer0);
  free(buffer1);
  return 0;
}

输入部分的反汇编：

.text:08048679 83 C4 10                      add     esp, 10h
.text:0804867C 8B 15 AC C8 BC 0A             mov     edx, ds:buffer1
.text:08048682 A1 A4 C8 BC 0A                mov     eax, ds:buffer0
.text:08048687 83 EC 04                      sub     esp, 4
.text:0804868A 52                            push    edx
.text:0804868B 50                            push    eax
.text:0804868C 68 43 88 04 08                push    offset a8s8s                    ; "%8s %8s"
.text:08048691 E8 CA FD FF FF                call    ___isoc99_scanf
.text:08048691
.text:08048696 83 C4 10                      add     esp, 10h
.text:08048699 C7 45 F4 00 00 00 00          mov     [ebp+var_C], 0

.bss:0ABCC8A4 ?? ?? ?? ??                   buffer0 dd ?                            ; DATA XREF: main+1F↑w
.bss:0ABCC8AC ?? ?? ?? ??                   buffer1 dd ?

可以看到，这里用全局变量保存动态内存指针，通过修改全局内存的方式去修改该指针指向我们指定去内存即可

解题脚本：

import angr
import sys


def main(argv):
    bin_path = argv[1]
    p = angr.Project(bin_path)
  
    # 指向scanf之后的地址
    start_address = 0x08048699
    init_state = p.factory.blank_state(addr=start_address)

    # symbolic dynamic memory 创建符号向量
    p1 = init_state.solver.BVS('p1', 64)
    p2 = init_state.solver.BVS('p2', 64)

    # 栈里的地址
    p1_addr = 0x7fff0000 - 0x100
    p2_addr = 0x7fff0000 - 0x200

    # 全局变量
    buffer0 = 0x0ABCC8A4
    buffer1 = 0x0ABCC8AC

    init_state.memory.store(buffer0, p1_addr, endness=p.arch.memory_endness)
    init_state.memory.store(buffer1, p2_addr, endness=p.arch.memory_endness)

    init_state.memory.store(p1_addr, p1)
    init_state.memory.store(p2_addr, p2)

    sm = p.factory.simgr(init_state)

    isgood = lambda x:b"Good" in x.posix.dumps(1)
    isbad = lambda x:b"Try" in x.posix.dumps(1)

    sm.explore(find=isgood, avoid=isbad)
    if sm.found:
        found_state = sm.found[0]
        passwd1 = found_state.solver.eval(p1, cast_to=bytes).decode('utf-8')
        passwd2 = found_state.solver.eval(p2, cast_to=bytes).decode('utf-8')
        print("soluation: {} {}".format(passwd1, passwd2))



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

示例：符号注入--文件系统

示例：

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(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 + 0x804A0A0) = complex_function(*(char *)(i + 0x804A0A0), i);
  if ( strncmp(buffer, "AQWLCTXB", 9u) )
  {
    puts("Try again.");
    exit(1);
  }
  puts("Good Job.");
  exit(0);
}

这里通过使用angr的接口来模拟一个文件，设置文件的内容为符号即可

解题脚本：

import angr
import sys


def main(argv):
    bin_path = argv[1]
    p = angr.Project(bin_path)

    start_address = 0x080488D6
    init_state = p.factory.blank_state(addr=start_address)

    # symbolic file
    # 文件信息；名称，大小
    filename = "OJKSQYDP.txt"
    filesize = 0x40

    # 文件内容（向量）
    password = init_state.solver.BVS('password', filesize * 8)
  
    # angr插入模拟文件
    sim_file = angr.storage.SimFile(filename, content=password, size=filesize)
    init_state.fs.insert(filename, sim_file)

    sm = p.factory.simgr(init_state)

    isgood = lambda x: b"Good" in x.posix.dumps(1)
    isbad = lambda x: b"Try" in x.posix.dumps(1)

    sm.explore(find=isgood, avoid=isbad)
    if sm.found:
        found_state = sm.found[0]
        passwd1 = found_state.solver.eval(password, cast_to=bytes).decode('utf-8')
        print("soluation: {}".format(passwd1))


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

Angr Hook

当出现一些函数，里面的循环里有分支，例如：

_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 )                    // a2 = 16
  {
    if ( *(_BYTE *)(i + a1) == *(_BYTE *)(i + 0x804A040) )
      ++v3;
  }
  return v3 == a2;
}

这里有迭代16次，每次里面都有分支，那对于这个循环，就会出现2的16次方个状态，对于这种情况可以使用Angr的Hook的方式来跳过这个函数，执行我们的hook代码，Hook执行流程示意图：

这种Hook主要用于：

在执行的中间注入符号
取代复杂函数
取代Angr不支持的指令

示例--Hook

示例程序：

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

解题脚本：

import angr
import sys
import claripy


def main(argv):
    bin_path = argv[1]
    p = angr.Project(bin_path)

    init_state = p.factory.entry_state()

    # deal with path explosion by hook
    check_addr = 0x080486B3
    check_skip_size = 5		# 跳过执行指令的字节数，这里是跳过了原本的call指令，直接执行完hook函数进入到call之后执行了

    # hook函数的写法
    @p.hook(check_addr, length=check_skip_size)
    def check_hook(state: angr.SimState):
        user_input_addr = 0x0804A054
        user_input_length = 0x10

	# 这里没有自己创建符号注入，因为Angr对于简单的用户输入可以自动创建
        # 获取自动创建的符号的值
	user_input_bvs = state.memory.load(user_input_addr, user_input_length)
        desired_string = "XYMKBKUHNIQYNQXE"

	# 设置函数的返回值，依然是个bitvector，不过是具体的值，所以是BVV
        state.regs.eax = claripy.If(
            user_input_bvs == desired_string,
            claripy.BVV(1, 32),
            claripy.BVV(0, 32)
        )

    is_good = lambda x:b"Good" in x.posix.dumps(1)
    is_bad = lambda x:b"Try" in x.posix.dumps(1)

    sm = p.factory.simgr(init_state)
    sm.explore(find=is_good, avoid=is_bad)
    if sm.found:
        found_state = sm.found[0]
        passwd = found_state.posix.dumps(0).decode("utf-8")
        print(f"solution: {passwd}")


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

SimProcedure

SimProcedure是Angr提供的一种更加pythonic的方式来Hook复杂函数，这种Hook，Hook的是函数内部，不管在哪里调用函数，都会进入Hook函数里

Angr里有通过SimProcedure的libc函数的重新实现

示例--SimProcedure

示例程序：

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((int)s, 0x10u) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

该程序存在平坦化干扰，所以在反汇编界面看起来是这样的：

存在大量执行相同指令的分支，地址各不相同，如果使用之前那种hook方式，就太麻烦了，直接Hook函数内部，不管在哪里调用都能走Hook流程

解题代码：

#!/bin/python3
import sys

import angr
import claripy


def main(argv):
    bin_path = argv[1]
    p = angr.Project(bin_path)

    init_state = p.factory.entry_state()

    # 需要定义一个类，继承angr.SimProcedure
    class my_Sim_Procedure(angr.SimProcedure):
	# 执行hook函数，实际上执行的该类的run函数，参数固定第一个为self，后面的参数需要和原本的函数一致
	# 参数的类型会是bitvector
        def run(self, user_input, user_input_length):
            # get angr's input bvs
            angr_bvs = self.state.memory.load(
                user_input,
                user_input_length
            )
            desire = "ORSDDWXHZURJRBDH"
	    # 通过return的方式进行返回，而非设置eax
            return claripy.If(
                angr_bvs == desire,
                claripy.BVV(1, 32),
                claripy.BVV(0, 32)
            )

    # 需要Hook的函数的符号名称
    check_symbol = "check_equals_ORSDDWXHZURJRBDH"
    # 执行Hook操作
    p.hook_symbol(check_symbol, my_Sim_Procedure())

    sm = p.factory.simgr(init_state)

    is_good = lambda x:b"Good" in x.posix.dumps(1)
    is_bad = lambda x:b"Try" in x.posix.dumps(1)

    sm = p.factory.simgr(init_state)
    sm.explore(find=is_good, avoid=is_bad)
    if sm.found:
        found_state = sm.found[0]
        passwd = found_state.posix.dumps(0).decode("utf-8")
        print(f"solution: {passwd}")


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

示例：静态链接文件的处理

Angr会自动替换动态链接的libc库函数为自己重新实现的libc库函数，对于静态链接的程序来说，Angr跑到库函数里执行很浪费时间，会加大时间开销，可能导致状态爆炸，所以需要手动Hook他们为Angr内置的重写的libc函数

示例程序：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+1Ch] [ebp-3Ch]
  int j; // [esp+20h] [ebp-38h]
  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, "PYIEFPIC", 8);
  printf("Enter the password: ");
  _isoc99_scanf("%8s", s1);
  for ( j = 0; j <= 7; ++j )
    s1[j] = complex_function(s1[j], j);
  if ( !strcmp(s1, s2) )
    puts("Good Job.");
  else
    puts("Try again.");
  return 0;
}

这里的qmemcpy是内联实现，对于其他的函数printf，puts，strcmp，scanf，需要手动hook，哦对，还有glibc的_libc_start_main函数

解题脚本：

import sys
import angr


def main(argv):
    bin_path = argv[1]
    p = angr.Project(bin_path)
    init_state = p.factory.entry_state()

    # 动态链接的程序angr会自动hook库函数，对于静态链接的，则需要手动hook
    printf_addr = 0x0804ED40
    scanf_addr = 0x0804ED80
    strcmp_addr = 0x08048280
    puts_addr = 0x0804F350
    __libc_start_main_addr = 0x08048D10

    p.hook(printf_addr, angr.SIM_PROCEDURES['libc']['printf']())
    p.hook(scanf_addr, angr.SIM_PROCEDURES['libc']['scanf']())
    p.hook(strcmp_addr, angr.SIM_PROCEDURES['libc']['strcmp']())
    p.hook(puts_addr, angr.SIM_PROCEDURES['libc']['puts']())
    p.hook(__libc_start_main_addr, angr.SIM_PROCEDURES['glibc']['__libc_start_main']())

    is_good = lambda x:b"Good" in x.posix.dumps(1)
    is_bad = lambda x:b"Try" in x.posix.dumps(1)

    sm = p.factory.simgr(init_state)
    sm.explore(find=is_good, avoid=is_bad)

    if sm.found:
        found_state = sm.found[0]
        print(found_state.posix.dumps(0))


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

示例：动态链接库

对于动态链接库，可以直接使用Angr去执行库里的函数

示例代码：

.text:000006D7                               ; _BOOL4 __cdecl validate(char *s1, int)
.text:000006D7                               public validate
.text:000006D7                               validate proc near                      ; DATA XREF: LOAD:00000250↑o
.text:000006D7
.text:000006D7                               s2= byte ptr -24h
.text:000006D7                               var_10= dword ptr -10h
.text:000006D7                               var_C= dword ptr -0Ch
.text:000006D7                               s1= dword ptr  8
.text:000006D7                               arg_4= dword ptr  0Ch
.text:000006D7
.text:000006D7                               ; __unwind {
.text:000006D7 55                            push    ebp
.text:000006D8 89 E5                         mov     ebp, esp
.text:000006DA 56                            push    esi
.text:000006DB 53                            push    ebx
.text:000006DC 83 EC 20                      sub     esp, 20h
.text:000006DF E8 1C FE FF FF                call    __x86_get_pc_thunk_bx
.text:000006DF
.text:000006E4 81 C3 1C 19 00 00             add     ebx, (offset _GLOBAL_OFFSET_TABLE_ - $)
.text:000006EA 83 7D 0C 07                   cmp     [ebp+arg_4], 7
.text:000006EE 7F 0A                         jg      short loc_6FA
.text:000006EE
.text:000006F0 B8 00 00 00 00                mov     eax, 0
.text:000006F5 E9 83 00 00 00                jmp     loc_77D
.text:000006F5
.text:000006FA                               ; ---------------------------------------------------------------------------
.text:000006FA
.text:000006FA                               loc_6FA:                                ; CODE XREF: validate+17↑j
.text:000006FA C7 45 F4 00 00 00 00          mov     [ebp+var_C], 0
.text:00000701 EB 0F                         jmp     short loc_712
.text:00000701
.text:00000703                               ; ---------------------------------------------------------------------------
.text:00000703
.text:00000703                               loc_703:                                ; CODE XREF: validate+3F↓j
.text:00000703 8D 55 DC                      lea     edx, [ebp+s2]
.text:00000706 8B 45 F4                      mov     eax, [ebp+var_C]
.text:00000709 01 D0                         add     eax, edx
.text:0000070B C6 00 00                      mov     byte ptr [eax], 0
.text:0000070E 83 45 F4 01                   add     [ebp+var_C], 1
.text:0000070E
.text:00000712
.text:00000712                               loc_712:                                ; CODE XREF: validate+2A↑j
.text:00000712 83 7D F4 13                   cmp     [ebp+var_C], 13h
.text:00000716 7E EB                         jle     short loc_703
.text:00000716
.text:00000718 8D 45 DC                      lea     eax, [ebp+s2]
.text:0000071B C7 00 50 56 42 4C             mov     dword ptr [eax], 'LBVP'
.text:00000721 C7 40 04 56 54 46 54          mov     dword ptr [eax+4], 'TFTV'
.text:00000728 C7 45 F0 00 00 00 00          mov     [ebp+var_10], 0
.text:0000072F EB 2C                         jmp     short loc_75D
.text:0000072F
.text:00000731                               ; ---------------------------------------------------------------------------
.text:00000731
.text:00000731                               loc_731:                                ; CODE XREF: validate+8A↓j
.text:00000731 8B 55 F0                      mov     edx, [ebp+var_10]
.text:00000734 8B 45 08                      mov     eax, [ebp+s1]
.text:00000737 8D 34 02                      lea     esi, [edx+eax]
.text:0000073A 8B 55 F0                      mov     edx, [ebp+var_10]
.text:0000073D 8B 45 08                      mov     eax, [ebp+s1]
.text:00000740 01 D0                         add     eax, edx
.text:00000742 0F B6 00                      movzx   eax, byte ptr [eax]
.text:00000745 0F BE C0                      movsx   eax, al
.text:00000748 83 EC 08                      sub     esp, 8
.text:0000074B FF 75 F0                      push    [ebp+var_10]
.text:0000074E 50                            push    eax
.text:0000074F E8 6C FD FF FF                call    _complex_function
.text:0000074F
.text:00000754 83 C4 10                      add     esp, 10h
.text:00000757 88 06                         mov     [esi], al
.text:00000759 83 45 F0 01                   add     [ebp+var_10], 1
.text:00000759
.text:0000075D
.text:0000075D                               loc_75D:                                ; CODE XREF: validate+58↑j
.text:0000075D 83 7D F0 07                   cmp     [ebp+var_10], 7
.text:00000761 7E CE                         jle     short loc_731
.text:00000761
.text:00000763 83 EC 08                      sub     esp, 8
.text:00000766 8D 45 DC                      lea     eax, [ebp+s2]
.text:00000769 50                            push    eax                             ; s2
.text:0000076A FF 75 08                      push    [ebp+s1]                        ; s1
.text:0000076D E8 2E FD FF FF                call    _strcmp
.text:0000076D
.text:00000772 83 C4 10                      add     esp, 10h
.text:00000775 85 C0                         test    eax, eax
.text:00000777 0F 94 C0                      setz    al
.text:0000077A 0F B6 C0                      movzx   eax, al
.text:0000077A
.text:0000077D
.text:0000077D                               loc_77D:                                ; CODE XREF: validate+1E↑j
.text:0000077D 8D 65 F8                      lea     esp, [ebp-8]
.text:00000780 5B                            pop     ebx
.text:00000781 5E                            pop     esi
.text:00000782 5D                            pop     ebp
.text:00000783 C3                            retn

解题脚本：

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', 8 * 8)
    initial_state.memory.store(buffer_pointer, password)

    simulation = project.factory.simgr(initial_state)

    # 到执行完该函数结束
    check_constraint_address = base + 0x77D
    simulation.explore(find=check_constraint_address)

    if simulation.found:
        solution_state = simulation.found[0]
	# 从结果里找出返回eax为1的结果，并打印
        solution_state.add_constraints(solution_state.regs.eax != 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)

Veritesting

Veritesting算法是CMU开发的，通过合并分支来减少状态爆炸

参考资料

‍

菜单

分享

Angr 初学笔记

Angr 初学笔记

符号执行是什么？

Angr 执行路径

执行路径（寻找目标路径）

状态爆炸（避免无用路径）

总结：Algorithm for Find and Avoid

示例：条件分支

Angr 符号

约束求解

符号注入

示例：符号注入--寄存器

示例：符号注入--全局内存

示例：符号注入--栈

示例：符号注入--动态内存

示例：符号注入--文件系统

Angr Hook

示例--Hook

SimProcedure

示例--SimProcedure

示例：静态链接文件的处理

示例：动态链接库

Veritesting

参考资料

评论

【置顶】本博客的使用指南&更新计划（2024.4更新）

[HTB] re - Simple Encryptor

osu!gaming CTF 2024 (2 pwn)

[libc 2.35 源码学习] IO_FILE 篇 - 任意地址读&写

[libc 2.35 源码学习] IO_FILE 篇 - vtable & IO_validate_vtable

[libc 2.35 源码学习] IO_FILE 篇 - 相关结构体

[libc 2.35 源码学习] IO_FILE 篇 - fclose

[libc 2.35 源码学习] IO_FILE 篇 - fwrite

[libc 2.35 源码学习] IO_FILE 篇 - fread

[libc 2.35 源码学习] IO_FILE 篇 - fopen