ISITDTU CTF 2019 Quals Writeup

I played the ISITDTU CTF 2019 Quals as a member of zer0pts. We got 7655 points and reached 10th place. Excepting that the score server was very slow entire the competition and some of challenges were not CTF challenges, I almost enjoyed this competition. Thank you admins for holding this CTF!

[Reverse 100points] Pytecode

We were given a disassembled python bytecode file. Because it had a simple structure, I could decompile it by my hand. As it gave a lot of constraints for the input, I used the z3 to determine the correct input.

from z3 import *

flag = [Int("x%d" % i) for i in range(30)]
solver = Solver()

for f in flag:
    solver.add(0x20 <= f, f <= 0x7F)

solver.add(flag[0] + 52 == flag[-1])
solver.add(flag[-1] - 2 == flag[7])
for i, c in enumerate("ISITDTU"):
    solver.add(flag[i] == ord(c))

solver.add(flag[9] == flag[14])
solver.add(flag[19] == flag[14])
solver.add(flag[19] == flag[24])
solver.add(flag[8] == 49)
solver.add(flag[8] == flag[16])

for i, c in enumerate("d0nT"):
    solver.add(flag[i + 10] == ord(c))

# solver.add(ord("0") <= flag[18], flag[18] <= ord("9"))
# solver.add(ord("0") <= flag[23], flag[23] <= ord("9"))
# solver.add(ord("0") <= flag[28], flag[28] <= ord("9"))
# solver.add(flag[18] - ord("0") + flag[23] - ord("0") + flag[28] - ord("0") == 9)
# solver.add(flag[18] == flag[28])
solver.add(flag[18] == ord("3"))
solver.add(flag[23] == ord("3"))
solver.add(flag[28] == ord("3"))

solver.add(flag[15] == ord("L"))
# solver.add(Xor(flag[17], -10) == -99)
solver.add(flag[17] == 107)
solver.add(flag[20] + 2 == flag[27])
solver.add(flag[27] == 100)
solver.add(flag[20] >= 97)
solver.add(flag[27] % 100 == 0)
solver.add(flag[25] == ord("C"))
solver.add(
    ord("0") <= flag[26],
    flag[26] <= ord("9"),
    flag[26] % 2 == 0,
    flag[26] % 3 == 0,
    flag[26] % 4 == 0,
)
solver.add(ord("0") <= flag[23], flag[23] <= ord("9"), flag[23] == ord("3"))
solver.add(flag[22] == flag[13] + 0x20)

solver.add(sum(flag) == 2441)
solver.add(flag[7] == ord("{"))
solver.add(flag[9] == ord("_"))
# solver.add(flag[21] == ord("y"))


if solver.check() != sat:
    print("unsat")
    exit()

model = solver.model()
flag_str = ""
for f in flag:
    flag_str += chr(model[f].as_long())
print(flag_str)

This script outs ISITDTU{1_d0nT_L1k3_b:t3_C0d3}.

## [Crypto 304] Chaos When I connected the server, it gave me the encoded key to get the flag. The server encoded arbitrary messages I sent. It formed like a `55/uu/&&/ff 00/ii/KK/((/(( ...`. By the observations, I found the rule of encoding. You can understood the rule from the following solution code.

from ptrlib import Socket
import random
import string


def decrypt(mes):
    chars = mes.split(" ")
    plain = ""
    for char in chars:
        elements = char.split("/")
        if len(elements) == 5:
            plain += char[-1]
        elif len(elements) == 3:
            plain += char[0]
        elif elements[2][0] in "~`!@#$%^&*()_-+=<,>.?|":
            plain += elements[1][0]
        else:
            plain += elements[2][0]
    return plain

sock = Socket("104.154.120.223", 8085)
sock.recvuntil("Your cipher key: ")
line = sock.recvline().decode().rstrip()
key = decrypt(line)
sock.recvuntil("Your choice: ")
sock.sendline("2")
sock.recvuntil("Please enter the key to get flag: ")
sock.sendline(key)
sock.interactive()

[Programming 100points] Do you like math?

This is not a CTF challenge.

from ptrlib import Socket

symbols = [
    [
        """
  #
 ##
# #
  #
  #
  #
#####
""",
        "1",
    ],
    [
        """
 #####
#     #
      #
 #####
#
#
#######
""",
        "2",
    ],
    [
        """
 #####
#     #
      #
 #####
      #
#     #
 #####
""",
        "3",
    ],
    [
        """
#
#    #
#    #
#    #
#######
     #
     #
""",
        "4",
    ],
    [
        """
#######
#
#
######
      #
#     #
 #####
""",
        "5",
    ],
    [
        """
 #####
#     #
#
######
#     #
#     #
 #####
""",
        "6",
    ],
    [
        """
#######
#    #
    #
   #
  #
  #
  #
""",
        "7",
    ],
    [
        """
 #####
#     #
#     #
 #####
#     #
#     #
 #####
""",
        "8",
    ],
    [
        """
 #####
#     #
#     #
 ######
      #
#     #
 #####
""",
        "9",
    ],
    [
        """
  ###
 #   #
#     #
#     #
#     #
 #   #
  ###
""",
        "0",
    ],
    [
        """

  #
  #
#####
  #
  #

""",
        "+",
    ],
    [
        """

 #   #
  # #
#######
  # #
 #   #

""",
        "*",
    ],
    [
        """



#####




""",
        "-",
    ],
]


def get_symbol(lines, p):
    for sym in symbols:
        is_this = True
        for i, symline in enumerate(sym[0].split("\n")):
            if i >= len(lines):
                break
            if not lines[i][p:].startswith(symline):
                is_this = False
                break
        if is_this:
            width = 0
            for symline in sym[0].split("\n"):
                width = max(width, len(symline))
            return (sym[1], width + p + 1)
    return ("=", p)


sock = Socket("104.154.120.223", 8083)

cnt = 0
while True:
    lines = []
    for _ in range(9):
        line = sock.recvline().decode().rstrip()
        print(line, flush=True)
        lines.append(line)
    sock.recvuntil(">>> ")

    expr = ""
    p = 0
    while True:
        sym, p = get_symbol(lines, p)
        if sym == "=":
            break
        expr += sym
    print("{}: {}".format(cnt, expr))
    sock.sendline(str(eval(expr)))
    cnt += 1

    if cnt == 100:
        break

sock.interactive()