记录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
import angr

def Go():
    def is_good(state):
        output = state.posix.dumps(1)
        if b'Right' in output:
            return True
        else:
            return False
    
    def is_bad(state):
        output = state.posix.dumps(1)
        if b'Fail' in output:
            return True
        else:
            return False
        
    path = './file_path'
    p = angr.Project(path, auto_load_libs=False)
    
    initial_state = p.factory.entry_state()
    
    
    sm = p.factory.simgr(initial_state, veritesting=True)
    
    sm.explore(find=is_good, avoid=is_bad)
    
    
    if sm.found:
        for i in sm.found:
            solved_state = i
            solution = solved_state.posix.dumps(0)
            print(f'[+]Success! Solution is {solution.decode("utf-8", "replace")}')
    else:
        print('[-]Failed! No solution found')
        
if __name__ == '__main__':
    Go()

进阶用法·

符号化·

创建向量·

对于程序中未知的量，我们可以通过符号化变量求解，可以把他理解为设未知数，可以符号化寄存器、栈、内存、动态内存、文件

首先是创建符号化向量的用法

1
2
x1 = claripy.BVS('x1', x1_size_in_bits)
#注意size是以bit为单位的，也就是byte*8

寄存器·

对于符号化寄存器，可以在创建initial_state后，使用以下代码

1
2
initial_state.regs.eax = x1
#x1是你创建的符号化向量

其中除了BVS，还有BVV。BVV(value, size)即BitVector Value，表示有确定值的位向量，而BVS(name, size)则是BitVector Symbol，开始时值未知

栈·

栈空间的处理，我们首先需要恢复ESP和EBP的状态，以便后续计算

1
initial_state.regs.ebp = initial_state.regs.esp #EBP=ESP

接着就是推入符号化向量至栈帧中的指定位置，但是我们需要的位置不一定是栈顶，所以我们需要进行填充，比如从ida看见一个变量int i; // [esp+8h] [ebp-10h]位于ebp-10h处，为了将符号化向量推入此处，我们就需要padding来填充

L_addr
rbp-30h i
rbp-29h i
rbp-28h i
rbp-27h i
… …
rbp-1h padding
rbp-0h padding

所以我们需要填充后再符号化

1
2
initial_state.regs.esp -= 0x2C #0x30-0x4
initial_state.stack_push(x1)   #x1为创建好的向量

内存·

其实就是将内存地址符号化

1
2
x1_addr = 0x114514
initial_state.memory.store(x1_addr, x1)

动态内存·

动态内存就是用malloc分配的，其实和内存的区别就在于中间多了一步将虚假的堆地址存入malloc()函数返回的变量的步骤

1
buffer0 -> fake_heap_addr0 -> symbolic_BVS0

所以我们的可以这样符号化

1
2
3
4
5
6
7
#将fake_heap存入buffer
initial_state.memory.store(buffer0, fake_heap_addr0, endness=project.arch.memory_endness)

#将symbolic_BVS存入fake_heap
initial_state.memory.store(fake_heap_addr0, symbolic_BVS0, endness=project.arch.memory_endness)

#这里的endness是设置端序，有LE、BE、ME可选，这里project.arch.memory_endness是使用与项目相同的端序储存

文件·

1
2
3
4
5
6
7
8
9
filename = 'OJKSQYDP.txt'
symbolic_file_size_bytes = 64
passwd0 = claripy.BVS('password', symbolic_file_size_bytes * 8)
passwd_file = angr.storage.SimFile(filename, content=passwd0, size=symbolic_file_size_bytes)
#这里BVS以bit为单位，file有以byte为单位，很奇怪

initial_state.fs.insert(filename, passwd_file)

simulation = project.factory.simgr(initial_state)

求解·

创建了向量后当然需要求解，使用eval方法

1
2
solved_x1 = solved_state.solver.eval(x1, cast_to=bytes)
print(f'[+] Success! Solution is: {solved_x1.decode('utf-8')}')

