04_angr_symbolic_stack

지난번 글을 보지 않았다면 먼저 보고 오자

03_angr_symbolic_registers

시작

이번에는 스택에 symbolic value를 넣어 스택의 값을 구하는 방법을 알아보겠다

이번 내용은 함수의 호출과정에서의 스택의 변화를 알 필요가 있기 때문에 예제의 환경인 x86환경에서의 함수 호출과정을 알고 난 뒤에 보는게 좋다

C언어 함수 호출과정 - x86

예제

먼저, main함수를 기드라로 까본다

undefined4 main(void)

{
  printf("Enter the password: ");
  handle_user();
  return 0;
}

handle_user가 가장 중요한 부분인것 같으니 이어서 까보자

void handle_user(void)

{
  int local_14;
  int local_10 [3];
  
  __isoc99_scanf("%u %u",local_10,&local_14);
  local_10[0] = complex_function0(local_10[0]);
  local_14 = complex_function1(local_14);
  if ((local_10[0] == 0x773024d1) && (local_14 == -0x43bcee31)) {
    puts("Good Job.");
  }
  else {
    puts("Try again.");
  }
  return;
}

변수 타입이 조금 깨지긴 했지만 입력받는 부분을 보면 unsigned int 타입인 것을 유추할 수 있다

이번에도 입력을 받을때 포멧 스트링을 사용했다

그렇다면 이번에도 레지스터에 symbolic value를 집어넣을 수 있을까?

안타깝게도 이번에는 스택에 들어간 입력을 레지스터로 옮기는 과정을 거치지 않는다

그도 그럴것이 저번에는 입력 받는 함수가 따로 있어서 그 반환값을 옮기느라 레지스터가 사용된 것이지만 이번에는 입력받은 변수를 함수 내부에서 바로 사용하기 때문이다

그래서 이때 필요한 것이 스택이다

풀이 코드 작성

scaffold04.py를 보자

import angr
import claripy
import sys

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

  start_address = ???
  initial_state = project.factory.blank_state(addr=start_address)

  initial_state.regs.ebp = initial_state.regs.esp

  password0 = claripy.BVS('password0', ???)
  ...

  padding_length_in_bytes = ???  # :integer
  initial_state.regs.esp -= padding_length_in_bytes

  initial_state.stack_push(???)  # :bitvector (claripy.BVS, claripy.BVV, claripy.BV)
  ...

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return ???

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return ???

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

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

    solution0 = solution_state.se.eval(password0)
    ...

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

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

Part 0

import angr
import claripy
import sys

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

  start_address = ???
  initial_state = project.factory.blank_state(addr=start_address)

위 8줄을 넘기고 start_address를 보자

전처럼 blank_state를 통해 initial_state의 주소를 start_address로 지정한다

그렇다면 이번에는 어디서 simgr가 시작해야 할까?

일단 입력과 검사를 모두 handle_user함수에서 하기 때문에 이 함수 내에서 시작하는 것이 맞아 보인다

출력도 handle_user함수에서 하기 때문에 handle_user에서 시작해도 된다

그렇다면 어떻게 스택에 symbolic value를 넣을 수 있을까?

바로 우리가 함수 프롤로그를 실행한 것처럼 세팅해주면 된다

이 과정은 밑에서 할 테니 일단 start_address에 handle_user함수의 주소가 들어가도 된다고 생각하고 주소를 찾아보자

 

일단 call __isoc99_scanf 뒤에서 시작해야 입력받은 값이 메모리에 들어있는 상태일 것이다

입력받은 값이 메모리에 들어있는 주소여야 당시 스택의 상황을 구했을 때 입력값을 알 수 있다

 

그리고

mov eax, dword ptr [ebp + local_10 ]
sub esp, 0xc
push eax

부분은 complex_function0을 실행하기 위해 인자를 넘기는 부분이므로 그 전의 주소를 넣어야 한다

그렇다면 그 사이에 있는 add esp, 0x10는 어떤 역할일까?

바로 scanf의 스택을 정리하는 부분이다

그래서 이 명령뒤의 주소를 넣어야 한다

종합해보면, add esp, 0x10 뒤, mov eax, dword ptr [ebp + local_10 ] 전의 주소인 0x08048697을 넣어야 하는 것이다

