By chaem | February 15, 2018
RedVelvet 출제자 WriteUp
우와 여러분! codegate2018의 예선이 끝났습니다!!!
이번 codegate는 저에게 의미가 새롭네요! 내가 codegate 문제를 내다니!!!
(나는 왜 여기있는가, 나는 누구인가 하하하 @@)
codegate문제를 내야한다고 했을때 진짜 무섭고, 스트레스 만땅이었는데… 어찌어찌 문제를 내고, 어찌어찌 예선을 끝내고, 이렇게 롸업을 쓰고있네요 호호
여러분 저 궁금한 게 있는데, 원래 이렇게 많이 풀리는 쉬운 문제있어야 하는거 맞죠?ㅎㅎㅎ
제 문제는 여러분들께 꿈과 희망을 드리기 위한 문제라ㅎㅎㅎ 롸업이 필요한 분이 없으실 것 같지만!
한 자, 한 자 적어보도록 하겠습니다!!! 저도 다른 분들처럼 어마어마한 문제를 만들게 될 그날까지…☆
우선, 문제 푸신 분들의 롸업을 봤는데 다들 너무 열심히 풀어 주셔서 감사했어요!!!
어려운 문제를 냈어도 뿌듯했겠지만, 많은 분들이 풀어주시는 것도 뿌듯하더군요!! 제 문제를 풀며 성취감을 느낀 주니어 친구들이 있는 것 같아 마음이 따끈따끈했습니닿ㅎㅎㅎ
사실, 이 문제가 원래 이렇게 간단한 문제가 아니었답니다…ㅎㅎ
호기롭게 “angr가 푸는 데 조금이라도 오래걸리는 문제를 만들자!“라는 마인드로 시작하였으나ㅎㅎㅎ 제가 angr 사용이 미숙한 탓에… 결국 문제는 점점 쉬워지고ㅎㅎㅎ
롸업을 보니 z3 / angr / guessing 을 이용하여 다양하게 문제들을 푸신 것 같아요!!! 완전 당황스러웠던 guessing을 한 팀이 있었는데 ㅋㅋㅋ 그 정도면 guessing 장인으로 인정하겠습니다 ㅎㅎ
그럼 Codegate2018 예선전의 첫번째 문제로 출제 된 레드벨벳 문제에 대해 이야기 해보겠습니다.
바이너리는 사용자로부터 입력값을 받고, 입력값이 적절한지 확인한 후 입력값이 맞다면 flag를 출력하는 구조입니다. 입력값으로는 총 27글자를 입력받고, 글자의 일부를 함수의 인자로 사용하는 15개의 함수를 통과 한 후에 sha256 해시와 비교하여 해시값이 맞을 경우 flag를 얻을 수 있다는 것을 알 수 있습니다. 각각의 함수는 문자열의 일부를 인자로 받아 특정한 연산을 진행한 후, 결과가 맞다면 HAPPINESS:)를 출력 후 다음 함수로 넘어가고, 틀리면 바로 프로그램을 종료 합니다.
먼저 angr 를 이용하여 다음과 같이 간단하게 풀이할 수 있습니다. 도달하고자 하는 곳의 주소를 find에, 피하고자 하는 주소를 avoid에 넣어주면 됩니다.
import angr
BUF_LEN = 100
def char(state, c):
'''returns constraints s.t. c is printable'''
return state.solver.And(c <= '~', c >= ' ')
p = angr.Project('./RedVelvet', auto_load_libs=False)
state = p.factory.entry_state()
print('adding constaints to stdin')
for i in range(BUF_LEN):
c = state.posix.files[0].read_from(1)
state.solver.add(char(state, c))
state.posix.files[0].seek(0)
state.posix.files[0].length = BUF_LEN
sm = p.factory.simgr(state)
sm.explore(find=0x401606, avoid=(0x401621, 0x401419, 0x4007D0))
print sm.found[-1].posix.dumps(0)angr를 통해 다음과 같이 flag를 획득할 수 있습니다!
다음은 z3 solver로 푸는 방법입니다. 리버싱을 통해 각 함수를 통과하는 조건을 알아내어 식에 대입하면, 해당 식을 모두 만족하는 값을 solver가 찾아줍니다.
from z3 import *
import hashlib
def func1(a1, a2):
s.add(a1 * 2 * (a2 ^ a1) - a2 == 10858)
s.add(a1 > 85, a1 <= 95, a2 > 96, a2 <= 111)
def func2(a1, a2):
s.add(a1 % a2 == 7)
s.add(a2 > 90)
def func3(a1, a2):
s.add( a1 / a2 + (a2 ^ a1) == 21, a1 <= 99, a2 <= 119 )
def func4(a1, a2):
s.add(((a2 ^ a1 ^ a2) % a2) + a1 == 137, a1 > 115, a2 <= 99, a2 == 95)
def func5(a1, a2):
s.add(((a2 + a1) ^ (a1 ^ a2 ^ a1)) == 225, a1 > 90, a2 <= 89 )
def func6(a1, a2, a3):
s.add( a1 <= a2 )
s.add( a2 <= a3 )
s.add( a1 > 85, a2 > 110, a3 > 115, ((a2 + a3) ^ (a1 + a2)) == 44, (a2 + a3) % a1 + a2 == 161 )
def func7(a1, a2, a3):
s.add( a1 >= a2 )
s.add( a2 >= a3 )
s.add( a1 <= 119, a2 > 90, a3 <= 89, ((a1 + a3) ^ (a2 + a3)) == 122, (a1 + a3) % a2 + a3 == 101 )
def func8(a1, a2, a3):
s.add( a1 <= a2 )
s.add( a2 <= a3 )
s.add( a3 <= 114, (a1 + a2) / a3 * a2 == 97, (a3 ^ (a1 - a2)) * a2 == -10088, a3 <= 114 )
def func9(a1, a2, a3):
s.add( a1 == a2 )
s.add( a2 >= a3 )
s.add( a3 <= 99, a3 + a1 * (a3 - a2) - a1 == -1443 )
def func10(a1, a2, a3):
s.add( a1 >= a2 )
s.add( a2 >= a3 )
s.add( a2 * (a1 + a3 + 1) - a3 == 15514, a2 > 90, a2 <= 99 )
def func11(a1, a2, a3):
s.add( a2 >= a1 )
s.add( a1 >= a3 )
s.add( a2 > 100, a2 <= 104, a1 + (a2 ^ (a2 - a3)) - a3 == 70, (a2 + a3) / a1 + a1 == 68 )
def func12(a1, a2, a3):
s.add( a1 >= a2 )
s.add( a2 >= a3 )
s.add( a2 <= 59, a3 <= 44, a1 + (a2 ^ (a3 + a2)) - a3 == 111, (a2 ^ (a2 - a3)) + a2 == 101 )
def func13(a1, a2, a3):
s.add( a1 <= a2 )
s.add( a2 <= a3 )
s.add( a1 > 40, a2 > 90, a3 <= 109, a3 + (a2 ^ (a3 + a1)) - a1 == 269, (a3 ^ (a2 - a1)) + a2 == 185 )
def func14(a1, a2, a3):
s.add( a1 >= a3 )
s.add( a2 >= a3 )
s.add( a2 <= 99, a3 > 90, a1 + (a2 ^ (a2 + a1)) - a3 == 185 )
def func15(a1, a2, a3):
s.add( a2 >= a3 )
s.add( a2 >= a1 )
s.add( a3 > 95, a2 <= 109, ((a2 - a1) * a2 ^ a3) - a1 == 1214, ((a3 - a2) * a3 ^ a1) + a2 == -1034 )
flag_l = []
while True:
xs = [BitVec("x%d" % i, 16) for i in range(26)]
s = Solver()
func1(xs[0], xs[1]);
func2(xs[1], xs[2]);
func3(xs[2], xs[3]);
func4(xs[3], xs[4]);
func5(xs[4], xs[5]);
func6(xs[5], xs[6], xs[7]);
func7(xs[7], xs[8], xs[9]);
func8(xs[9], xs[10], xs[11]);
func9(xs[11], xs[12], xs[13]);
func10(xs[13], xs[14], xs[15]);
func11(xs[15], xs[16], xs[17]);
func12(xs[17], xs[18], xs[19]);
func13(xs[19], xs[20], xs[21]);
func14(xs[21], xs[22], xs[23]);
func15(xs[23], xs[24], xs[25]);
for fake in flag_l:
s.add(Not(And(fake[0] == xs[0], fake[1] == xs[1], fake[2] == xs[2], fake[3] == xs[3], fake[4] == xs[4], fake[5] == xs[5], fake[6] == xs[6], fake[7] == xs[7], fake[8] == xs[8], fake[9] == xs[9], fake[10] == xs[10], fake[11] == xs[11], fake[12] == xs[12], fake[13] == xs[13], fake[14] == xs[14], fake[15] == xs[15], fake[16] == xs[16], fake[17] == xs[17], fake[18] == xs[18], fake[19] == xs[19], fake[20] == xs[20], fake[21] == xs[21], fake[22] == xs[22], fake[23] == xs[23], fake[24] == xs[24], fake[25] == xs[25])))
r = s.check()
if r == sat:
m = s.model()
t = ''
for i in xrange(len(xs)):
t += chr(m[xs[i]].as_long())
print(repr(t))
if hashlib.sha256(t) == '0a435f46288bb5a764d13fca6c901d3750cee73fd7689ce79ef6dc0ff8f380e':
break
flag_l.append(map(ord, list(t)))
else:
print r
break이렇게 z3 solver를 통해 flag를 획득하는 것도 가능합니다.
문제를 풀어주신 모든 분들, 수고하셨습니다 :)