约束求解·

当angr遇到循环加上分支路线路线时，就容易发生路径爆炸，即使是非常简单的功能也可能无法求解，这时候可以我们自己化简逻辑

这方面angr和z3差不多，同样是.add()添加约束，接着用.eval()求解

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
# fresh state
>>> state = proj.factory.entry_state()
>>> state.solver.add(x - y >= 4)
>>> state.solver.add(y > 0)
>>> state.solver.eval(x)
5
>>> state.solver.eval(y)
1
>>> state.solver.eval(x + y)
6

# 其中eval还有一些其他用法
# solver.eval(expression) 将会解出一个可行解
# solver.eval_one(expression)将会给出一个表达式的可行解，若有多个可行解，则抛出异常。
# solver.eval_upto(expression, n)将会给出最多n个可行解，如果不足n个就给出所有的可行解。
# solver.eval_exact(expression, n)将会给出n个可行解，如果解的个数不等于n个，将会抛出异常。
# solver.min(expression)将会给出最小可行解
# solver.max(expression)将会给出最大可行解

所以我们的思路大概如下：

  1. 设置符号化向量

  2. 找到我们需要简化的地址

  3. 写出我们的约束条件

  4. 根据条件求解

这里主要记新的东西

1
2
3
# 只要到达compare函数就停下来
cpr_addr = 0x114514
sm.explore(find=cpr_addr)

接着添加约束条件并求解

1
2
3
4
5
6
7
8
9
# 首先load出符号化的向量，注意是byte
symbolic_bitvector0 = solved_state.memory.load(x0_BVS_addr, BVS_size_in_bytes)

# 接着设置目标值
desired_value = 'XXXXXXXXXX'

# 然后添加约束条件，并求解
solved_state.solver.add(symbolic_bitvector0 == desired_value)
solution0 = solved_state.solver.eval(x0, cast_to=bytes)

Hook函数·

Hook地址·

和约束求解类似，我们的思路依然是用自己的函数逻辑替换原函数

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
@p.hook(compare_addr, length=len_to_skip)
    def skip_check_equals(state):
        input_addr = 0x114514
        input_len = 16
        # 同样使用load提取内存数据，不同的是不需要我们自己设置符号化向量
        input_string = state.memory.load(input_addr, input_len)

        desired_value = 'XXXXXXXXXXXXXX'

        # 注意返回值到哪个寄存器，通常是ax，有eax和rax之分
        # 使用BVV构建直接值
        register_size_in_bit = 32
        state.regs.eax = claripy.If(
            input_string == desired_value,
            claripy.BVV(1, register_size_in_bit)
            claripy.BVV(0, register_size_in_bit)
        )

Hook函数名·

假如一个函数被反复调用，我们又需要hook时，显然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
# hook函数设置大致相同，不同的是定义一个继承angr.SimProcedure的类，再通过p.hook_symbol调用
class ReplaceCheckEquals(angr.SimProcedure):
    # 编写方式接近于C
    # 除self外的参数即为需要hook的函数的声明
    def run(self, to_check, length):
        input_addr = to_check
        input_len = length
        # 同样使用load提取内存数据，不同的是不需要我们自己设置符号化向量
        input_string = state.memory.load(input_addr, input_len)

        desired_value = 'XXXXXXXXXXXXXX'

        # 注意返回值到哪个寄存器，通常是ax，有eax和rax之分
        # 使用BVV构建直接值
        register_size_in_bit = 32
        state.regs.eax = claripy.If(
            input_string == desired_value,
            claripy.BVV(1, register_size_in_bit)
            claripy.BVV(0, register_size_in_bit)
        )

# 设置需要hook的函数名并调用类
check_equals_symbol = 'check_equals_XXXXXXXXXXXX'
p.hook_symbol(check_equals_symbol, ReplaceCheckEquals())