picoCTF 2018 keygen-me-2 Write up

z3 쓰는 괜찮은 문제인거같아서 가져왔다

리버싱 공부좀 해야지

 

이거보면 return 이 대충 0부터 시작하고 35까지 하는걸 알수 있다.

 

이 스테이지 전부다 통과해야되니까

결국 z3돌리라는 말이다.

 

from z3 import *

def m(a, b):
      return If(a % b >= 0,
    a % b,
    a % b + b)

s = Solver()

v = []
for i in range(16):
  e = Int('v'+str(i))
  v.append(e)
  s.add(e >= 0)
  s.add(e <= 35)

s.add(m(v[0] + v[1], 36) == 14)
s.add(m(v[2] + v[3], 36) == 24)
s.add(m(v[2] - v[0], 36) == 6)
s.add(m(v[1] + v[3] + v[5], 36) == 4)
s.add(m(v[2] + v[4] + v[6], 36) == 13)
s.add(m(v[3] + v[4] + v[5], 36) == 22)
s.add(m(v[6] + v[8] + v[10], 36) == 31)
s.add(m(v[1] + v[4] + v[7], 36) == 7)
s.add(m(v[9] + v[12] + v[15], 36) == 20)
s.add(m(v[13] + v[14] + v[15], 36) == 12)
s.add(m(v[8] + v[9] + v[10], 36) == 27)
s.add(m(v[7] + v[12] + v[13], 36) == 23)

print(s.check())

z3 짤때 다른 블로그 참고를 많이 했다. 아닌가 그냥 그대로 갖고왔다. 이것밖에 좋은게 없네

 

values = [31, 19, 1, 23, 1, 34, 11, 23, 8, 7, 12, 0, 16, 20, 31, 33]

output = ''
for i in range(0, 16):
  v = values[i]
  print v
  if v < 10:
    output += chr(v+0x30)
  else:
    output += chr(v+0x37)

print output

그래서 z3 나온값으로 다시 문자열 복구시켜주면 된다.

 

이게 z3다 보니까 output이 전부다 다를 수 있다.