UUTCTF2019 Again find the flag

풀 이

2019.05.05 00:02

main함수

문제는 check함수의 결과값에 따라 결과가 달라집니다.

 

형식 및 문자 검사

입력한 시리얼은 어떤 형태를 가지는데 위 과정에서 형식을 검사합니다. 시리얼은 5의 배수자리에 '_'가 위치하고 그 외의 모든 시리얼은 0~9의 값만 가지게 됩니다.

 

Ascii to number

저희가 입력한 문자열은 Ascii 문자입니다. 때문에 ascii 문자 '0'~'9'를 정수타입인 0~9로 바꿀 필요가 있습니다. 위 과정은 Ascii코드에서 0x30('0')을 빼 정수로 만들고 있습니다.

 

시리얼 검증

시리얼은 몇가지 검사를 수행하는데 먼저 특정 구역의 시리얼은 1보다 커야하거나 7보다 작아야하거나 등의 조건이 있습니다. 마지막으로 각 요소들을 더하거나 나누는 등 작업을 하고 몇가지 검사를 하는데, 만약 이 과정을 사람이 직접 풀게된다면 굉장히 힘든 작업이 됩니다. 이때 사용하는 라이브러리가 z3라는 특정 조건에 해당하는 미지수를 찾아주는 라이브러리를 사용합니다.

 

위 조건을 z3의 형태로 입력하면 다음과 같은 스크립트가 완성됩니다.

from z3 import *

# https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
def get_models(F, M):
    s = Solver()
    count = 0
    s.add(F)
    while count < M and s.check() == sat:
        m = s.model()
        count += 1
        yield m
        # Create a new constraint the blocks the current model
        block = []
        for d in m:
            # d is a declaration
            if d.arity() > 0:
                raise Z3Exception("uninterpreted functions are not supported")
            # create a constant from declaration
            c = d()
            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                raise Z3Exception("arrays and uninterpreted sorts are not supported")
            block.append(c != m[d])
        s.add(Or(block))

s = []
d = [BitVec('i%d' % i, 16) for i in xrange(16)]

for i in xrange(4):
    s.append(And(d[i] > 0, d[i] <= 9))
    s.append(And(d[i+4] >= 2, d[i+4] <= 8)) # 2 ~ 8
    s.append(And(d[i+8] >= 0, d[i+8] <= 9)) # nothing
    s.append(And(d[i+12] >= 3, d[i+12] <= 7))

for i in xrange(12, 16):
    s.append(d[i] - 3 < 5)
for i in xrange(0, 4):
    s.append(d[i] >= 1)
for i in xrange(4, 8):
    s.append(d[i] - 2 < 7)

f = []
for i in xrange(0, 4): 
    f.append(d[i] != d[i+8])
s.append(And(f))

f = []
for i in xrange(0, 4): 
    f.append(d[i+4] != d[i+12])
s.append(And(f))

iv3 = sum(d[0:4])
iv7 = sum(d[4:8])
iv5 = sum(d[8:12])
iv4 = sum(d[12:16])
s.append((iv3+iv7+iv5)/3 == iv4)
s.append(iv5/3 == iv3)
s.append(iv3 != iv7)

for A in get_models(s, 20):
    ans = []
    uc = 1
    for i in d:
        ans.append(str(A[i]))
        if uc % 4 == 0:
            ans.append('_')
        uc += 1

    x = "".join(ans[:-1])
    print x

 

'풀 이' 카테고리의 다른 글

단순한 로그인  (0) 2019.05.15
UUTCTF2019 Again find the flag  (0) 2019.05.05
드래곤  (0) 2019.04.30
SECCON2018/pwn/profile  (0) 2018.11.14
h3x0rCTF/pwn/libsteak  (0) 2018.11.04
hacklu2018/pwn/baby-kernel  (0) 2018.10.23