angr

https://github.com/ZERO-A-ONE/AngrCTF_FITM

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

Angr 总的来说是一个多架构的二进制分析平台，具备对二进制文件的动态符号执行能力和多种静态分析能力。在逆向中，一般使用的其动态符号执行解出 Flag，但其实 Angr 还在诸多领域存在应用，比如对程序脆弱性的分析中。

使用 Angr 的步骤可以分为：

创建 project
设置 state
新建符号量 : BVS (bitvector symbolic ) 或 BVV (bitvector value)
把符号量设置到内存或者其他地方
设置 Simulation Managers ，进行路径探索的对象
运行，探索满足路径需要的值
约束求解，获取执行结果

创建 project

path_to_binary = "./00_angr_find"   
project = angr.Project(path_to_binary, auto_load_libs=False)

使用 angr 的首要步骤就是创建 Project 加载二进制文件。angr 的二进制装载组件是 CLE，它负责装载二进制对象（以及它依赖的任何库）和把这个对象以易于操作的方式交给 angr 的其他组件。angr 将这些包含在 Project 类中。一个 Project 类是代表了你的二进制文件的实体。你与 angr 的大部分操作都会经过它

auto_load_libs 设置是否自动载入依赖的库，在基础题目中我们一般不需要分析引入的库文件，这里设置为否

如果 auto_load_libs 是 True（默认值），真正的库函数会被执行。这可能正是也可能不是你想要的，取决于具体的函数。比如说一些 libc 的函数分析起来过于复杂并且很有可能引起 path 对其的尝试执行过程中的 state 数量的爆炸增长

如果 auto_load_libs 是 False，且外部函数是无法找到的，并且 Project 会将它们引用到一个通用的叫做 ReturnUnconstrained 的 SimProcedure 上去，它就像它的名字所说的那样：它返回一个不受约束的值

设置 state

initial_state = project.factory.entry_state()

state 代表程序的一个实例镜像，模拟执行某个时刻的状态，就类似于快照。保存运行状态的上下文信息，如内存/寄存器等, 我们这里使用 project.factory.entry_state() 告诉符号执行引擎从程序的入口点开始符号执行，除了使用 .entry_state() 创建 state 对象, 我们还可以根据需要使用其他构造函数创建 state

设置 Simulation Managers

simulation = project.factory.simgr(initial_state)

Project 对象仅表示程序一开始的样子，而在执行时，我们实际上是对 SimState 对象进行操作，它代表程序的一个实例镜像，模拟执行某个时刻的状态

SimState 对象包含程序运行时信息，如内存/寄存器/文件系统数据等。SM（Simulation Managers）是 angr 中最重要的控制接口，它使你能够同时控制一组状态 (state) 的符号执行，应用搜索策略来探索程序的状态空间。

运行，探索满足路径需要的值

print_good_address = 0x8048678  
simulation.explore(find=print_good_address)

符号执行最普遍的操作是找到能够到达某个地址的状态，同时丢弃其他不能到达这个地址的状态。SM 为使用这种执行模式提供了 .explore() 方法

当使用 find 参数启动 .explore() 方法时，程序将会一直执行，直到发现了一个和 find 参数指定的条件相匹配的状态。find 参数的内容可以是想要执行到的某个地址、或者想要执行到的地址列表、或者一个获取 state 作为参数并判断这个 state 是否满足某些条件的函数。当 active stash 中的任意状态和 find 中的条件匹配的时候，它们就会被放到 found stash 中，执行随即停止。之后你可以探索找到的状态，或者决定丢弃它，转而探索其它状态。

这里 0x8048678 的地址值是根据 IDA 打开后我们可以发现是保存导致打印“ Good Job”的块地址的变量

若能输出正确的字符串 “Good Job” 即代表我们的执行路径是正确的

获取执行结果

if simulation.found:
    solution_state = simulation.found[0]  # 获取通过 explore 找到符合条件的状态
    solution = solution_state.posix.dumps(sys.stdin.fileno())
    print("[+] Success! Solution is: {}".format(solution.decode("utf-8")))

此时相关的状态已经保存在了 simgr 当中，我们可以通过 simgr.found 来访问所有符合条件的分支，这里我们为了解题，就选择第一个符合条件的分支即可

这里解释一下 sys.stdin.fileno(), 在 UNIX 中，按照惯例，三个文件描述符分别表示标准输入、标准输出和标准错误

>>> import sys
>>> sys.stdin.fileno()
0
>>> sys.stdout.fileno()
1
>>> sys.stderr.fileno()
2

所以一般也可以写成：

 solution = solution_state.posix.dumps(0)

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) 将会给出最大可行解

🪴 Cyril

探索