Grammar Lesson -- TU CTF 2017

Points: 150

Solves: ???

Description:

I do declare this to challenge to be at least mildly engaging, and certainly useful going forwards

flag format: TUCTF{…}

Given:

A file with a set of restrictions in Prolog that the keys have to satisfy in order to pass the check.

Solution

(by L0rdComm4nder)

TLDR

The prolog code encodes a series of constraints that are easily encoded in Z3

Description

Looking at the given files one notices the existence of two important functions tokenizer and checkkey.

The tokenizer function basically transforms character codes into the corresponding characters 0 to 9 and a few others ( ) , - &.

The checkkey function checks the validity of the generated keys.

These constraints are easily encoded in Z3 and we know that a key should be of the form (XX,XX-XX,XX&XX,XX-XX,XX) and satisfy some conditions.

#!/usr/bin/env python3
from z3 import *
from pwn import *

SERVER = "grammarlesson.tuctf.com"
PORT = 6661


s = Solver()
flag = [Int('flag%d' % i) for i in range(25)]
p = [Int('p%d' % i) for i in range(8)]
q = [Int('q%d' % i) for i in range(8)]
o = [Int('o%d' % i) for i in range(8)]

def is_digit(x):
    s.add(x >= 0)
    s.add(x <= 9)

s.add(flag[0] == ord('('))
is_digit(flag[1])
is_digit(flag[2])
s.add(flag[3] == ord(','))
is_digit(flag[4])
is_digit(flag[5])

s.add(flag[1]+flag[2] == p[0])
s.add(flag[4]+flag[5] == p[1])
s.add(p[0]*p[1] == q[0])

s.add(flag[6] == ord('-'))

is_digit(flag[7])
is_digit(flag[8])
s.add(flag[9] == ord(','))
is_digit(flag[10])
is_digit(flag[11])

s.add(flag[7]+flag[8] == p[2])
s.add(flag[10]+flag[11] == p[3])
s.add(p[2]*p[3] == q[1])
s.add(q[0] + q[1] == o[0])

s.add(flag[12] == ord('&'))

is_digit(flag[13])
is_digit(flag[14])
s.add(flag[15] == ord(','))
is_digit(flag[16])
is_digit(flag[17])

s.add(flag[13]+flag[14] == p[4])
s.add(flag[16]+flag[17] == p[5])
s.add(p[4]*p[5] == q[2])

s.add(flag[18] == ord('-'))

is_digit(flag[19])
is_digit(flag[20])
s.add(flag[21] == ord(','))
is_digit(flag[22])
is_digit(flag[23])

s.add(flag[19]+flag[20] == p[6])
s.add(flag[22]+flag[23] == p[7])
s.add(p[6]*p[7] == q[3])
s.add(q[2] + q[3] == o[1])

s.add(o[0] * o[1] == 82944)

s.add(flag[24] == ord(')'))


def hack(x):
    if x>=0 and x<=9:
        return chr(x +48)
    else:
        return chr(x)

chan = remote(SERVER, PORT, timeout=9999)
chan.recvuntil(': ')

rounds=0
while z3.sat == s.check():
    rounds += 1
    m = s.model()
    plaint = "".join([ hack(int(repr(m[flag[i]]))) for i in range(len(flag)) ])
    print plaint
    chan.sendline(plaint)
    if rounds == 10:
        break
    chan.recvuntil(': ')
    block = []
    for i in range(len(flag)):
        block.append( flag[i] != m[flag[i]])
    s.add(Or(block))

chan.interactive()

Running the above script, and submitting the 10 first retrieved flags one gets

(99,99-99,99&92,38-10,16)
(88,88-88,80&81,97-09,35)
(88,75-78,88&80,86-08,64)
(88,77-58,88&80,77-08,91)
(88,77-58,88&80,77-08,82)
(88,77-58,88&80,07-08,98)
(88,67-68,88&80,66-08,84)
(88,67-38,88&80,76-08,86)
(88,67-92,88&80,56-08,88)
(88,67-92,88&80,46-08,89)
TUCTF{Gr4mm3r_1s_v3ry_imp0rtAnT!_4ls0_Pr0log_iz_c00l!}