一、环境搭建

dockker

docker pull angr/angr

angr文档

https://github.com/angr/angr-doc

二、Angr入门

符号执行

符号执行就是在运行程序时，用符号来替代真实值。符号执行相较于真实值执行的优点在于，当使用真实值执行程序时，我们能 够遍历的程序路径只有一条，而使用符号进行执行时，由于符号是可变的，我们就可以利用这一特性，尽可能的将程序的每一条 路径遍历，这样的话，必定存在至少一条能够输出正确结果的分支，每一条分支的结果都可以表示为一个离散关系式，使用约束 求解引擎即可分析出正确结果。

angr-CLE

CLE是angr加载二进制文件的组建，在加载二进制文件的时候会分析病读取binary的信息

import angr
b = angr.Project("./test")

angr-IR

angr用VEX IR将指令转化为中间语言IR，分析IR并且模拟

如：ARM指令
subs R2, R2, #8

转化为VEX IR
t0 = GET:I32(16)
t1 = 0x8:I32
t3 = Sub32(t0,t1)
PUT(16) = t3
PUT(68) = 0x59FC8:I32

angr-Solver Engine

angr的求解引擎叫Claripy （z3的封装）

import claripy
bv = claripy.BVV(0x41424344, 32)

SimulatorManager-模拟管理器

SimulatorManager是angr模拟执行的控制中心，提供了.run , .explore, .step 等不同类型的执行选项

step()表示向下执行一个block（42bytes），step()函数产生active状态，表示该分支在执行中；
run()表示运行到结束，run()函数产生deadended状态，表示分支结束；
explore()可以对地址进行限制以减少符号执行遍历的路径。

SimulateState-状态

SimulateState是angr的最小分析单元，对应每个step都有一个state

blank_state()构造一个“blank slate”空白状态，其中大部分数据未初始化。当访问未初始化的数据时，将返回一个不受约束的符号值。
entry_state()构造一个状态，准备在主二进制文件的入口处执行。
full_init_state()构造一个状态，该状态可以根据需要在主二进制程序入口点之前运行所有初始化器，例如，共享库构造器或预初始化器。当它完成这些，它将跳转到入口点。
call_state()构造准备执行给定函数的状态。

angr 分析过程

 1、加载二进制文件
 2、设置程序状态
 3、设置模拟器
 4、设置程序路径
 5、模拟器执行结果

三、Angr实践

1、find & avoid （2020网络安全公益赛）

2、symbolic_registers （2020 kctf 十二生肖 [签到题]）

project.factory.blank_state(addr=start_address) => 创建自定义入口的状态上下文
initial_state.regs => 操作状态上下文的寄存器
claripy.BVS('变量名', 变量大小) => 创建求解变量
solution_state.se.eval(变量) => 求解符号变量

def main():
    # global mem
    proj = angr.Project("spring2020.exe", load_options={"auto_load_libs": True})

    start_addr = 0x401A1B  # 0x00401A1B
    state = proj.factory.blank_state(addr=start_addr)
    arg1 = claripy.BVS('arg1', 4 * 8)

    # tmp_addr = 0x00B42568
    state.regs.eax = 0x00B42568
    flag_addr = state.regs.eax

    state.memory.store(flag_addr, arg1)
    state.se.add(arg1.get_byte(3) == 0)

    simgr = proj.factory.simulation_manager(state)
    simgr.explore(find=0x00401750, avoid=0x00401790)

    if simgr.found:
        simgr_state = simgr.found[0]
        res1 = simgr_state.solver.eval(arg1)
        print(res1)

        print(hex(res1))
        hexd = hex(res1)

        result = ''
        for i in range(2, len(hexd)):
            if i % 2 == 0:
                result += (chr(int(hexd[i:i + 2], 16)))
        print(result)
    else:
        raise Exception('Could not find the solution')

3、hooks （defcamp-r100）

Hook回调函数格式:

@project.hook(Hook地址,执行完Hook函数后指令往后跳转n字节) 
def skip_check_equals_(state):

pass

1、初始化proj
2、hook指定地址的函数
3、调用project.execute()
4、当遇到project.terminate_execution()符号执行结束

def hook():
    proj = angr.Project('./r100', load_options={"auto_load_libs": False})
    @proj.hook(0x400844)
    def pringflag(state):
        print(state.posix.dumps(1))
        print(state.posix.dumps(0))
        proj.terminate_execution()
    proj.execute()

4、android题

Java层 checkFirst 判断code

1、长度16
2、字符是1-8的数字

Native层
checkfirst要求注册码以12345678开头
checkAgain要求注册码为12345678数字的某种排列

check_first

check_again

import angr
import claripy
import binascii

def main():
    base = 0x400000 + 1

    proj = angr.Project('./lib/armeabi-v7a/libnative-lib.so', load_options={"auto_load_libs":False})

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

    checkAgain_addr = 0x8328 + base

    state = proj.factory.blank_state(addr=checkAgain_addr)

    state.solver.add(code.get_byte(0) == int(binascii.hexlify(b"1"), 16))
    state.solver.add(code.get_byte(1) == int(binascii.hexlify(b"2"), 16))
    state.solver.add(code.get_byte(2) == int(binascii.hexlify(b"3"), 16))
    state.solver.add(code.get_byte(3) == int(binascii.hexlify(b"4"), 16))
    state.solver.add(code.get_byte(4) == int(binascii.hexlify(b"5"), 16))
    state.solver.add(code.get_byte(5) == int(binascii.hexlify(b"6"), 16))
    state.solver.add(code.get_byte(6) == int(binascii.hexlify(b"7"), 16))
    state.solver.add(code.get_byte(7) == int(binascii.hexlify(b"8"), 16))

    simgr = proj.factory.simulation_manager(state)

    simgr.explore(
        find=[
            0x8530 + base, # check_again
            0x7F92 + base  # check_first
        ],
        avoid=[0x7F88 + base,  # check_first
               0x8512 + base,  # check_again
               0x84E8 + base, 0x84A2 + base, 0x8468 + base, 0x8456 + base, 0x8442 + base, 0x85FC + base
        ])



    if simgr.found:
        simgr_state = simgr.found[0]
        for i in range(8, 16):
            cond_0 = code.get_byte(i) >= ord('1')
            cond_1 = code.get_byte(i) <= ord('8')
            simgr_state.add_constraints(simgr_state.solver.And(cond_0, cond_1))


        if simgr_state.satisfiable():
            flag = simgr_state.solver.eval(code, cast_to=bytes)
            print("find it : ", flag)
        else:
            print("find fail")


if __name__ == '__main__':
    main()

x86版本参考：https://www.jianshu.com/p/508febd24921

相关资料参考：
微笑老弟的Angr基础笔记 https://bbs.pediy.com/thread-251278.htm
angr官方examples https://github.com/angr/angr-doc/tree/master/examples

冰蝎，蚁剑Java内存马查杀防御技术