05_angr_symbolic_memory #Angr Tutorial For CTF

sacnf로 전역변수에 값을 쓰고, 비교를 하는 함수다.

우선 %8s %8s %8s %8s 이므로 start_address를 scanf 이후로 맞춰주고, 변수들을 만들어 준다.

또한 8바이트를 받으므로 64(8*8)비트를 넣어준다.

 

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

  # The binary is calling scanf("%8s %8s %8s %8s").
  # (!)
  password0 = claripy.BVS('password0', 64)
  password1 = claripy.BVS('password1', 64)
  password2 = claripy.BVS('password2', 64)
  password3 = claripy.BVS('password3', 64)

 

 

user_input은 0x0A1BA1C0에 저장되고 변수 하나당 8바이트씩 저장한다.

 

  password0_address = 0x0A1BA1C0
  initial_state.memory.store(password0_address, password0)
  password1_address = 0x0A1BA1C8
  initial_state.memory.store(password1_address, password1)
  password2_address = 0x0A1BA1D0
  initial_state.memory.store(password2_address, password2)
  password3_address = 0x0A1BA1D8
  initial_state.memory.store(password3_address, password3)

 

import angr
import claripy
import sys

def main(argv):
  path_to_binary = '05_angr_symbolic_memory'
  project = angr.Project(path_to_binary)

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

  # The binary is calling scanf("%8s %8s %8s %8s").
  # (!)
  password0 = claripy.BVS('password0', 64)
  password1 = claripy.BVS('password1', 64)
  password2 = claripy.BVS('password2', 64)
  password3 = claripy.BVS('password3', 64)

  # Determine the address of the global variable to which scanf writes the user
  # input. The function 'initial_state.memory.store(address, value)' will write
  # 'value' (a bitvector) to 'address' (a memory location, as an integer.) The
  # 'address' parameter can also be a bitvector (and can be symbolic!).
  # (!)
  password0_address = 0x0A1BA1C0
  initial_state.memory.store(password0_address, password0)
  password1_address = 0x0A1BA1C8
  initial_state.memory.store(password1_address, password1)
  password2_address = 0x0A1BA1D0
  initial_state.memory.store(password2_address, password2)
  password3_address = 0x0A1BA1D8
  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 state.posix.dumps(sys.stdout.fileno())

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return b"Try again." in state.posix.dumps(sys.stdout.fileno())

  simulation.explore(find=is_successful, avoid=should_abort)

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

    # Solve for the symbolic values. We are trying to solve for a string.
    # Therefore, we will use eval, with named parameter cast_to=bytes
    # which returns bytes that can be decoded to a string instead of an integer.
    # (!)
    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 = str(solution0)+" "+str(solution1)+" "+str(solution2)+" "+str(solution3)

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

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