前言

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

正文

首先angr最基础的使用如下

import angr
import sys
def main(argv):
  
    project = angr.Project('./')
    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)

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

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

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

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

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

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

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

实战

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

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

写成脚本如下，

address_to_check_constraint = 0x40273C
simulation.explore(find=address_to_check_constraint)

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

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

constrained_parameter_address = solution_state.regs.rbp-0x60
constrained_parameter_size_bytes = 42*4
constrained_parameter_bitvector = solution_state.memory.load(
constrained_parameter_address,
constrained_parameter_size_bytes

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

solution_state.add_constraints(constrained_parameter_bitvector == constrained_parameter_desired_value)
print(solution_state.posix.dumps(sys.stdin.fileno()))


最后

import angr
import sys
import claripy


def main(argv):
    path_to_binary = './ze.exe'  # :string
    project = angr.Project(path_to_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)


    address_to_check_constraint = 0x40273C


    simulation.explore(find=address_to_check_constraint)


    if simulation.found:
   
      solution_state = simulation.found[0]
      constrained_parameter_address = solution_state.regs.rbp-0x60
      constrained_parameter_size_bytes = 42*4
      constrained_parameter_bitvector = solution_state.memory.load(
      constrained_parameter_address,
      constrained_parameter_size_bytes
    )


      constrained_parameter_desired_value = b'\x17\x4f\x00\x00\xf6\x9c\x00\x00\xdb\x8d\x00\x00\xa6\x8e\x00\x00\x29\x69\x00\x00\x11\x99\x00\x00\xa2\x40\x00\x00\x3e\x2f\x00\x00\xb6\x62\x00\x00\x82\x4b\x00\x00\x6c\x48\x00\x00\x02\x40\x00\x00\xd7\x52\x00\x00\xef\x2d\x00\x00\xdc\x28\x00\x00\x0d\x64\x00\x00\x8f\x52\x00\x00\x3b\x61\x00\x00\x81\x47\x00\x00\x17\x6b\x00\x00\x37\x32\x00\x00\x93\x2a\x00\x00\x5f\x61\x00\x00\xbe\x50\x00\x00\x8e\x59\x00\x00\x56\x46\x00\x00\x31\x5b\x00\x00\x3a\x31\x00\x00\x10\x30\x00\x00\xfe\x67\x00\x00\x5f\x4d\x00\x00\xdb\x58\x00\x00\x99\x37\x00\x00\xa0\x60\x00\x00\x50\x27\x00\x00\x59\x37\x00\x00\x53\x89\x00\x00\x22\x71\x00\x00\xf9\x81\x00\x00\x24\x55\x00\x00\x71\x89\x00\x00\x1d\x3a\x00\x00' # :string (encoded)
      solution_state.add_constraints(constrained_parameter_bitvector == constrained_parameter_desired_value)
      print(solution_state.posix.dumps(sys.stdin.fileno()))
    else:
        raise Exception('Could not find the solution')


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

此时跑一下很快就出来了