[Codegate 2018] RedVelvet

Codegate 2018 RedVelvet reversing 182pt

해당 문제는 64bit ELF 파일이다. 

먼저 IDA로 열고 분석하였다.

func1~15 함수에서 입력문을 비교하는데 z3아니면 angr 쓰라는 말 같다.

[z3 solve]

from z3 import *
 
s = Solver()
f = [BitVec("flag[%d]"%i, 16) for i in range(26)]
 
for i in range(26):
        s.add(f[i] >= 32)
        s.add(f[i] < 127)
 
 
s.add(f[0] * 2 * (f[1] ^ f[0]) - f[1] == 10858)
s.add(f[0] > 85)
s.add(f[0] <= 95)
s.add(f[1] > 96)
s.add(f[1] <= 111)
s.add(f[1] % f[2] == 7)
s.add(f[2] > 90)
s.add(f[2] / f[3] + (f[3] ^ f[2]) == 21)
s.add(f[2] <= 99)
s.add(f[3] <= 119)
v2 = f[4] ^ f[3] ^ f[4]
s.add((v2 % f[4]) + f[3] == 137)
s.add(f[3] > 115)
s.add(f[4] == 95)
s.add(((f[5] + f[4]) ^ (f[4] ^ f[5] ^ f[4])) == 225)
s.add(f[5] <= 89)
s.add(f[5] <= f[6])
s.add(f[6] <= f[7])
s.add(f[5] > 85)
s.add(f[6] > 110)
s.add(f[7] > 115)
s.add((f[6] + f[7]) ^ (f[5] + f[6]) == 44)
s.add((f[6] + f[7]) % f[5] + f[6] == 161)
s.add(f[7] >= f[8])
s.add(f[8] >= f[9])
s.add(f[7] <= 119)
s.add(f[8] > 90)
s.add(f[9] <= 89)
s.add((f[7] + f[9]) ^ (f[8] + f[9]) == 122)
s.add((f[7] + f[9]) % f[8] + f[9] == 101)
s.add(f[9] <= f[10])
s.add(f[10] <= f[11])
s.add(f[11] <= 114)
s.add((f[9] + f[10]) / f[11] * f[10] == 97)
s.add((f[11] ^ (f[9] - f[10])) * f[10] == 0xFFFFD898)
s.add(f[11] <= 114)
s.add(f[11] == f[12])
s.add(f[12] >= f[13])
s.add(f[13] <= 99)
s.add(f[13] + f[11] * (f[13] - f[12]) - f[11] == 0xFFFFFA5D)
s.add(f[13] >= f[14])
s.add(f[14] >= f[15])
s.add(f[14] * (f[13] + f[15] + 1) - f[15] == 15514)
s.add(f[14] > 90)
s.add(f[14] <= 99)
s.add(f[16] >= f[15])
s.add(f[15] >= f[17])
s.add(f[16] > 100)
s.add(f[16] <= 104)
s.add(f[15] + (f[16] ^ (f[16] - f[17])) - f[17] == 70)
s.add((f[16] + f[17]) / f[15] + f[15] == 68)
s.add(f[17] >= f[18])
s.add(f[18] >= f[19])
s.add(f[18] <= 59)
s.add(f[19] <= 44)
s.add(f[17] + (f[18] ^ (f[19] + f[18])) - f[19] == 111)
s.add((f[18] ^ (f[18] - f[19])) + f[18] == 101)
s.add(f[19] <= f[20])
s.add(f[20] <= f[21])
s.add(f[19] > 40)
s.add(f[20] > 90)
s.add(f[21] <= 109)
s.add(f[21] + (f[20] ^ (f[21] + f[19])) - f[19] == 269)
s.add((f[21] ^ (f[20] - f[19])) + f[20] == 185)
s.add(f[21] >= f[23])
s.add(f[22] >= f[23])
s.add(f[22] <= 99)
s.add(f[23] > 90)
s.add(f[21] + (f[22] ^ (f[22] + f[21])) -f[23] == 185)
s.add(f[24] >= f[25])
s.add(f[24] >= f[23])
s.add(f[25] > 95)
s.add(f[24] <= 109)
s.add(((f[24] - f[23]) * f[24] ^ f[25]) - f[23] == 1214)
s.add(((f[25] - f[24]) * f[25] ^ f[23]) + f[24] == 0xFFFFFBF6)
 
print s.check() 
arr = s.model()
 
flag = ''.join([chr(int(str(arr[f[i]]))) for i in range(0, 26)])
print flag #What_You_Wanna_Be?:)_l`_la

What_You_Wanna_Be?:)_l`_la -> What_You_Wanna_Be?:)_la_la (modify)

[angr_solve]

import angr
 
p = angr.Project("./RedVelvet", load_options={'auto_load_libs': False})
ex = p.surveyors.Explorer(find=0x401546, avoid=0x4007D0)
ex.run()
 
flag = ex.found[0].state.posix.dumps(0)
print flag[:26] #input length == 26

z3 과 마찬가지로 angr도 한글자가 틀린데 이 부분은 sha256 암호화 hash값 까지 비교해봐야 알겠지만 어차피 한글자만 다른거 같아서 게싱으로 a로 바꿔주고 인증하였다.