angr逆向一把梭z3-先知社区

前言

angr 使用符号执行技术，将程序的输入表示为符号变量，而不是具体的值。它会跟踪这些符号变量在程序中的传播和变化，并生成一系列约束条件。通过约束求解器（如 Z3），angr 可以找到满足特定条件的输入，例如触发程序中的某个分支或绕过安全检查。

正文

首先angr最基础的使用如下

find后面直接放想要去的地址

simulation.explore(find=<target_address>, avoid=<avoid_address>)

是 angr 框架中的一个 API 方法，具体用于路径探索。模拟程序的执行并探索不同的执行路径，直到满足特定条件。

find：指定一个目标地址或状态。当模拟的路径到达该地址时，路径探索结束，程序认为找到了目标。

例如，find=0x804868c会告诉模拟器，当程序执行到这个内存地址时，停止探索并返回该路径。

avoid（可选）：指定一个或多个地址，当模拟的路径到达这些地址时，会避免这些路径继续执行。可以用来避免进入某些不想探索的路径。比如那些永假的条件。

但是往往仅仅如此的话是不够的，在一些工作量大路径多的程序里，我们需要手动采取一些缓解运算量的措施。

实战

下面我们将尝试用angr解出这个z3

在这个进程里，我们只把加密跑完，就取出比较验证的地址0x040273C，后面评估工作量太大，不再模拟执行

写成脚本如下，

模拟探索到这个地方便返回路径。

我们查看v4发现是stack空间，这里为了能让v4和密文一次性比较，需要手动处理一下指针，这里相对内存而言我觉得比较难

这个for循环比较如果不加以限制，让angr直接跑的话会有很大的工作量，耗时很久，我们应该把密文提出来加到约束条件

最后

此时跑一下很快就出来了