angr_ctf笔记

抽空系统学下angr关于符号执行的一些api。通过angr_ctf来学，可以自己构建，不过solution目录下有已经构建好的程序、练习文件和参考答案，直接用就行了。目录下的SymbolicExecution.pptx还详细讲了一些符号执行的入门知识，可以看看。

00_angr_find

解常规逆向的基本框架，输入来自stdin。同时如果想默认从main函数开始执行，使用entry_state作为初始状态。

import angr
import sys

def main(argv):
  path_to_binary = './00_angr_find'
  # 起project，需要视情况加参数
  project = angr.Project(path_to_binary)

  # 起始状态，entry_state表示main()
  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  # 创建SimulationManager
  simulation = project.factory.simgr(initial_state)

  print_good_address = 0x804868f  # :integer (probably in hexadecimal)
  simulation.explore(find=print_good_address)

  # simulation.found是存储可行状态的list
  if simulation.found:
    solution_state = simulation.found[0]

    # 输入符合要求的stdin
    print(solution_state.posix.dumps(sys.stdin.fileno()).decode())
  else:
    raise Exception('Could not find the solution')

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

01_angr_avoid

simulation.explore可以通过avoid来减少搜索空间。

import angr
import sys

def main(argv):
  path_to_binary = './01_angr_avoid'
  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)

  # 通过avoid避免搜索某些路径
  print_good_address = 0x80485f7
  will_not_succeed_address = [0x80485bf, 0x8048575, 0x8048609]
  simulation.explore(find=print_good_address, avoid=will_not_succeed_address)

  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)

02_angr_find_condition

explore方法的find和avoid参数允许接受一个函数，以处理复杂的state判定问题。这个函数接受一个SimState参数，并返回True和False。

import angr
import sys

def main(argv):
  path_to_binary = "./02_angr_find_condition"
  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)

  # 用于find的函数
  def is_successful(state: angr.SimState):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return b'Good Job.' in stdout_output

  # 用于avoid的函数
  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)

  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)

03_angr_symbolic_registers

• **当输入来源比较复杂时，可以直接在程序获取输入之后将符号值注入到指定地方。**这个例子注入到寄存器。
• 如果想自定义起始地址，起始状态应该使用blank_state。
• claripy.BVS(name, bit)接受bit数创建符号。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  # 自定义起始位置，使用blank_state
  start_address = 0x80488c7
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  # 使用claripy创建位向量
  password0_size_in_bits = 32
  password0 = claripy.BVS('password0', password0_size_in_bits)
  password1_size_in_bits = 32
  password1 = claripy.BVS('password0', password1_size_in_bits)
  password2_size_in_bits = 32
  password2 = claripy.BVS('password0', password2_size_in_bits)

  # 将符号注入到寄存器
  initial_state.regs.eax = password0
  initial_state.regs.ebx = password1
  initial_state.regs.edx = password2

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    # 求解满足条件的符号
    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)
    solution2 = solution_state.solver.eval(password2)

    solution = f'{solution0:x} {solution1:x} {solution2:x}'
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

04_angr_symbolic_stack

• 当符号值位于栈上时，需要提前做好栈布局，再将符号值放到栈上（push或直接内存赋值）。

• state.stack_push(thing)

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  # 取scanf之后的地址
  start_address = 0x80486ae
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  # mov     ebp, esp
  initial_state.regs.ebp = initial_state.regs.esp

  # angr无法处理当scanf获取输入超过1的情况。
  password0 = claripy.BVS('password0', 32)
  password1 = claripy.BVS('password1', 32)

  # BN>=4.1可以方便地看栈布局
  padding_length_in_bytes = 8
  initial_state.regs.esp -= padding_length_in_bytes

  # push符号值
  initial_state.stack_push(password0)
  initial_state.stack_push(password1)

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)

    solution = ' '.join(map(str, [ solution0, solution1 ]))
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

05_angr_symbolic_memory

