Angr大法好

[TOC]

符号执行

简单的来说，符号执行就是在运行程序时，用符号去替代真实值。符号执行有什么好处呢？当使用真实值执行程序时，我们能遍历的程序路径只有一条，而使用符号执行，由于符号的灵活性（可变）我们就可以利用这一特性，尽可能地将程序的每一条路径遍历，这样的话，必定存在至少一条能够输出正确结果的分支。每一条分支的结果都可以表示为一个离散关系式，离散关系式的话我们使用约束求解引擎即可分析出正确结果。（在我看来就是去遍历每一条路径，就是枚举）

比如对于下面这个程序：符号执行不会给a,b赋真实的值，而是给他们一个未知符号a=x,b=y然后向下执行，比如我们想要执行win函数，那么最后就要求解 ((3 + x) * 2) * 2 + 4 = y 这个约束条件，而这里明显是解不出来的，所以采用动态的符号执行，也就是给a或b赋一个具体值

#include <stdio.h>

void win(){
        printf("You win!\n");
}
void lose(){
        printf("Lose!\n");
}

int main(int argc, char *argv[]){
        int a, b, c, d;
        scanf("%d%d", &a, &b);
        c = 3 + a;
        d = 2 * c;
        if(d * 2 + 4 == b) win();
        else lose();
        return 0;
}

当然问题也很明显，因为angr就是遍历所有路径，那么时间复杂度就会很高，换句话说，当我们的程序存在大量循环时，因为符号执行会尽量遍历所有的路径，所以每次循环之后会形成至少两个分支，当循环的次数足够多时，就会造成路径爆炸，整个机器的内存会被耗尽。

所有我们可以添加适当的约束去减小路径的遍历数量。（也可以类比有效性剪枝）

Angr 使用基础

import angr

def main():
    p = angr.Project(bin_filename,auto_load_libs=True)
    simgr = p.factory.simulation_manager(p.factory.full_init_state())
    simgr.explore(find=to_visite_address, avoid=to_avoid_address)

    found_state = simgr.found[0]
    return found_state.posix.dumps(0).strip(b'\0\n')

if __name__ == '__main__':
    print(main())

angr.Project()：创建一个工程，第一个参数为二进制文件名，第二个参数为是否加载文件相关依赖；该工程 p 包含许多属性，如 文件名p.filename，文件框架p.arch等待。

p.factory.full_init_state()：会返回一个初始化状态，也可以使用p.factory.entry_state()默认main()

p.factory.simulation_manager()：模拟执行，可以简写为p.factory.simgr()

simgr.explore()：这个函数就是去找到满足约束条件的路径；find参数表示经过该地址，avoid表示不经过该地址

simgr.found：是一个数组，表示找到的状态

found_state.posix.dump(0)：想要表示到达该状态，我们需要的输入

found_state.posix.dump(1)：表示输出

然后我们跟着https://github.com/jakespringer/angr_ctf这个项目学习Angr的基本使用方法，具体的函数具体用到具体学

00_angr_find

程序很简单，输入密码，经过complex_function函数处理后与特定字符串比较：

则我们explore时，find=‘Good Job.’的地址，avoid=‘Try again.’的地址

int __cdecl main(int argc, const char **argv, const char **envp)
{
  int i; // [esp+1Ch] [ebp-1Ch]
  char s1[9]; // [esp+23h] [ebp-15h] BYREF
  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;
}

#exp.py:
import angr
#创建工程
proj = angr.Project('./00_angr_find', auto_load_libs = False)
#得到一个初始化状态（这个状态是从main()函数开始执行）
init_state = proj.factory.entry_state()
#初始化一个仿真器（模拟器）
sim = proj.factory.simulation_manager(init_state)
#explore
sim.explore(find = 0x08048678, avoid =  0x08048666)
#得到找到的状态数组
found_states = sim.found
#判断是否找到，即数组是否为空
if found_states:
    #输出要到达该状态的输入
    ans = found_states[0].posix.dumps(0)
    print(ans)
else:
    print("Can't find solution!")
#passwod：JXWVXRKX

01_angr_avoid

这个跟第0个差不多，但是应该加了很多花指令；所以这里avoid的值应该是avoid_me这个函数，不然要跑非常久

