Codegate 2018 CTF RedVelvet

코드를 보면 대충 입력값을 15개 함수를 통해 연산을 하고 이에 만족하는 값을 구해주면 된다. 간단히 z3나 angr로 풀면되는데 angr는 아직 제대로 써보질 못해서 일단 z3로 풀었다. angr도 익혀서 담에 풀어봐야겠다.

from z3 import *

input= []
for i in xrange(26):
    input.append(z3.BitVec('input[' + str(i) + ']',16))

s = Solver()

s.add(input[0] * 2 * (input[1] ^ input[0]) - input[1] == 10858)
s.add(input[0] > 85)
s.add(input[0] <= 95)
s.add(input[1] > 96)
s.add(input[1] <= 111)
s.add(input[1] % input[2] == 7)
s.add(input[2] > 90)
s.add(input[2] / input[3] + (input[3] ^ input[2]) == 21)
s.add(input[2] <= 99)
s.add(input[3] <= 119)
s.add(input[3] > 115)
s.add(input[4] <= 99)
s.add(input[4] == 95)
s.add(((input[5] + input[4]) ^ (input[4] ^ input[5] ^ input[4])) == 225)
s.add(input[5] <= 89)
s.add(input[5] <= input[6])
s.add(input[6] <= input[7])
s.add(input[5] > 85)
s.add(input[6] > 110)
s.add(input[7] > 115)
s.add(((input[6] + input[7]) ^ (input[5] + input[6])) == 44)
s.add((input[6] + input[7]) % input[5] + input[6] == 161)
s.add(input[7] >= input[8])
s.add(input[8] >= input[9])
s.add(input[7] <= 119)
s.add(input[8] > 90)
s.add(input[9] <= 89)
s.add(((input[7] + input[9]) ^ (input[8] + input[9])) == 122)
s.add((input[7] + input[9]) % input[8] + input[9] == 101)
s.add(input[9] <= input[10])
s.add(input[10] <= input[11])
s.add(input[11] <= 114)
s.add((input[9] + input[10]) / input[11] * input[10] == 97)
s.add((input[11] ^ (input[9] - input[10])) * input[10] == -10088)
s.add(input[11] <= 114)
s.add(input[11] == input[12])
s.add(input[12] >= input[13])
s.add(input[13] <= 99)
s.add(input[13] + input[11] * (input[13] - input[12]) - input[11] == -1443)
s.add(input[13] >= input[14])
s.add(input[14] >= input[15])
s.add(input[14] * (input[13] + input[15] + 1) - input[15] == 15514)
s.add(input[14] > 90)
s.add(input[14] <= 99)
s.add(input[16] >= input[15])
s.add(input[15] >= input[17])
s.add(input[16] > 100)
s.add(input[16] <= 104)
s.add(input[15] + (input[16] ^ (input[16] - input[17])) - input[17] == 70)
s.add((input[16] + input[17]) / input[15] + input[15] == 68)
s.add(input[17] >= input[18])
s.add(input[18] >= input[19])
s.add(input[18] <= 59)
s.add(input[19] <= 44)
s.add(input[17] + (input[18] ^ (input[19] + input[18])) - input[19] == 111)
s.add((input[18] ^ (input[18] - input[19])) + input[18] == 101)
s.add(input[19] <= input[20])
s.add(input[20] <= input[21])
s.add(input[19] > 40)
s.add(input[20] > 90)
s.add(input[21] <= 109)
s.add(input[21] + (input[20] ^ (input[21] + input[19])) - input[19] == 269)
s.add((input[21] ^ (input[20] - input[19])) + input[20] == 185)
s.add(input[21] >= input[23])
s.add(input[22] >= input[23])
s.add(input[22] <= 99)
s.add(input[23] > 90)
s.add(input[21] + (input[22] ^ (input[22] + input[21])) - input[23] == 185)
s.add(input[24] >= input[25])
s.add(input[24] >= input[23])
s.add(input[25] > 95)
s.add(input[24] <= 109)
s.add(((input[24] - input[23]) * input[24] ^ input[25]) - input[23] == 1214)
s.add(((input[25] - input[24]) * input[25] ^ input[23]) + input[24] == -1034)

flag = ""

if s.check() == z3.sat:
    try:
        m = s.model()
        for i in range(0, 26):
            flag += chr(int(str(m[input[i]])))
        print flag
    except:
        print "Not Found"

Flag = What_You_Wanna_Be?:)_la_la