[Codegate 2018] RedVelvet

  Reversing 분야의 문제이다. 사용자로부터 flag 값을 입력받는다. 바이너리에는 총 15개의 flag 검증 루틴이 존재하고, 사용자로부터 입력받아 검증된 flag가 SHA256으로 연산했을 때 특정 값과 동일해야 한다.

  중간에 Anti-Reversing이 걸려있긴 한데, 바이너리 패치로 간단하게 우회할 수 있으므로 무시해도 되며, 중요한 부분은 func 함수와 SHA256 연산 후, strcmp 함수이다. func 함수의 루틴은 z3나 순수 리버싱으로 풀어도 되지만, 귀찮아서 angr를 사용하였다.

angr 소스코드

#!/usr/bin/python
import angr
 
def main():
    p = angr.Project('./RedVelvet', load_options={"auto_load_libs": False})
    state = p.factory.blank_state(addr=0x4011A9)
 
    hinput = state.se.BVS('input', 27 * 8)
    for byte in hinput.chop(8):
        state.add_constraints(byte >= 0x20)
        state.add_constraints(byte <= 0x7D)
 
    state.add_constraints(hinput.chop(8)[0] == 'W')
    state.add_constraints(hinput.chop(8)[1] == 'h')
    state.add_constraints(hinput.chop(8)[2] == 'a')
    state.add_constraints(hinput.chop(8)[3] == 't')
    state.add_constraints(hinput.chop(8)[4] == '_')
    state.add_constraints(hinput.chop(8)[5] == 'Y')
    state.add_constraints(hinput.chop(8)[6] == 'o')
    state.add_constraints(hinput.chop(8)[7] == 'u')
    state.add_constraints(hinput.chop(8)[8] == '_')
    state.add_constraints(hinput.chop(8)[9] == 'W')
    state.add_constraints(hinput.chop(8)[10] == 'a')
    state.add_constraints(hinput.chop(8)[11] == 'n')
    state.add_constraints(hinput.chop(8)[12] == 'n')
    state.add_constraints(hinput.chop(8)[13] == 'a')
    state.add_constraints(hinput.chop(8)[14] == '_')
    state.add_constraints(hinput.chop(8)[15] == 'B')
    state.add_constraints(hinput.chop(8)[16] == 'e')
    state.add_constraints(hinput.chop(8)[17] == '?')
    state.add_constraints(hinput.chop(8)[18] == ':')
    state.add_constraints(hinput.chop(8)[19] == ')')
    state.add_constraints(hinput.chop(8)[20] == '_')
    state.add_constraints(hinput.chop(8)[21] == 'l')
    state.add_constraints(hinput.chop(8)[22] == 'c')
    state.add_constraints(hinput.chop(8)[23] == '_')
    state.add_constraints(hinput.chop(8)[24] == 'l')
    state.add_constraints(hinput.chop(8)[25] == 'a')
    
 
    path_group = p.factory.simgr(state)
    path_group.explore(find=0x401606, avoid=0x401626)
 
    found = path_group.found[0]
    print found.state.posix.dumps(0).split('\0')[0]
 
if __name__ == '__main__':
    main()
 

  angr의 수행 결과, "What_You_Wanna_Be?:)_lc_la" 라는 문자열을 얻을 수 있었는데, 실제로 입력해 보면 검증루틴을 전부 통과하는 것을 확인할 수 있다. 이것으로 풀리면 좋겠지만, 아쉽게도 SHA256으로 연산된 해시 값의 결과가 다르기 때문에 인증 flag는 아니다. 그래서 z3를 추가로 사용하여 값을 확인해 보았다.

z3 소스코드

#!/usr/bin/python
from z3 import *
 
def solver1(s, x, y):
    s.add(x * 2 * (y ^ x) - y == 10858, x > 85, x <= 95, y > 96, y <= 111)
 
def solver2(s, x, y):
    s.add(x % y == 7, y > 90 )
 
def solver3(s, x, y):
    s.add(x / y + (y ^ x) == 21, x <= 99, y <= 119)
 