import angr
proj = angr.Project('./01_angr_avoid', auto_load_libs = False)
init_state = proj.factory.entry_state()
sim = proj.factory.simulation_manager(init_state)
sim.explore(find = 0x080485E0 , avoid = 0x080485A8)
found_states = sim.found
if found_states:
    ans = found_states[0].posix.dumps(0)
    print(ans)
else:
    print("Can't find solution!")

02_angr_find_condition

程序跟上面两个差不多，只是换一个方式

上面两个 explore 中的 find、avoid 参数都是地址，其实也可以传入一个布尔值返回类型的函数

#exp.py
#python3 exp.py filename
import angr
import sys

def exp(argv):
    bin_name = argv[1]
    proj = angr.Project(bin_name, auto_load_libs = False)
    init_state = proj.factory.entry_state()
    simgr = proj.factory.simgr(init_state)

    def is_good(state):
        return b'Good Job.' in state.posix.dumps(1)

    def is_bad(state):
        return b'Try again.' in state.posix.dumps(1)

    simgr.explore(find = is_good, avoid = is_bad)

    if simgr.found:
        found_state = simgr.found[0]
        ans = found_state.posix.dumps(0)
        print(ans)
    else:
        print("Can't find solution!")

if __name__ == "__main__":
    exp(sys.argv)

3~4 是针对 scanf 这个函数的，由于之前的 angr 版本不能处理 scanf 接收多个参数的情况，即scanf(“%d %d”)等待类似情况。既然不能处理 scanf 函数接收多个参数，那么我们自己参数放进 scanf 对应的地址中，然后跳过 scanf 函数不就行了；注3-5直接用上面的方法也可以解，新版的angr是可以处理scanf多个参数的

03_angr_symbolic_registers

03 中 scanf 接收参数后会把参数放在寄存器中，所以我们得把对应的寄存器给符号化

main 函数如下：通过 get_user_input 函数获得用户的三个输入，然后进行处理比对

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

get_user_input 函数如下：该函数通过 scanf(“%x %x %x”)读取三个参数，这里我们看下汇编代码

int get_user_input()
{
  int v1; // [esp+0h] [ebp-18h] BYREF
  int v2; // [esp+4h] [ebp-14h] BYREF
  int v3[4]; // [esp+8h] [ebp-10h] BYREF

  v3[1] = __readgsdword(0x14u);
  __isoc99_scanf("%x %x %x", &v1, &v2, v3);
  return v1;
}

get_user_input 汇编代码：可以看到scanf读取用户输入后，最终把参数依次放到了 eax、ebc、edx 寄存器中；然后我们在看下 main 的反汇编

.text:0804890C 55                            push    ebp
.text:0804890D 89 E5                         mov     ebp, esp
.text:0804890F 83 EC 18                      sub     esp, 18h
.text:08048912 65 8B 0D 14 00 00 00          mov     ecx, large gs:14h
.text:08048919 89 4D F4                      mov     [ebp+var_C], ecx
.text:0804891C 31 C9                         xor     ecx, ecx
.text:0804891E 8D 4D F0                      lea     ecx, [ebp+var_10]
.text:08048921 51                            push    ecx
.text:08048922 8D 4D EC                      lea     ecx, [ebp+var_14]
.text:08048925 51                            push    ecx
.text:08048926 8D 4D E8                      lea     ecx, [ebp+var_18]
.text:08048929 51                            push    ecx
.text:0804892A 68 93 8A 04 08                push    offset aXXX           ; "%x %x %x"
.text:0804892F E8 9C FA FF FF                call    ___isoc99_scanf
.text:0804892F
.text:08048934 83 C4 10                      add     esp, 10h
.text:08048937 8B 4D E8                      mov     ecx, [ebp+var_18]
.text:0804893A 89 C8                         mov     eax, ecx
.text:0804893C 8B 4D EC                      mov     ecx, [ebp+var_14]
.text:0804893F 89 CB                         mov     ebx, ecx
.text:08048941 8B 4D F0                      mov     ecx, [ebp+var_10]
.text:08048944 89 CA                         mov     edx, ecx
.text:08048946 90                            nop
.text:08048947 8B 4D F4                      mov     ecx, [ebp+var_C]
.text:0804894A 65 33 0D 14 00 00 00          xor     ecx, large gs:14h
.text:08048951 74 05                         jz      short locret_8048958
.text:08048951
.text:08048953 E8 48 FA FF FF                call    ___stack_chk_fail
.text:08048953
.text:08048958                               ; ---------------------------------------------------------------------------
.text:08048958
.text:08048958                               locret_8048958:               ; CODE XREF: get_user_input+45↑j
.text:08048958 C9                            leave
.text:08048959 C3                            retn

