Angr逆向分析框架与Z3求解器实战教程

1. Angr框架概述

Angr是一个基于Python的二进制分析框架，它结合了符号执行、约束求解和程序分析技术，主要用于逆向工程、漏洞挖掘和程序分析等领域。

1.1 核心概念

• 符号执行：将程序的输入表示为符号变量而非具体值，跟踪这些变量在程序中的传播和变化
• 约束求解：使用Z3等求解器解决路径约束，找到满足特定条件的输入
• 路径探索：系统地探索程序的不同执行路径

2. 基础使用方法

2.1 基本框架

import angr
import sys

def main(argv):
    # 加载目标程序
    project = angr.Project('./binary')
    
    # 创建初始状态，设置符号内存和寄存器
    initial_state = project.factory.entry_state(
        add_options={
            angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
            angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
        })
    
    # 创建模拟管理器
    simulation = project.factory.simgr(initial_state)
    
    # 探索路径，寻找目标地址
    simulation.explore(find=0x804868c)
    
    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)

2.2 关键参数说明

• find: 目标地址，当执行到达该地址时停止探索
• avoid: 要避免的地址，当执行到达这些地址时放弃当前路径
• add_options: 设置符号执行选项
  • SYMBOL_FILL_UNCONSTRAINED_MEMORY: 将未初始化的内存标记为符号变量
  • SYMBOL_FILL_UNCONSTRAINED_REGISTERS: 将未初始化的寄存器标记为符号变量

3. 实战技巧

3.1 优化路径探索

对于复杂程序，直接全路径探索可能导致计算量过大，需要采取优化措施：

1. 精确控制探索范围：只模拟关键部分代码
2. 手动添加约束：减少不必要的路径探索
3. 提前终止条件：在加密/解密完成后立即提取状态

3.2 处理内存比较

当程序进行内存块比较时（如strcmp或memcmp），直接模拟会导致性能问题：

1. 提取密文：从二进制中提取比较的密文
2. 手动添加约束：将输入与密文的关系转化为约束条件
3. 避免逐字节比较：使用批量约束代替循环比较

3.3 指针处理技巧

处理栈空间变量时，需要注意指针问题：

1. 识别栈变量：通过反汇编确定变量位置
2. 手动设置内存：使用state.memory.store设置符号值
3. 处理指针引用：确保符号变量被正确解引用

4. 高级应用

4.1 约束求解集成

Angr内置Z3求解器，可以：

1. 提取路径约束：solution_state.solver.constraints
2. 添加自定义约束：state.solver.add()
3. 求解具体值：state.solver.eval()

4.2 性能优化策略

1. 路径剪枝：尽早识别并丢弃不可行路径
2. 符号化简化：只对关键输入符号化
3. 分层分析：先快速定位关键区域再详细分析

5. 典型问题解决方案

5.1 加密算法逆向

1. 定位加密函数入口
2. 在加密完成后设置断点
3. 提取加密后的数据作为约束
4. 反向求解原始输入

5.2 验证逻辑绕过

1. 识别验证失败分支
2. 设置avoid参数避开失败路径
3. 直接定位成功验证后的代码位置

6. 调试技巧

1. 状态检查：state.regs查看寄存器值
2. 内存查看：state.mem[address].uint32_t查看内存
3. 约束查看：state.solver.constraints查看当前约束
4. 符号值查看：state.solver.eval(symbol)获取符号具体值

通过以上方法和技巧，可以高效使用Angr解决复杂的逆向工程问题，特别是那些需要自动化求解输入条件的情况。