CCE 2020 - Maetdol
2020.09 라온화이트햇 핵심연구팀 최규범 kbchoi@raoncorp.com
목차
개요
CCE 2020 예선 리버싱 문제 Maetdol 풀이 보고서입니다.
대회 종료까지 4팀이 해결한 문제로, 패킹과 관련된 속임수때문에 문제 풀이에 혼돈을 주었습니다.
문제 해결까지 중간 중간 실패한 과정들도 포함하여, 문제 풀이 과정을 상세히 작성해보았습니다.
바이너리 분석
먼저, Maetdol.exe를 Hex Editor로 기본적인 정보를 살펴보았다.
Section 정보에서 UPX 패커 정보를 알 수 있다.
UPX 패커의 '-d' 옵션을 통해서 바이너리를 Unpack 하였다.
IDA를 통해 Unpack한 바이너리를 열고, 0x401000 주소를 분석하였다. (Windows 환경의 실행 파일 대부분이 해당 주소에서 주요 기능을 수행한다.)
무언가 Hash로 보이는 데이터를 저장하는 것으로 보인다.
scanf를 통해 입력 값을 받은 후, 최상위 비트가 존재하는지 확인한다.
입력 받은 글자 수가 55글자인지, 0x80 미만의 출력 가능한 문자열인지 확인한다.
글자 시작이 'cce2020{M'인지 확인 후, 입력 받은 글자를 이진 문자열로 변환한다.
'0'을 7개 더한 후 변환한 이진 문자열의 크기가 392인지 확인한다.
55개의 입력을 받고 7개의 '0'을 더했으므로 해당 이진 문자열 크기는 392가 된다.
55 * 7 + 7 = 392
그리고 어떠한 연산을 수행하여 다시 배열에 저장한다.
디버깅을 통해 입력 값 → 이진 문자열 → 배열의 관계를 확인해보았다.
위 비교 조건을 만족하는 임의 값을 입력하여 진행하였다.
마지막 배열을 저장하는 Maetdol.exe+0x16CB를 디버깅하여 확인하였다.
처음에는 0xC7이 저장된다.
위와 같은 데이터가 배열에 저장되었다. 이진 데이터로 보면, '11000111 10001110 10011010 ...' 이다.
입력 값 'cce...'를 이진 데이터로 보면, '01100011 01100011 01100101 ...' 이다.
'11000111 10001110 10011010 ...' ⇒ 저장된 배열
'01100011 01100011 01100101 ...' ⇒ 'cce...'
자세히 보니 둘과의 관계가 일부 보인다.
우선 이미 상위 비트를 검사하였기에, 입력 값에서 7개 비트만 사용한 것을 알 수 있다.
'e' ⇒ 1100101 ⇒ 1010011
또한 이진 문자열로 변경하면서, 그 순서를 뒤집은 것으로 보여진다.
이후 저장된 배열을 8바이트 단위로 더하여 저장한다.
그리고 Hash 함수로 추정되는 sub_403634를 호출하고, 그 결과 Hash를 저장한다.
그리고 처음 저장된 6개의 Hash와 비교하는 것으로 추정된다.
모두 일치할 경우 해당 입력 값이 Flag일 것이다.
이제 Hash 함수로 추정되는 sub_403634를 분석해야한다.
sub_403634 함수는 위와 같이 동작한다. (무언가 복잡한 식이 많고, 이미 존재하는 함수처럼 보일 때는 구글 검색해보는 것이 좋다.)
함수 시작에서 사용되는 값을 검색하였다.
SHA1과 MD5에 대한 결과가 보이며 비교하는 Hash의 길이를 보았을 때, MD5로 추정된다.
Wikipedia에서 MD5 의사 코드를 발견하였는데, sub_403634와 아주 동일한 형태를 띄고 있다.
sub_403634는 MD5 Hash 함수임을 알 수 있다.
"그치만"
단방향 함수인 MD5 Hash를 역으로 계산할 방법은 없어보인다.
하지만 분명 풀 수 있게 낸 문제이므로, 무언가 해결에 필요한 속임수가 존재할 것이다. "그치만... 동적 디버깅이라도 하지 않으면, Hash 값이 이상한지 알 수 없는 걸..."
먼저 sub_403634 함수의 인자를 원하는 값으로 넣고, 실제 MD5의 값과 비교하였다.
그 결과, 알던 것과는 너무나도 다른 내용의 무언가가 나왔다.
64회 수행되는 위 MD5 알고리즘의 결과가 저장되는 곳과, 반복문이 끝나는 지점을 확인했다.
실제 MD5 Hash의 연산 중간 값 64개와, 마지막 연산의 결과를 비교해본다.
64번 반복되어야 할 연산이, 기묘하게도 16번만 반복하고 끝난다.
"대체 무슨 사연이..? 취재팀은 급하게 반복문 조건으로 발길을 돌렸다."
반복문 조건을 확인해보니, 본래 64회 반복해야할 내용이 16회로 달라져있다.
보고도 믿기지 않아 어려번 재실행해보았지만, 16회 반복으로 되어있었다.
UPX 패커의 '-d' 옵션 결과와 실행하여 Unpack 된 내용이 다르도록, 특정 속임수가 있는 것 같다.
역연산
16회만 반복 연산할 경우, F값이 정해지는 조건은 일정해진다.
연산에 사용되는 M[g]의 경우, 위와 같은 형태로 구성되며 4바이트 단위로 쓰인다.
중간에 사용되는 K, s는 고정된 참조 값이다.
" 1/4 밖에 안남은 MD5를 보았다. 웅장하게 코드를 수호하던 그 MD5 맞나..?"
def md5_custom(buf):
a0 = 0x67452301 # A
b0 = 0xefcdab89 # B
c0 = 0x98badcfe # C
d0 = 0x10325476 # D
data = [buf & 0xFFFFFFFF, (buf >> 32) & 0xFFFFFFFF, 0x80, 0,
0, 0, 0, 0,
0, 0, 0, 0,
0, 0, 0x40, 0 ]
A, B, C, D = a0, b0, c0, d0
for i in range(16):
F = ((B & C) | (D & (~B))) & 0xFFFFFFFF
tmp = (A + F + K[i] + data[i]) & 0xFFFFFFFF
new_B = (B + ROL(tmp, R[i])) & 0xFFFFFFFF
A, B, C, D = D, new_B, B, C
a0 = (a0 + A) & 0xFFFFFFFF
b0 = (b0 + B) & 0xFFFFFFFF
c0 = (c0 + C) & 0xFFFFFFFF
d0 = (d0 + D) & 0xFFFFFFFF
return [a0, b0, c0, d0]위 내용을 토대로 4등분 된 MD5 함수를 구현하였다.
8바이트 입력 값을 제외한 나머지 연산에 필요한 값(data[2] ~ data[16], K, R)을 모두 알고 있다.
def rev_md5_custom(result):
A = (result[0] - 0x67452301) & 0xFFFFFFFF
B = (result[1] - 0xefcdab89) & 0xFFFFFFFF
C = (result[2] - 0x98badcfe) & 0xFFFFFFFF
D = (result[3] - 0x10325476) & 0xFFFFFFFF
data = [1, 1, 0x80, 0,
0, 0, 0, 0,
0, 0, 0, 0,
0, 0, 0x40, 0]
"""
F <= ((B & C) | (D & (~B)))
new_A <= D
new_B <= B + ROL( (A + F + K[i] + data[i]), R[i] )
new_C <= B
new_D <= C
"""
for i in range(15, 1, -1):
orgD = A
orgB = C
orgC = D
tmp = ROR(B - C, R[i])
F = ((orgB & orgC) | (orgD & (~orgB)))
orgA = tmp - F - K[i] - data[i]
orgA &= 0xFFFFFFFF
A,B,C,D = orgA, orgB, orgC, orgD따라서, 역연산을 통해 4등분 된 MD5 함수의 "2번째 반복문 중간 결과(A,B,C,D)"를 알아낼 수 있다.
A = 0x67452301
B = 0xEFCDAB89
C = 0x98BADCFE
D = 0x10325476
#i : 0
F1 = ((B & C) | (D & (~B))) & 0xFFFFFFFF
tmp = (A + F1 + K[0] + data[0])
new_B1 = (B + ROL(tmp, R[0])) & 0xFFFFFFFF
A, B, C, D = D, new_B, B, C
#A1 : D
#B1 : new_B1
#C1 : B
#D1 : C
#i : 1
F2 = ((new_B & B) | (C & (~new_B))) & 0xFFFFFFFF
# ((B1 & C1)|(D1 & (~B1))) & 0xFFFFFFFF
tmp = (D + F2 + K[1] + data[1])
# (A1 + F + K[1] + data[1])
new_B2 = (new_B1 + ROL(tmp, R[1])) & 0xFFFFFFFF
A, B, C, D = D, new_B, B, C
#A2 : C
#B2 : new_B2 = (new_B1 + ROL((D + ((new_B & B)|(C & (~new_B))) + K[1] + data[1]), R[1]))
#C2 : new_B1 = (B + ROL((A + ((B & C) | (D & (~B))) + K[0] + data[0]), R[0]))
#D2 : B"2번째 반복문 중간 결과(A,B,C,D)"는 위와 같다.
new_B1의 역연산을 통해서 첫번째 입력 값 data[0]을 구할 수 있다.
이후 new_B1을 통해 new_B2의 역연산이 가능해지고, data[1]을 구할 수 있게 된다.
문제 풀이 코드
from pwn import *
f = open("Maetdol_unpacked.exe", "rb")#UPX Unpacked Binary
data = f.read()
f.close()
R,K = [],[]
tmp = data[0x1C3A0:0x1C3A0+0x100]
for i in range(0, 0x100, 4):
R.append(u32(tmp[i:i+4]))
tmp = data[0x1C4A0:0x1C4A0+0x100]
for i in range(0, 0x100, 4):
K.append(u32(tmp[i:i+4]))
def ROL(x, c):
x &= 0xFFFFFFFF
return ((x << c) | (x >> (32 - c))) & 0xFFFFFFFF
def ROR(x, c):
x &= 0xFFFFFFFF
return ((x >> c) | (x << (32 - c))) & 0xFFFFFFFF
def reverse_md5_custom(res):
A = (res[0] - 0x67452301) & 0xFFFFFFFF
B = (res[1] - 0xEFCDAB89) & 0xFFFFFFFF
C = (res[2] - 0x98BADCFE) & 0xFFFFFFFF
D = (res[3] - 0x10325476) & 0xFFFFFFFF
data = [1, 1, 0x80, 0,
0, 0, 0, 0,
0, 0, 0, 0,
0, 0, 0x40, 0]
for i in range(15, 1, -1):
orgD = A
orgB = C
orgC = D
to_rotate = ROR(B - C, R[i])
F = ((orgB & orgC) | (orgD & (~orgB)))
orgA = to_rotate - F - K[i] - data[i]
orgA &= 0xFFFFFFFF
A,B,C,D = orgA, orgB, orgC, orgD
x0 = (ROR((C - 0xefcdab89), R[0]) - 0x67452301 - 0x98badcfe - K[0]) & 0xFFFFFFFF
F0 = 0x98badcfe
new_B = (0xefcdab89 + ROL(0x67452301 + F0 + K[0] + x0, R[0])) & 0xFFFFFFFF
F1 = ((new_B & 0xefcdab89) | (0x98badcfe & (~new_B)))
x1 = (ROR(B - C, R[1]) - 0x10325476 - F1 - K[1]) & 0xFFFFFFFF
return (x1 << 32) + x0
import z3
goal = [[0x3b1d2597, 0xda0fa46a, 0x6d8bbe1c, 0xeef458e9],
[0x7f526ea1, 0xf7523f94, 0xe22f7b6f, 0x4c753bd2],
[0x80fc359e, 0x09eebdae, 0x8a4834f5, 0x370642cd],
[0xbac882bf, 0xb7a23e35, 0xdb1cfff9, 0x994b2ce6],
[0x605be09c, 0x418902f1, 0x53808dfb, 0x83c2964f],
[0x9c32a2b5, 0x0eee2f36, 0x119dbf2c, 0xd31fb222]]
x = [ z3.BitVec('x%i' % i, 64) for i in range(6)]
s = z3.Solver()
s.add(z3.Or(x[0] == 0xB36F83C9609A8EC7, x[0] == 0xB26F83C9609A8EC7))
#cce2020{M
for i in range(6):
sm = x[i] + x[(i + 1) % 6]
s.add(sm == rev(goal[i]))
if s.check() == z3.sat:
m = s.model()
enc = [0] * 6
for d in m.decls():
if str(d)[0] == 'x':
enc[int(str(d)[1:])] = int(str(m[d]))
enc_s = b""
for i in range(6):
enc_s += p64(enc[i])
dec_s = ""
for x in enc_s:
dec_s += bin(x)[2:].rjust(8, "0")
flag = b""
for i in range(0, len(dec_s), 7):
flag += bytes([int(dec_s[i:i+7][::-1], 2)])
print(flag)
#cce2020{M4r13_Anto1ne773_did_n0t_s4y_l3t_7h3m_eat_c4K3=
#cce2020{M4r13_Anto1ne773_did_n0t_s4y_l3t_7h3m_eat_c4K3}