[DreamHack] babycmp 문제 풀이_reversing_nabi

 

SERIAL을 구하는 문제입니다.

 

DA로 열었을 때, mfc로 GUI를 구현한 프로그램인 것을 확인할 수 있습니다.

이때 사용자 입력값을 찾아가는 방법은 여러가지가 있을 수 있지만 저는 두가지 방법으로 따라가보았습니다.

1. 사용자 입력값과 관련되어 호출되는 문자열을 따라간다.
2. Event ID를 이용하여 사용자 입력값을 검증하는 함수를 따라간다.

2번 방법은 인터넷에서 mfc를 분석할 수 있는 재미있는 방법인 것 같아 해당 예제로 공부해보았습니다. 좀 예전에 풀었던 문제인데 2번 분석을 해보고 싶어 다시 쓰게된 라업이라… 어떻게 풀었는지 잘 기억이 안납니다..ㅎㅎ 주석을 달아두었던 ida 파일도 삭제한 상태여서 처참히 코드만 남았습니다… (라업을 바로바로 작성해야하는 이유)

2번과 관련된 방법은 아래 링크를 참고해주시면 좋을 것 같습니다.

https://scorchingnraining.tistory.com/entry/Control-ID%EB%A1%9C-MFC-%ED%98%B8%EC%B6%9C-%ED%95%A8%EC%88%98%EB%A5%BC-%EC%B0%BE%EC%95%84%EB%B3%B4%EC%9E%90-MFC-%EB%A6%AC%EB%B2%84%EC%8B%B1

Control ID로 MFC 호출 함수를 찾아보자 (MFC 리버싱)

 

성공 문자열로 추측되는 GOT IT! 문자열이 호출되는 함수의 주소를 따라갔습니다.

 

IDA의 xref 기능을 이용하여 해당 문자열이 포함된 함수의 주소 sub_140001F60을 찾았습니다.

 

사용자 입력값을 바탕으로 검증하는 부분으로 추측되는 sub_140001C30 함수를 트레이싱하였습니다.

 

처음에는 복잡한 로직이라고 생각했는데 동적 분석으로 값을 따라가면서 확인해보니 어렵지 않았습니다….

flag를 얻는데는 필요없는 코드들이 많았고 연산해했던 부분은 2번째 사진에 있던 sub_140001A10 함수였습니다.

 

&v19가 사용자 input값이었고 &v17이 아마 리턴값을 저장하는 버퍼 주소였을겁니다... 아마….

 

아무튼 함수 내부로 들어가면 간단한 연산을 통해 flag 값을 검증하는 것을 확인할 수 있습니다.

그리고 연산값을 반환하여 아래 사진의 하드코딩된 값들과 비교하는 연산 구문을 확인할 수 있습니다.

 

지금도 정적 분석 코드만 보니 굉장히 헷갈리는데…ㅎㅎ

mfc는 동적으로 분석하는게 덜 헷갈리는거 같습니다…

허허 아무튼 제가 위에서 분석한 내용을 바탕으로 작성한 코드는 아래와 같습니다. z3를 이용해 풀이를 작성하였는데 역연산이 어려운 문제는 아니다보니 역연산을 이용해 코드를 재작성하면 좋을 것 같습니다…ㅎ

 

from z3 import *

solver = Solver()

variable_list = [BitVec('x{}'.format(i), 32) for i in range(24)]

key = "neko_hat"

hex_values = [0x40007608, 0x800075F6, 0xB0007607, 0x90007607, 0x000075FA, 0x50007604, 0xF00075FF, 0x40007616,
              0x20007607, 0x300075FB, 0xF0007609, 0x30007608, 0xD00075F7, 0x00007604, 0xF00075FF, 0xF0007610,
              0xD0007606, 0x100075F8, 0x50007603, 0x40007607, 0x300075FA, 0x20007604, 0x100075FE, 0xD0007612]

for i in range(24):
    temp = LShR(variable_list[i], 4) | ((variable_list[i] & 0xF) << 28)
    temp ^= ord(key[i % 8])
    temp += ord(key[i % 4])
    temp += 30000
    solver.add(temp == hex_values[i])

if solver.check() == sat:
    model = solver.model()
    print([model.eval(variable_list[i]) for i in range(24)])
else:
    print("No solution found.")

이 10진수를 아스키로 변환하면 플래그가 나옵니다..!