2018 Codegate RedVelvet

위에 보이는 func 함수들은 각각 연산을 하면서 값을 체크한다.

그래서 이 연산들을 해주기 위해 z3를 사용했다.

from z3 import*
 
var = [BitVec('var[%d]' %i,16) for i in range(0,26)]
 
 
 
s = Solver()
 
s.add(var[0] * 2 *(var[1] ^ var[0]) - var[1] == 10858)
 
s.add(var[0] > 85)
 
s.add(var[0] <= 95)
 
s.add(var[1] > 96)
 
s.add(var[1] <= 111)
 
 
 
s.add(var[1] % var[2] == 7)
 
s.add(var[2] > 90)
 
 
 
s.add(var[2]/var[3]+(var[3]^var[2]) == 21)
 
s.add(var[2]<=99)
 
s.add(var[3]<=119)
 
 
 
v2 = (var[4]^var[3]^var[4])
 
s.add((v2 % var[4])+var[3] == 137)
 
s.add(var[3] > 115)
 
s.add(var[4] <= 99)
 
s.add(var[4] == 95)
 
 
 
s.add(((var[5] + var[4]) ^ (var[4] ^ var[5] ^ var[4])) == 225)
 
s.add(var[4]>90)
 
s.add(var[5]<=89)
 
 
 
s.add(var[5]<=var[6])
 
s.add(var[6]<=var[7])
 
s.add(var[5]>85)
 
s.add(var[6]>110)
 
s.add(var[7]>115)
 
s.add((var[6]+var[7])^(var[5]+var[6]) == 44)
 
s.add((var[6]+var[7])%var[5]+var[6] == 161)
 
 
 
s.add(var[7]>=var[8])
 
s.add(var[8]>=var[9])
 
s.add(var[7]<=119)
 
s.add(var[8]>90)
 
s.add(var[9]<=89)
 
s.add((var[7]+var[9])^(var[8]+var[9])==122)
 
s.add((var[7]+var[9])%var[8]+var[9] == 101)
 
 
 
s.add(var[9]<=var[10])
 
s.add(var[10]<=var[11])
 
s.add(var[11]<=114)
 
s.add((var[9]+var[10])/var[11]*var[10]==97)
 
s.add((var[11]^(var[9]-var[10]))*var[10] == -10088)
 
s.add(var[11]<=114)
 
 
 
s.add(var[11] == var[12])
 
s.add(var[12]>=var[13])
 
s.add(var[13]<=99)
 
s.add(var[13]+var[11]*(var[13]-var[12])-var[11]== -1443)
 
 
 
s.add(var[13]>=var[14])
 
s.add(var[14]>=var[15])
 
s.add(var[14] * (var[13] + var[15] + 1) - var[15] == 15514)
 
s.add(var[14]>90)
 
s.add(var[14]<=99)
 
 
 
s.add(var[16]>=var[15])
 
s.add(var[15]>=var[17])
 
s.add(var[16]>100)
 
s.add(var[16]<=104)
 
s.add(var[15]+(var[16]^(var[16]-var[17]))-var[17]==70)
 
s.add((var[16]+var[17])/var[15]+var[15] == 68)
 
 
 
s.add(var[17]>=var[18])
 
s.add(var[18]>=var[19])
 
s.add(var[18]<=59)
 
s.add(var[19]<=44)
 
s.add(var[17] + (var[18] ^ (var[19] + var[18])) - var[19] == 111)
 
s.add((var[18] ^ (var[18] - var[19])) + var[18] == 101)
 
 
 
s.add(var[19] <= var[20])
 
s.add(var[20] <= var[21])
 
s.add(var[19]>40)
 
s.add(var[20]>90)
 
s.add(var[21]<=109)
 
s.add(var[21] + (var[20] ^ (var[21] + var[19])) - var[19] == 269)
 
s.add((var[21] ^ (var[20] - var[19])) + var[20] == 185)
 
 
 
s.add(var[21]>=var[23])
 
s.add(var[22]>=var[23])
 
s.add(var[22]<=99)
 
s.add(var[23]>90)
 
s.add(var[21] + (var[22] ^ (var[22] + var[21])) - var[23] == 185)
 
 
 
s.add(var[24]>=var[25])
 
s.add(var[24]>=var[23])
 
s.add(var[25]>95)
 
s.add(var[24]<=109)
 
s.add(((var[24] - var[23]) * var[24] ^ var[25]) - var[23] == 1214)
 
s.add(((var[25] - var[24]) * var[25] ^ var[23]) + var[24] == -1034)
 
 
print s.check()
print s.model()

이렇게 연산을 진행하면

이렇게 값이 나온다 이걸 이제 순서대로 문자로 바꿔주면

What_You_Wanna_Be?:)_l`_la 라고 나온다.

근데 이대로 넣으니까 인증이 안된다. 근데 `을 보고 la la가 아닐까? 생각해서 `를 a로 바꾸고 인증하니까 됐다.

z3는 처음 써봤는데 신기했다. 다음에는 angr도 써봐야겠다. 그리고 레드벨벳은 예쁘다.

FLAG: What_You_Wanna_Be?:)_la_la