main 函数反汇编：可以看到 main 函数在调用完 get_user_input 函数后，给eax,ebx,edx的值传给了[ebp+var_14],[ebp+var_10],[ebp+var_C]，而这三个就是v5,v6,v8

.text:08048978 83 C4 10                      add     esp, 10h
.text:0804897B E8 8C FF FF FF                call    get_user_input
.text:0804897B
.text:08048980 89 45 EC                      mov     [ebp+var_14], eax
.text:08048983 89 5D F0                      mov     [ebp+var_10], ebx
.text:08048986 89 55 F4                      mov     [ebp+var_C], edx
.text:08048989 83 EC 0C                      sub     esp, 0Ch
.text:0804898C FF 75 EC                      push    [ebp+var_14]
.text:0804898F E8 75 FB FF FF                call    complex_function_1

所以思路很清晰了，我们想跳过 scanf(“%x %x %x”)，那么也就是跳过 get_user_input 函数，所以我们让程序从下面这个位置开始执行，但是为了模拟 scanf 的功能，我们要让 eax,ebx,edx 符号化

.text:08048980 89 45 EC                      mov     [ebp+var_14], eax

这里介绍：claripy这个包

claripy.BVS(name, size)：创建一个符号向量，第一个参数为符号向量名称，第二个为其大小(单位为位/比特)

注意输入是16进制，所以最后得转换一下；这里可能会有人问，为啥最后不直接found_state.posix.dumps(0)呢？别忘了，我们跳过了scanf，也就是说我们根本就没有输入

#exp.py
import sys
import angr
import claripy

def exp(argv):
    #创建工程
    bin_name = argv[1]
    proj = angr.Project(bin_name, auto_load_libs = False)

    #初始化状态
    start_addr = 0x8048980
    init_state = proj.factory.blank_state(addr = start_addr)

    #创建符号向量，其中我们知道eax,ebx,edx是32位的寄存器
    x1 = claripy.BVS('x1', 32)
    x2 = claripy.BVS('x2', 32)
    x3 = claripy.BVS('x3', 32)

    #符号化eax,ebx,edx寄存器
    init_state.regs.eax = x1
    init_state.regs.ebx = x2
    init_state.regs.edx = x3

    #模拟执行
    simgr = proj.factory.simgr(init_state)

    def is_good(state):
        return b'Good Job.' in state.posix.dumps(1)

    def is_bad(state):
        return b'Try again.' in state.posix.dumps(1)

    simgr.explore(find = is_good, avoid = is_bad)

    if simgr.found:
        found_state = simgr.found[0]
        #约束求解x1,x2,x3
        x1 = found_state.solver.eval(x1)
        x2 = found_state.solver.eval(x2)
        x3 = found_state.solver.eval(x3)
        print(' '.join(map(hex, [x1,x2,x3])))
    else:
        print("Cant't find solution!")

if __name__ == "__main__":
    exp(sys.argv)

04_angr_symbolic_stack

这个题 scanf 接收的输入最后保存在了栈上，所以我们对对符号化(伪栈)

主要函数如下：scanf 接收两个值，然后处理检查；看下汇编吧

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.");
}

handle_user部分汇编：可以看到scanf把接收的值存放在[ebp+var_10]，[ebp+var_C]处，并且后面调用complex_function函数，比较时时也是调用了这两个位置的值；那么我们就模拟一下栈结构以此来模拟scanf函数的功能

