Codegate 2018 RedVelvet writeup

RedVelvet

gdb를 이용해 리버싱을 해보면 우선 사용자의 input을 받은 다음 func1 ~ func15 까지 15개의 함수에 사용자 input을 2~3개씩 쪼개서 각 함수의 인자로 넣어준다. 그리고 함수안에서 어떠한 계산 후 계산의 결과와 input 값이 일치하는지 확인 후 일치하면 HAPPINESS!라는 문자열이 출력된다.

한 함수라도 통과하지 못하면 프로그램이 종료한다.

함수를 전부 통과하게되면 각 함수마다 한번씩 총 15번 HAPPINESS!라는 문자열이 출력된 후 전부 통과하게 되면 플래그를 뱉어준다.

처음에는 손으로 직접 리버싱하여 함수를 분석한 후 약간(?) 노가다로 키를 구하는 방식으로 하다가 더 편한 방법을 찾았다.

python에 z3라는 라이브러리를 이용하면 수학식을 계산해서 값을 뽑아줄 수 있다.

 

func10까지는 노가다로 구했다가 func11부터 15까지는 라이브러리를 이용해 풀었다.

아래는 키를 구하는 코드다.

#sha256_hash = 0a435f46288bb5a764d13fca6c901d3750cee73fd7689ce79ef6dc0ff8f380e5
from z3 import *

s = Solver()

for i in range(1,27):
        globals()['a%i'%i]=BitVec('a%i'%i,32)

#func1
s.add(a1 * 2 * (a1 ^ a2)  - a2 == 0x2a6a)
s.add(a1 > 0x55)
s.add(a1 <= 0x5f)
s.add(a2 > 0x60)
s.add(a2 <= 0x6f)

#func2
s.add(a2 % a3 == 0x7)
s.add(a2 > 0x5a)

#func3
s.add(a3 / a4 +(a4 ^ a3) == 0x15)
s.add(a3 <= 0x63)
s.add(a4 <= 0x77)

#func4
s.add(a5 == 0x5f)

#func5
s.add((a6 + a5)^(a5 ^ a6 ^ a5 ) == 0xe1)
s.add(a5 > 0x5a)
s.add(a6 <= 0x59)

#func6
s.add(a6 <= a7)
s.add(a7 <= a8)
s.add(a6 > 0x55)
s.add(a7 > 0x6e)
s.add(a8 > 0x73)
s.add((a7+a8) ^ (a6 + a7) == 0x2c)
s.add((a7 + a8)%a6 + a7  == 0xa1)

#func7
s.add(a8 >= a9)
s.add(a9 >= a10)
s.add(a8 <= 0x77)
s.add(a9 > 0x5a)
s.add(a10 <= 0x59)
s.add((a8 + a10) ^ (a9 + a10) == 0x7a)
s.add((a8 + a10) % a9 + a10 == 0x65)

#func8
s.add(a10 <= a11)
s.add(a11 <= a12)
s.add(a12 <= 0x72)
s.add((a10 + a11) / a12 * a11 == 0x61)
s.add((a12 ^ (a10 - a11)) * a11 == 0xffffd898)

#func9
s.add(a12 == a13)
s.add(a13 >= a14)
s.add(a14 <= 0x63)
s.add(a14 + a12 * (a14 - a13) - a12 == 0xfffffa5d)

#func10
s.add(a14 >= a15)
s.add(a15 >= a16)
s.add(a15 * (a14 + a16 + 1) - a16 == 0x3c9a)
s.add(a15 > 0x5a)
s.add(a15 <= 0x63)

#func11
s.add(a17 >= a16)
s.add(a16 >= a18)
s.add(a17 > 0x64)
s.add(a17 <= 0x68)
s.add(a16 + (a17 ^ (a17- a18)) - a18 == 0x46)
s.add((a17 + a18) / a16 + a16 == 0x44)

#func12
s.add(a18 >= a19)
s.add(a19 >= a20)
s.add(a19 <= 0x3b)
s.add(a20 <= 0x2c)
s.add(a18 + (a19 ^ (a20 + a19)) - a20 == 0x6f)
s.add((a19 ^ (a19 - a20)) + a19 == 0x65)

#func13
s.add(a22 + (a21 ^ (a20 + a22)) - a20 == 0x10d)
s.add((a22 ^ (a21 - a20)) + a21 == 0xb9)
s.add(a20 <= a21)
s.add(a21 <= a22)
s.add(a20 > 0x28)
s.add(a21 > 0x5a)
s.add(a22 <= 0x6d)

#func14
s.add(a22 + (a23 ^ (a22 + a23)) - a24 == 0xb9)
s.add(a22 >= a24)
s.add(a23 >= a24)
s.add(a23 <= 0x63)
s.add(a24 > 0x5a)

#func15
s.add((a26 ^ ((a25 - a24) * a25)) - a24 == 0x4be)
s.add((a24 ^ ((a26 - a25) * a26)) + a25 == 0xfffffbf6)
s.add(a25 >= a26)
s.add(a25 >= a24)
s.add(a26 > 0x5f)
s.add(a25 <= 0x6d)

print s.check()
#print s.model()

if (s.check() == sat):
        values =s.model()
        flag=""
        for i in range(1,27):
                obj = globals()['a%i' % i]
                char = values[obj].as_long()
                flag += chr(char)
        print flag

FLAG : What_You_Wanna_Be?:)_lc_la

lc_la라고 나오는데 이 값을 your flag에 입력하면 flag를 뱉지 않는다.

gdb로 어셈을 보다보면 sha256으로 내가 입력한 flag를 암호화한 다음 gdb 내에 있는 0a435f46288bb5a764d13fca6c901d3750cee73fd7689ce79ef6dc0ff8f380e5 이 값과 비교를 해서 같으면 플래그를 뱉어준다.

아마 저 암호화된 값은 진짜 flag를 SHA256으로 암호화 한 것으로 보인다.

게싱으로 lc를 la로 바꿔서 What_You_Wanna_Be?:)_la_la로 입력하면 플래그를 뱉어준다.

Ref. http://revers3r.tistory.com/103?category=112084

Ref. https://github.com/AnisBoss/CTFs/blob/master/Codegate%20CTF%202018/RedVelvet%20-%20254pts%20(Rev)/solve.py