• state.memory.store(addr, value, endness=project.arch.memory_endness)，addr和value可以是具体值，也可以是符号。当存储具体数值时，默认是大端，需要使用endness参数指定小端。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x8048618
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password0 = claripy.BVS('password0', 8*8)
  password1 = claripy.BVS('password1', 8*8)
  password2 = claripy.BVS('password2', 8*8)
  password3 = claripy.BVS('password3', 8*8)

  # 写内存
  password0_address = 0xab232c0
  initial_state.memory.store(password0_address, password0)
  password1_address = 0xab232c8
  initial_state.memory.store(password1_address, password1)
  password2_address = 0xab232d0
  initial_state.memory.store(password2_address, password2)
  password3_address = 0xab232d8
  initial_state.memory.store(password3_address, password3)

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    # eval默认生成整数，使用cast_to生成其它类型
    solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode()
    solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode()
    solution2 = solution_state.solver.eval(password2,cast_to=bytes).decode()
    solution3 = solution_state.solver.eval(password3,cast_to=bytes).decode()
    solution = ' '.join([solution0, solution1, solution2, solution3])

    print(solution)
  else:
    raise Exception('Could not find the solution')

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

06_angr_symbolic_dynamic_memory

• 对于动态分配的内存，我们可以直接指定一个地址假设其已经得到了分配，angr会自行进行处理。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x80486af
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password0 = claripy.BVS('password0', 8*8)
  password1 = claripy.BVS('password1', 8*8)

  # 直接分配地址，angr会自行分配内存
  fake_heap_address0 = 0x12345678
  pointer_to_malloc_memory_address0 = 0xa2def74
  initial_state.memory.store(pointer_to_malloc_memory_address0, fake_heap_address0, endness=project.arch.memory_endness)
  fake_heap_address1 = 0x11223344
  pointer_to_malloc_memory_address0 = 0xa2def7c
  initial_state.memory.store(pointer_to_malloc_memory_address0, fake_heap_address1, endness=project.arch.memory_endness)

  # 往假定的地址填充数据
  initial_state.memory.store(fake_heap_address0, password0)
  initial_state.memory.store(fake_heap_address1, password1)

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode()
    solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode()
    solution = ' '.join([solution0, solution1])

    print(solution)
  else:
    raise Exception('Could not find the solution')

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

07_angr_symbolic_file

• 通过angr.storage.SimFile和state.fs.insert来插入符号化文件。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x80488bc
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  filename = 'FOQVSBZB.txt'
  symbolic_file_size_bytes = 0x40

  password = claripy.BVS('password', symbolic_file_size_bytes * 8)

  # 创建符号文件
  password_file = angr.storage.SimFile(filename, content=password)
  
  # 将符号文件插入state
  initial_state.fs.insert(filename, password_file)

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = solution_state.solver.eval(password,cast_to=bytes).decode()

    print(solution)
  else:
    raise Exception('Could not find the solution')

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

08_angr_constraints

• 当最后的限制函数复杂，会导致angr路径爆炸的话，可以手动通过state.add_constraints添加约束。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  start_address = 0x804863c
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  password = claripy.BVS('password', 16*8)

  password_address = 0x804a040
  initial_state.memory.store(password_address, password)

  simulation = project.factory.simgr(initial_state)

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

  if simulation.found:
    solution_state = simulation.found[0]

    constrained_parameter_address = 0x804a040
    constrained_parameter_size_bytes = 16
    constrained_parameter_bitvector = solution_state.memory.load(
      constrained_parameter_address,
      constrained_parameter_size_bytes
    )

    constrained_parameter_desired_value = b'OSIWHBXIFOQVSBZB'

    # 手动添加约束
    solution_state.add_constraints(constrained_parameter_bitvector == constrained_parameter_desired_value)

    solution = solution_state.solver.eval(password, cast_to=bytes).decode()

    print(solution)
  else:
    raise Exception('Could not find the solution')

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

09_angr_hooks

• 除了手动加约束，还可以使用@project.hook修饰一个以state为参数的hook函数来hook一段代码。
• hook函数返回值要传递给约束求解器的话应使用claripy接受的值。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  # scanf只处理一个输入，可以直接使用entry_state
  initial_state = project.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  check_equals_called_address = 0x80486ca

  instruction_to_skip_length = 5
  # 修饰hook函数，以address为起始，length为跳过长度
  @project.hook(check_equals_called_address, length=instruction_to_skip_length)
  def skip_check_equals_(state):	# hook函数以state为参数
    user_input_buffer_address = 0x804a044
    user_input_buffer_length = 16

    user_input_string = state.memory.load(
      user_input_buffer_address,
      user_input_buffer_length
    )
    
    check_against_string = b'OSIWHBXIFOQVSBZB'

    # 返回值后续还要给约束求解器使用。claripy.If(expression, ret_if_true, ret_if_false)
    state.regs.eax = claripy.If(
      user_input_string == check_against_string, 
      claripy.BVV(1, 32), 
      claripy.BVV(0, 32)
    )

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = solution_state.posix.dumps(sys.stdin.fileno()).decode()
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