Part 1

initial_state.regs.ebp = initial_state.regs.esp

password0 = claripy.BVS('password0', ???)
...

padding_length_in_bytes = ???  # :integer
initial_state.regs.esp -= padding_length_in_bytes

이제 아까 미뤄놓은 함수 프롤로그 세팅을 해줄 차례이다

먼저, mov ebp, esp를 해 준다

initial_state.regs.ebp에 initial_state.regs.esp를 넣어주면 된다

그다음에 password가 나오는데 이건 잠시 미뤄두고 아래줄부터 보자

padding_length_in_bytes에 어떤 정수를 넣어야 한다

이 값은 esp값을 얼마만큼 뺄 것인지에 대한 변수이다

그렇다면

sub esp, 0x18

sub esp, 0x4 에 따라 0x18 + 0x4를 넣으면 될까?

그렇지 않다. 일단 저 부분은 scanf를 호출할 때 인자를 넘기기 위한 스택 확장이 들어있고, 뒤에 add esp, 0x10이 다시 정리를 한다

그렇다고 0x18 + 0x4 - 0x10을 넣는 것도 아니다

이따가 나오겠지만, 우리가 스택에 symbolic value를 넣을 때 push하듯 넣는다

그래서 지금은 push를 두번 하면 각각 dword ptr [ebp + local_10]와 dword ptr [ebp + local_14]에 자리잡는 스택의 모습을 만들어야 한다

현재 python 코드 상의 스택의 구조는 이렇게 생겼을 것이다

push를 한 번 하면 local_10, 한번 더 하면 local_14에 symbolic value가 들어가려면 esp를 ebp-8로 설정해야 한다

따라서 padding_length_in_bytes에 8을 넣어 esp - padding_length_in_bytes를 했을때 esp가 ebp-8을 가리키고 있는 상태가 되도록 한다

 

아까 넘겼던 password는 전에 만들었던 것처럼 claripy의 BVS로 만든다

32bit 프로그램이므로 ???에는 32를 넣으면 된다

Part 2

  initial_state.stack_push(???)  # :bitvector (claripy.BVS, claripy.BVV, claripy.BV)
  ...

  simulation = project.factory.simgr(initial_state)

여기가 symbolic value를 push하는 부분이다

state의 stack_push를 사용하면 그 state의 스택에 특정 값을 push할 수 있다

우리는 symbolic value를 push해서 스택 상황을 구할 건데, 그냥 ???에 아까 만든 password 변수를 넣어주면 된다

그 다음 initial_state에서 시작하는 simgr를 만들면 된다

Part 3

  def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return ???

  def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return ???

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

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

    solution0 = solution_state.se.eval(password0)
    ...

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

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

나머진 똑같다

최종 코드

import angr
import claripy
import sys

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

  start_address = 0x08048697
  initial_state = project.factory.blank_state(addr=start_address)

  initial_state.regs.ebp = initial_state.regs.esp

  password0 = claripy.BVS('password0', 32)
  password1 = claripy.BVS('password1', 32)

  padding_length_in_bytes = 0x8
  initial_state.regs.esp -= padding_length_in_bytes

  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)

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

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

흐름을 정리하면 다음과 같다

1. scanf의 스택 정리가 끝나고 결과를 레지스터에 넣게 직전, 0x08048697을 initial_state로 한다

2. 함수 프롤로그를 건너뛰고 시작하기 때문에 이를 직접 실행해줘야 한다

2-1. mov ebp, esp에 대한 initial_state.regs.ebp = initial_state.regs.esp를 한다

2-2. esp에서 8을 빼서 push를 하면 ebp-0xc 위치에 들어가게끔 스택을 만들어준다

3. 스택에 symbolic value를 push해서 프로그램이 원하는 주소를 실행하면 처음의 스택 상황이 뭐였는지 구할 수 있게 한다

결과

실행하면 1704280884 2382341151가 나왔고, 그대로 프로그램에 넣으면 Good Job.이 나온다

지금까지 스택에 symbolic value를 넣고 값을 찾는 방법을 알아보았다

다음에는 특정 주소에 대한 메모리를 직접 찾는 방법을 알아보겠다