Trollcat CTF - Solver

 

 

어려운 문제가 아니니까, 간단하게 풀이할 수 있다.

 

Key를 buf에 입력받고, sub_1200 함수를 통해 비교한다.

 

z3를 사용하는 문제이다. 왜 문제이름도 Solver인지 알 수 있다.

 

from z3 import *

# Creates solver
s = Solver()

# Creates an array of variables to solve for
flag = [BitVec('flag%i'%i,8) for i in range(0, 22)]

# checks that variables are in range
for i in range(0, 22):
    s.add(flag[i] >= 48)
    s.add(flag[i] <= 122)

# adds all the checks
s.add(flag[0] + flag[3] == 100)
s.add(flag[1] + flag[18] == 214)
s.add(flag[2] + flag[4] == 178)
s.add(flag[5] ^ flag[6] == 76)
s.add(flag[8] - flag[7] == 17)
s.add(flag[10] - flag[9] == 59)
s.add(flag[12] + flag[11] - flag[13] == 69)
s.add(flag[15] + flag[14] - flag[16] == 31)
s.add(flag[16] + flag[17] - flag[18] == 88)
s.add((flag[20] ^ flag[19]) ^ flag[21] == 69)

# print if we were able to solve or not
print(s.check())
print(s.model())
# gets the variables
m = s.model()

# initializes an empty dictionary
t = {}

# parses the model to dictionary
for a in str(m)[1:-1].split(','):
    t[a.split('=')[0].strip()] = a.split('=')[1].strip()

# creates the string from the variables
s =""
for i in [BitVec('flag%i'%i, 8) for i in range(0, 22)]:
    s += chr(int(t[str(i)]))

# prints the string
print(s)