.text:08048679 55                            push    ebp
.text:0804867A 89 E5                         mov     ebp, esp
.text:0804867C 83 EC 18                      sub     esp, 18h
.text:0804867F 83 EC 04                      sub     esp, 4
.text:08048682 8D 45 F0                      lea     eax, [ebp+var_10]
.text:08048685 50                            push    eax
.text:08048686 8D 45 F4                      lea     eax, [ebp+var_C]
.text:08048689 50                            push    eax
.text:0804868A 68 B3 87 04 08                push    offset aUU            ; "%u %u"
.text:0804868F E8 DC FC FF FF                call    ___isoc99_scanf
.text:0804868F
.text:08048694 83 C4 10                      add     esp, 10h
.text:08048697 8B 45 F4                      mov     eax, [ebp+var_C]
.text:0804869A 83 EC 0C                      sub     esp, 0Ch
.text:0804869D 50                            push    eax
.text:0804869E E8 06 FE FF FF                call    complex_function0
.text:0804869E
.text:080486A3 83 C4 10                      add     esp, 10h
.text:080486A6 89 45 F4                      mov     [ebp+var_C], eax
.text:080486A9 8B 45 F0                      mov     eax, [ebp+var_10]
.text:080486AC 83 EC 0C                      sub     esp, 0Ch
.text:080486AF 50                            push    eax
.text:080486B0 E8 DC FE FF FF                call    complex_function1

我们从下面的位置开始执行：我们没有从 add esp,1h这里开始执行，因为这句代码是对scanf平衡栈的

.text:08048697 8B 45 F4                      mov     eax, [ebp+var_C]

import sys
import angr
import claripy

def exp(argv):
    bin_path = argv[1]
    proj = angr.Project(bin_path, auto_load_libs = False)

    start_addr = 0x08048697
    init_state = proj.factory.blank_state(addr = start_addr)

    #模拟栈
    init_state.stack_push(init_state.regs.ebp) #可加可不加
    init_state.regs.ebp = init_state.regs.esp
    init_state.regs.esp -= 8 #这里减8，后面push时才是0xc,x10

    x1 = claripy.BVS('x1', 32)
    x2 = claripy.BVS('x2', 32)

    init_state.stack_push(x1) #var_C
    init_state.stack_push(x2) #var_10

    simgr = proj.factory.simgr(init_state)

    def is_good(state):
        return b'Good Job.' in state.posix.dumps(1)

    def is_bad(state):
        return b'Try again.' in state.posix.dumps(1)

    simgr.explore(find = is_good, avoid = is_bad)

    if simgr.found:
        found_state = simgr.found[0]
        x1 = found_state.solver.eval(x1)
        x2 = found_state.solver.eval(x2)
        print(f'{x1} {x2}')
    else:
        print("Can't find solution!")

if __name__ == "__main__":
    exp(sys.argv)

05_angr_symbolic_memory

这个题很简单，scanf接收多个参数，且参数都是全局变量，在 BSS 段上

main函数如下：我们直接把对应的地址给符号化就行了

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

注意：这里符号向量的长度为64，因为%8s是输入长度为8的字符串，而一个字符是一个字节也就是8位，那么8个字符就是64位；还有由于是字符串，所以约束求解时我们要转为bytes求解

import sys
import angr
import claripy

def exp(argv):
    bin_name = argv[1]
    proj = angr.Project(bin_name, auto_load_libs = False)

    start_addr = 0x08048601
    init_state = proj.factory.blank_state(addr = start_addr)
	
    #长度64比特
    x1 = claripy.BVS('x1', 64)
    x2 = claripy.BVS('x2', 64)
    x3 = claripy.BVS('x3', 64)
    x4 = claripy.BVS('x4', 64)

    x1_addr = 0x0A1BA1C0
    x2_addr = 0x0A1BA1C8
    x3_addr = 0x0A1BA1D0
    x4_addr = 0x0A1BA1D8
	
    #内容符号化
    init_state.memory.store(x1_addr, x1)
    init_state.memory.store(x2_addr, x2)
    init_state.memory.store(x3_addr, x3)
    init_state.memory.store(x4_addr, x4)

    simgr = proj.factory.simgr(init_state)

    def is_good(state):
        return b'Good Job.' in state.posix.dumps(1)

    def is_bad(state):
        return b'Try again.' in state.posix.dumps(1)

    simgr.explore(find = is_good, avoid = is_bad)

    if simgr.found:
        found_state = simgr.found[0]
        #约束求解
        x1 = found_state.solver.eval(x1, cast_to = bytes).decode('utf-8')
        x2 = found_state.solver.eval(x2, cast_to = bytes).decode('utf-8')
        x3 = found_state.solver.eval(x3, cast_to = bytes).decode('utf-8')
        x4 = found_state.solver.eval(x4, cast_to = bytes).decode('utf-8')
        print(f'{x1} {x2} {x3} {x4}')
    else:
        print("Can't find solution!")

if __name__ == "__main__":
    exp(sys.argv)