Pico CTF 2018 keygen-me-2

전형적인 키젠미 문제고 z3를 사용해 주면 된다.

z3에 사용될 조건들을 보면 조금 특이한게 인풋들이 custom ord,mod 함수를 통해 재 정의된다. 

해당 함수들이 하는 역할은 0~9,A~Z의 ascii 값을 0~35의 int형 값으로 변환해 주는 역할을 한다.

위 형식에 맞춰 z3로 구해진 값을 다시 변환해주면 유효한 input이 나오고 해당 input을 통해 원격 서버의 바이너리를 실행해보면 플래그를 구할 수 있다.

solve.py

from z3 import *

def custom_ord(data):
    if And(data>47,data<58):
        return data-48
    elif And(data>64,data<91):
        return data-55
    else:
        print "Not Found Custom Ord!!!! Exit!!!"
        exit(1)

def custom_mod(data1,data2):
    return data1%data2


a1 = []
for i in xrange(16):
    a1.append(z3.Int('a1['+str(i)+']'))
s = Solver()

for i in xrange(16):
    s.add(And(a1[i]>-1,a1[i]<36))
    #s.add(custom_mod(custom_ord(a1[0])+custom_ord(a1[1]),36)==14)
    s.add(custom_mod(a1[0]+a1[1],36)==14)
    s.add(custom_mod(a1[2] + a1[3], 36) == 24)
    s.add(custom_mod(a1[2] - a1[0], 36) == 6)
    s.add(custom_mod(a1[1] + a1[3] + a1[5], 36) == 4)
    s.add(custom_mod(a1[2] + a1[4] + a1[6], 36) == 13)
    s.add(custom_mod(a1[3] + a1[4] + a1[5], 36) == 22)
    s.add(custom_mod(a1[6] + a1[8] + a1[10], 36) == 31)
    s.add(custom_mod(a1[1] + a1[4] + a1[7], 36) == 7)
    s.add(custom_mod(a1[9] + a1[12] + a1[15], 36) == 20)
    s.add(custom_mod(a1[13] + a1[14] + a1[15], 36) == 12)
    s.add(custom_mod(a1[8] + a1[9] + a1[10], 36) == 27)
    s.add(custom_mod(a1[7] + a1[12] + a1[13], 36) == 23)


flag = ""
if s.check() == z3.sat:
    try:
        m = s.model()
        print m
        for i in range(0, 16):
            if int(str(m[a1[i]]))<10:
                flag += chr(int(str(m[a1[i]]))+48)
            else:
                flag += chr(int(str(m[a1[i]])) + 55)
        print flag
    except:
        print "Not Found"