Codegate 2018 RedVelvet writeup

RedVelvet

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

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

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

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

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

 

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

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

?

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121

#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