BugsBunny CTF 2017 Rev150

바이너리는 64bit elf 파일이고 메인함수를 보면 입력값을 받아서 아래와 같이 여러함수를 거친 후 플래그를 출력해준다.

먼저 numeric 함수를 보면 입력값에서 48을 뺀 값이 9이하인지 확인을 한다. 이를 통해 입력값이 0~9까지의 숫자여야 한다는걸 알 수 있다.

이후 함수들에 대해 분석해보면 각 함수별로 입력값을 통해 여러가지 연산을 하고 있는데 z3로 각 연산에 만족하는 수를 구해주면 된다.

중간에 결과값이 0인 연산과 같은 경우 a[11]이 0일 것이기 때문에 제외한 후 따로 s.add((a[11] - 48) == 0) 요렇게 a[11]을 0으로 지정해줬다. 

from z3 import *

a = []
s = Solver()
for i in range(0,20):
    a.append(BitVec('a['+str(i)+']',8))
    s.add(a[i]<=57,a[i]>=48)

s.add((a[11] - 48) == 0)
s.add((a[15] - 48 + a[4] - 48) == 10)
s.add((a[1] - 48) * (a[18] - 48) == 2)
s.add((a[15] - 48) / (a[9] - 48) == 1)
s.add(a[5] - a[17] == -1)
s.add(a[15] - a[1] == 5)
s.add((a[1] - 48) * (a[10] - 48) == 18)
s.add(a[8] - 48 + a[13] - 48 == 14)
s.add((a[18] - 48) * (a[8] - 48) == 5)
#s.add((a[4] - 48) * (a[11] - 48) == 0)
s.add(a[8] - 48 + a[9] - 48 == 12)
s.add(a[12] - a[19] == 1)
s.add((a[9] - 48) % (a[17] - 48) == 7)
s.add((a[14] - 48) * (a[16] - 48) == 40)
s.add(a[7] - a[4] == 1)
s.add(a[6] - 48 + a[0] - 48 == 6)
s.add(a[2] == a[16])
s.add(a[4] - a[6] == 1)
s.add((a[0] - 48) % (a[5] - 48) == 4)
#s.add((a[5] - 48) * (a[11] - 48) == 0)
s.add((a[10] - 48) % (a[15] - 48) == 2)
#s.add((a[11] - 48) / (a[3] - 48) == 0)
s.add(a[14] - a[13] == -4)
s.add(a[18] - 48 + a[19] - 48 == 3)
s.add(a[3] - 48 + a[17] - 48 == 9)

flag = ""

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

Flag = 42813724579039578812