10_angr_simprocedures

• 对于程序里的函数，可以使用SimProcedure进行hook：为需要hook的函数定义一个SimProcedure的子类，并定义run(self, arg1, arg2, ...)函数。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  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}
  )

  # 为待hook的函数定义一个SimProcedure子类
  class ReplacementCheckEquals(angr.SimProcedure):
    # 定义run函数，替代待hook函数
    def run(self, to_check, length):
      user_input_buffer_address = to_check
      user_input_buffer_length = length

      user_input_string = self.state.memory.load(
        user_input_buffer_address,
        user_input_buffer_length
      )

      check_against_string = b'OSIWHBXIFOQVSBZB'
      
      # 处理函数的返回值
      return claripy.If(user_input_string == check_against_string, claripy.BVV(1, 32), claripy.BVV(0, 32))


  # hook_symbol方法用来hook有符号的函数，hook方法用来hook指定地址的函数。
  check_equals_symbol = 'check_equals_OSIWHBXIFOQVSBZB'
  project.hook_symbol(check_equals_symbol, ReplacementCheckEquals())

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = solution_state.posix.dumps(sys.stdin.fileno())
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

11_angr_sim_scanf

算是前一个挑战的练习：hook特定参数的scanf。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  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}
  )

  class ReplacementScanf(angr.SimProcedure):
    # scanf("%u %u", addr0, addr1)
    def run(self, format_string, scanf0_address, scanf1_address):
      scanf0 = claripy.BVS('scanf0', 4*8)
      scanf1 = claripy.BVS('scanf1', 4*8)

      self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
      self.state.memory.store(scanf1_address, scanf1, endness=project.arch.memory_endness)

      # 可以把变量存储再state的globals中
      self.state.globals['solution0'] = scanf0
      self.state.globals['solution1'] = scanf1

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  simulation = project.factory.simgr(initial_state)

  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)

  if simulation.found:
    solution_state = simulation.found[0]

    stored_solutions0 = solution_state.globals['solution0']
    stored_solutions1 = solution_state.globals['solution1']
    solution = ' '.join(map(str, [solution_state.solver.eval(stored_solutions0), solution_state.solver.eval(stored_solutions1)]))

    print(solution)
  else:
    raise Exception('Could not find the solution')

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

12_angr_veritesting

• 如果实在绕不开循环，可以尝试为SimulationManager开启veritesting：project.factory.simgr(initial_state, veritesting=True)来优化循环处理。

• 但不知道为什么我电脑还是卡住了，搜遍全网也不知道为啥。。

import angr
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary, load_options={'auto_load_libs': False})
  initial_state = project.factory.entry_state()
  simulation = project.factory.simgr(initial_state, veritesting=True)

  def is_successful(state: angr.SimState):
    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)

  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)

13_angr_static_binary

• 程序使用静态链接时，需要手动hook标准库函数。

# angr.SIM_PROCEDURES['libc']['malloc']
# angr.SIM_PROCEDURES['libc']['fopen']
# angr.SIM_PROCEDURES['libc']['fclose']
# angr.SIM_PROCEDURES['libc']['fwrite']
# angr.SIM_PROCEDURES['libc']['getchar']
# angr.SIM_PROCEDURES['libc']['strncmp']
# angr.SIM_PROCEDURES['libc']['strcmp']
# angr.SIM_PROCEDURES['libc']['scanf']
# angr.SIM_PROCEDURES['libc']['printf']
# angr.SIM_PROCEDURES['libc']['puts']
# angr.SIM_PROCEDURES['libc']['exit']
# angr.SIM_PROCEDURES['glibc']['__libc_start_main']
# There are many more, see:
# https://github.com/angr/angr/tree/master/angr/procedures/libc

import angr
import sys