def solver4(s, x, y):
    s.add(((y ^ x ^ y) + ((y ^ x ^ y) >> 32)*0x100000000 % y) + x == 137, x > 115 y == 95)
 
def solver5(s, x, y):
    s.add(((y + x) ^ (x ^ y ^ x)) == 225, x > 90, y <= 89)
 
def solver6(s, x, y, z):
    s.add(x <= y, y <= z, x > 85, y > 110, z > 115, ((y + z) ^ (x + y)) == 44, (y + z) % x + y == 161)
 
def solver7(s, x, y, z):
    s.add(x >= y, y >= z, x <= 119, y > 90, z <= 89, ((x + z) ^ (y + z)) == 122, (x + z) % y + z == 101)
 
def solver8(s, x, y, z):
    s.add(x <= y, y <= z, z <= 114, (x + y) / z * y == 97, (z ^ (x - y)) * y == -10088, z <= 114)
 
def solver9(s, x, y, z):
    s.add(x == y, y >= z, z <= 99, z + x * (z - y) - x == -1443)
 
def solver10(s, x, y, z):
    s.add(x >= y, y >= z, y * (x + z + 1) - z == 15514, y > 90, y <= 99)
 
def solver11(s, x, y, z):
    s.add(y >= x, x >= z, y > 100, y <= 104, x + (y ^ (y - z)) - z == 70, (y + z) / x + x == 68)
 
def solver12(s, x, y, z):
    s.add(x >= y, y >= z, y <= 59, z <= 44, x + (y ^ (z + y)) - z == 111, (y ^ (y - z)) + y == 101)
 
def solver13(s, x, y, z):
    s.add(x <= y, y <= z, x > 40, y > 90, z <= 109, z + (y ^ (z + x)) - x == 269, (z ^ (y - x)) + y == 185)
 
def solver14(s, x, y, z):
    s.add(x >= z, y >= z, y <= 99, z > 90, x + (y ^ (y + x)) - z == 185)
 
def solver15(s, x, y, z):
    s.add(y >= z, y >= x, z > 95, y <= 109, ((y - x) * y ^ z) - x == 1214, ((z - y) * z ^ x) + y == -1034)
 
def main():
    array = [ BitVec('a%i'%i,8) for i in range(0,26)]
 
    s = Solver()
#    solver1(s, array[0], array[1])
#    solver2(s, array[1], array[2])
#    solver3(s, array[2], array[3])
#    solver4(s, array[3], array[4])
#    solver5(s, array[4], array[5])
#    solver6(s, array[5], array[6], array[7])
#    solver7(s, array[7], array[8], array[9])
#    solver8(s, array[9], array[10], array[11])
#    solver9(s, array[11], array[12], array[13])
#    solver10(s, array[13], array[14], array[15])
#    solver11(s, array[15], array[16], array[17])
#    solver12(s, array[17], array[18], array[19])
    solver13(s, array[19], array[20], array[21])
    solver14(s, array[21], array[22], array[23])
    solver15(s, array[23], array[24], array[25])
 
    for i in range(0, 26):
        s.add(array[i] >= 0x20 and array[i] <= 0x7e)
 
    print s.check()
    print s.model()
 
if __name__ == '__main__':
    main()
 

  중간 중간 sat를 만족하지 않는 식이 작성되어, angr의 결과를 어느정도 신뢰하여 주석처리 하였다. 그래서 맨 뒷 9자를 확인해본 결과, "?:)_l`_la"를 얻을 수 있었다. angr의 결과와 매우 유사한데, 이유는 solver14의 결과로 제법 다양한 값이 나올 수 있기 때문에 그렇다. 검증 루틴을 전부 통과할 수 있는 flag 값은 여러 개이지만, SHA256 해시 값이 다르게 되는 이유이다.

  c와 `를 넣으면 검증 루틴을 통과하지만, 인증 flag가 아니기 때문에 더 다양한 문자가 나올 수 있다고 추측할 수 있고, `와 c 사이의 문자를 하나씩 입력해본 결과, a인 것을 확인할 수 있었다.