03_angr_symbolic_registers #Angr Tutorial For CTF

main

 

입력 받는 scanf 함수들이 get_user_input 함수에 들어있다.

 

get_user_input

 

angr는 scanf에 %x %x와 같이 여러가지 입력을 지원하지 않는다.

따라서 시작 주소 기존의 entry_state가 아닌 scanf 이후로 맞춰둬야 한다.

scanf는 get_user_input 함수에 있으니, 끝났을 때의 기준으로 맞췄다.

 

 

  start_address = 0x08048980  # :integer (probably hexadecimal)
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

 

이제 심볼릭 변수들을 초기화 해줘야한다. password0 형식에 맞춰 1, 2도 생성해 준다. (변수명을 원하는대로 수정해도 된다.) (%x는 4바이트이므로 사이즈는 32비트이다.)

  password0_size_in_bits = 32  # :integer
  password1_size_in_bits = 32  # :integer
  password2_size_in_bits = 32  # :integer
  password0 = claripy.BVS('password0', password0_size_in_bits)
  password1 = claripy.BVS('password1', password1_size_in_bits)
  password2 = claripy.BVS('password2', password2_size_in_bits)

 

scanf에서 받은 값들은 각각 eax, ebx, edx로 들어가게 된다.

  initial_state.regs.eax = password0
  initial_state.regs.ebx = password1
  initial_state.regs.edx = password2

 

입력값이 3개이므로 출력값도 3개로 해줘야 하는데, scanf에서 %x로 받고 있으므로 hex로 출력해준다.

    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)
    solution2 = solution_state.solver.eval(password2)
    
    solution = hex(solution0)+" "+hex(solution1)+" "+hex(solution2)  # :string
    print(solution)

 

# Angr doesn't currently support reading multiple things with scanf (Ex: 
# scanf("%u %u).) You will have to tell the simulation engine to begin the
# program after scanf is called and manually inject the symbols into registers.

import angr
import claripy
import sys

def main(argv):
  path_to_binary = '03_angr_symbolic_registers'
  project = angr.Project(path_to_binary)

  # Sometimes, you want to specify where the program should start. The variable
  # start_address will specify where the symbolic execution engine should begin.
  # Note that we are using blank_state, not entry_state.
  # (!)
  start_address = 0x08048980  # :integer (probably hexadecimal)
  initial_state = project.factory.blank_state(
    addr=start_address,
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )

  # Create a symbolic bitvector (the datatype Angr uses to inject symbolic
  # values into the binary.) The first parameter is just a name Angr uses
  # to reference it. 
  # You will have to construct multiple bitvectors. Copy the two lines below
  # and change the variable names. To figure out how many (and of what size)
  # you need, dissassemble the binary and determine the format parameter passed
  # to scanf.
  # (!)
  password0_size_in_bits = 32  # :integer
  password1_size_in_bits = 32  # :integer
  password2_size_in_bits = 32  # :integer
  password0 = claripy.BVS('password0', password0_size_in_bits)
  password1 = claripy.BVS('password1', password1_size_in_bits)
  password2 = claripy.BVS('password2', password2_size_in_bits)

  # Set a register to a symbolic value. This is one way to inject symbols into
  # the program.
  # initial_state.regs stores a number of convenient attributes that reference
  # registers by name. For example, to set eax to password0, use:
  #
  # initial_state.regs.eax = password0
  #
  # You will have to set multiple registers to distinct bitvectors. Copy and
  # paste the line below and change the register. To determine which registers
  # to inject which symbol, dissassemble the binary and look at the instructions
  # immediately following the call to scanf.
  # (!)
  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 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. If there are multiple solutions, we only
    # care about one, so we can use eval, which returns any (but only one)
    # solution. Pass eval the bitvector you want to solve for.
    # (!)
    solution0 = solution_state.solver.eval(password0)
    solution1 = solution_state.solver.eval(password1)
    solution2 = solution_state.solver.eval(password2)

    # Aggregate and format the solutions you computed above, and then print
    # the full string. Pay attention to the order of the integers, and the
    # expected base (decimal, octal, hexadecimal, etc).
    solution = hex(solution0)+" "+hex(solution1)+" "+hex(solution2)  # :string
    print(solution)
  else:
    raise Exception('Could not find the solution')

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