def main(argv):
  path_to_binary = argv[1]
  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}
  )

  project.hook(0x8048d60, angr.SIM_PROCEDURES['glibc']['__libc_start_main']())
  project.hook(0x804fab0, angr.SIM_PROCEDURES['libc']['printf']())
  project.hook(0x804fb10, angr.SIM_PROCEDURES['libc']['scanf']())
  project.hook(0x80503f0, angr.SIM_PROCEDURES['libc']['puts']())
  project.hook(0x804f050, angr.SIM_PROCEDURES['libc']['exit']())
  project.hook(0x8048228, angr.SIM_PROCEDURES['libc']['strcmp']())

  simulation = project.factory.simgr(initial_state)

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

  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)

14_angr_shared_library

如何处理PIE程序和处理单个函数。

• 对于PIE程序，在创建project时需要在load_options中指定base。
• 对于要处理的单个函数，可以使用call_state(addr, args, ...)作为初始状态。
• 在传递常量时要使用claripy.BVV。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]

  # 指定基址
  base = 0x9000000
  project = angr.Project(path_to_binary, load_options={
    'main_opts' : {
      'base_addr' : base
    }
  })

  buffer_pointer = claripy.BVV(0x9003000, 32)

  # 注意使用claripy.BVV
  validate_function_address = base + 0x670
  initial_state = project.factory.call_state(
                    validate_function_address,
                    buffer_pointer,
                    claripy.BVV(8, 32),
                    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
                  )

  password = claripy.BVS( 'password', 8*8 )
  initial_state.memory.store( buffer_pointer , password )
  
  simulation = project.factory.simgr(initial_state)

  check_constraint_address = base + 0x718
  simulation.explore(find=check_constraint_address)

  if simulation.found:
    solution_state = simulation.found[0]

    solution_state.add_constraints( solution_state.regs.eax != 0 )
    solution = solution_state.solver.eval(password, cast_to=bytes)
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

15_angr_arbitrary_read

如何用angr检查是否存在溢出以及可以用来任意读取数据：使用solver.symbolic检查puts的参数。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  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}
  )

  # scanf接受超过两个参数，需要手动hook
  class ReplacementScanf(angr.SimProcedure):
    # Hint: scanf("%u %20s")
    def run(self, format_string, key, buf):
      # %u
      scanf0 = claripy.BVS('scanf0', 4*8)
      
      # %20s
      scanf1 = claripy.BVS('scanf1', 20*8)

      # 将bitvector按bit分解为byte
      for char in scanf1.chop(bits=8):
        self.state.add_constraints(char >= 0x20, char <= 0x7e)

      # 整数需要注意小端存储，字节串直接默认大端即可
      scanf0_address = key
      self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
      scanf1_address = buf
      self.state.memory.store(scanf1_address, scanf1)

      self.state.globals['solution0'] = scanf0
      self.state.globals['solution1'] = scanf1

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  # 检查puts的函数
  def check_puts(state):
    # 进入puts后取参数
    puts_parameter = state.memory.load(state.regs.esp+4, 4, endness=project.arch.memory_endness)

    # symbolic方法可以检查参数是否有多个可接受值，如果有，说明可能可以符号化，可以被人为控制
    if state.solver.symbolic(puts_parameter):
      good_job_string_address = 0x4f534957

      # 参数是否可以等于good_job_string_address
      is_vulnerable_expression = puts_parameter == good_job_string_address

      # 是否可以满足？
      if state.satisfiable(extra_constraints=(is_vulnerable_expression,)):
        state.add_constraints(is_vulnerable_expression)
        return True
      else:
        return False
    else:
      return False

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    # 每次调用puts时都检查参数
    puts_address = 0x8048370
    if state.addr == puts_address:
      return check_puts(state)
    else:
      return False

  simulation.explore(find=is_successful)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = [solution_state.solver.eval(solution_state.globals['solution0']), solution_state.solver.eval(solution_state.globals['solution1'], cast_to=bytes)]
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

16_angr_arbitrary_write

