Angr符号执行框架入门教程

第一部分：Angr基础介绍

1. 什么是Angr

Angr是一个基于Python的二进制分析框架，它结合了静态与动态符号分析技术，适用于各种二进制分析任务。其核心功能是符号执行引擎，可以在不实际执行程序的情况下分析哪些输入会经历哪些代码路径。

2. 符号执行基本原理

符号执行将程序的某些部分（如输入）视为符号（类似方程中的x），然后向后遍历执行以找到满足约束条件的符号值。例如：

int x;
scanf("%d", &x);
if ((x > 1) && (x < 10)) {
    puts("Success!!");
} else {
    puts("Fail.");
}

符号执行引擎会注入一个符号λ，然后寻找满足x>1且x<10的λ值。

3. 第一个Angr示例：00_angr_find

这是一个简单的二进制文件，输入一个字符串后会打印是否正确。我们想找到能打印"Good Job"的输入。

基本脚本框架：

import angr
import sys

def main(argv):
    path_to_binary = "./00_angr_find"
    project = angr.Project(path_to_binary)
    initial_state = project.factory.entry_state()
    simulation = project.factory.simgr(initial_state)
    
    print_good_address = 0x8048678  # 找到打印"Good Job"的地址
    simulation.explore(find=print_good_address)
    
    if simulation.found:
        solution_state = simulation.found[0]
        print(solution_state.posix.dumps(sys.stdin.fileno()))
    else:
        raise Exception('Could not find the solution')

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

关键点：

1. 创建Project对象
2. 从入口点创建初始状态
3. 创建Simulation Manager
4. 指定目标地址进行探索
5. 获取并打印解决方案

第二部分：高级符号执行技术

1. 条件查找：02_angr_find_condition

当程序有多个输出"Good Job"或"Try again"的代码块时，可以根据输出内容来判断状态。

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

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

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

2. 符号寄存器：03_angr_symbolic_registers

当程序使用复杂格式字符串（如"%x %x %x"）时，需要直接将符号值注入寄存器。

start_address = 0x8048980  # 跳过scanf调用
initial_state = project.factory.blank_state(addr=start_address)

password0 = claripy.BVS('password0', 32)  # 32位符号位向量
password1 = claripy.BVS('password1', 32)
password2 = claripy.BVS('password2', 32)

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

# 求解
solution0 = format(solution_state.solver.eval(password0), 'x')
solution1 = format(solution_state.solver.eval(password1), 'x')
solution2 = format(solution_state.solver.eval(password2), 'x')

3. 符号栈：04_angr_symbolic_stack

当变量存储在栈上而非寄存器时，需要手动构造栈帧。

start_address = 0x8048697  # 跳过scanf调用
initial_state = project.factory.blank_state(addr=start_address)

# 设置EBP=ESP
initial_state.regs.ebp = initial_state.regs.esp

# 创建符号位向量
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)

# 调整栈指针并压入符号值
initial_state.regs.esp -= 8  # 填充8字节
initial_state.stack_push(password0)
initial_state.stack_push(password1)

关键概念总结

1. 符号执行：将输入视为符号而非具体值，通过求解约束条件找到有效输入
2. Project：Angr分析的基本对象，代表被分析的二进制程序
3. 状态(State)：程序在某个执行点的快照
4. Simulation Manager：管理状态执行和探索
5. 符号位向量(BVS)：表示符号值的基本数据类型
6. 探索策略：
   • find：指定目标状态或地址
   • avoid：指定要避免的状态或地址
7. 状态注入：
   • 寄存器注入：state.regs.寄存器名 = 符号值
   • 栈注入：调整ESP后使用stack_push

最佳实践

1. 对于复杂输入格式，跳过scanf等函数直接从后续指令开始分析
2. 使用blank_state而非entry_state时，确保正确设置寄存器值
3. 注意符号位向量的大小应与目标变量大小匹配（如32位寄存器用32位向量）
4. 栈操作时注意对齐和填充
5. 使用条件函数处理多个可能输出路径的情况

通过掌握这些基础知识和技巧，可以逐步解决更复杂的二进制分析问题。