如何用angr检查是否存在溢出以及可以用来任意写：使用solver.symbolic检查strncpy的参数。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  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}
  )

  # scanf接受超过两个参数，需要手动hook
  class ReplacementScanf(angr.SimProcedure):
    # Hint: scanf("%u %20s")
    def run(self, format_string, key, buf):
      # %u
      scanf0 = claripy.BVS('scanf0', 4*8)
      
      # %20s
      scanf1 = claripy.BVS('scanf1', 20*8)

      for char in scanf1.chop(bits=8):
        self.state.add_constraints(char >= 0x20, char <= 0x7e)

      scanf0_address = key
      self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness)
      scanf1_address = buf
      self.state.memory.store(scanf1_address, scanf1)

      self.state.globals['solutions'] = [scanf0, scanf1]

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  def check_strncpy(state):
    # 调用strncpy时参数位置
    strncpy_dest = state.memory.load(state.regs.esp+4, 4, endness=project.arch.memory_endness)
    strncpy_src = state.memory.load(state.regs.esp+8, 4, endness=project.arch.memory_endness)
    strncpy_len = state.memory.load(state.regs.esp+12, 4, endness=project.arch.memory_endness)

    # 我们要控制的source地址的内容，而不是source地址本身
    src_contents = state.memory.load(strncpy_src, strncpy_len)

    # 我们要控制的是source地址的内容和dest地址，需要检查
    if state.solver.symbolic(src_contents) and state.solver.symbolic(strncpy_dest):
      password_string = b'NEDVTNOP'
      buffer_address = 0x4D43523C

      # bitvectors支持切片，但它是倒着的。例如，b == 'ABCDEFGH'，则b[7:0] == 'H'，b[63:48] == 'AB'，b[-1:-16] == 'AB'。
      does_src_hold_password = src_contents[-1:-8*8] == password_string

      # 检查dest地址
      does_dest_equal_buffer_address = strncpy_dest == buffer_address

      if state.satisfiable(extra_constraints=(does_src_hold_password, does_dest_equal_buffer_address)):
        state.add_constraints(does_src_hold_password, does_dest_equal_buffer_address)
        return True
      else:
        return False
    else:
      return False

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    strncpy_address = 0x8048410
    if state.addr == strncpy_address:
      return check_strncpy(state)
    else:
      return False

  simulation.explore(find=is_successful)

  if simulation.found:
    solution_state = simulation.found[0]

    solution = [solution_state.solver.eval(solution_state.globals['solutions'][0]), solution_state.solver.eval(solution_state.globals['solutions'][1], cast_to=bytes)]
    print(solution)
  else:
    raise Exception('Could not find the solution')

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

17_angr_arbitrary_jump

• 可以通过检测simulation_manager的unconstrained stash来发现那些可以被劫持控制流的地方。

• 当执行到某条指令后有太多可能的分支，即PC可符号化时，angr会将此状态标注为unconstrained，并默认抛出异常。可以在创建simulation_manager时设置参数save_unconstrained=True来阻止。

import angr
import claripy
import sys

def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  symbolic_input = claripy.BVS("input", 100*8)

  initial_state = project.factory.entry_state(
          stdin=symbolic_input,
          add_options = {
              angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
              angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
              }
          )

  # 创建一个能保存stash的simulation_manager 
  simulation = project.factory.simgr(
    initial_state,
    save_unconstrained=True,
    stashes={
      'active' : [initial_state],
      'unconstrained' : [],
      'found' : [],
      'not_needed' : []
    }
  )

  # 我们的目标是unconstrained，found状态在这里需要手动指定
  def has_found_solution():
    return simulation.found

  # 代表PC可以被我们操控的状态
  def has_unconstrained_to_check():
    return simulation.unconstrained

  # 代表可以继续探索的状态
  def has_active():
    return simulation.active

  while (has_active() or has_unconstrained_to_check()) and (not has_found_solution()):
    for unconstrained_state in simulation.unconstrained:
        # 在这里，unconstrained状态就是我们要找的found状态
      simulation.move('unconstrained', 'found')

    simulation.step()

  if simulation.found:
    solution_state = simulation.found[0]

    # 为unconstrained状态添加约束
    solution_state.add_constraints(solution_state.regs.eip == 0x4D435250)

    for byte in symbolic_input.chop(bits=8):
      solution_state.add_constraints(
              byte >= 0x20,
              byte <= 0x7e
      )

    solution = solution_state.solver.eval(symbolic_input,cast_to=bytes).decode()
    print(solution)
  else:
    raise Exception('Could not find the solution')

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