Plaid CTF 2020 Write-up 2 - YOU wa SHOCKWAVE

2020-04-19 ctf reverse engineering

Story

Feeling stifled by the large crowd gathered in the entrance plaza, you open up your minimap and try to find somewhere to search far away from the entrance gate. Ah, perfect—there’s some kind of library on the other side of the Sanctum. A nice, quiet place to search alone for a bit.

Entering the library, you find that your guess the library would be quiet was… rather faulty. As the door swings closed behind you, instead of a soft bell that one might expect to hear, you’re greeted with the wail of an electric guitar, quickly followed by some heavy drums. Perhaps not a great place to sit quietly, but at least it seems like you’ve got the place to yourself!

You find yourself drawn to a section labeled “anime” (perhaps this is some sort of multimedia collection?), and everything there is spinning and flashing and generally making your eyes hurt a little. But there’s got to be a flag hiding somewhere behind the seizure-inducing mess, right?

The files

The challenge file is an archive containing .dlls and .exes, main executable is called Projector.exe. Running this showed a classy window that puts modern design to shame.

Designer UI

Here, it prompts for the flag.

Some investigation online revealed that these files relates to Macromedia Shockwave. We also learned that the logic is contained in the .dcr file, which is a compressed version of a .dir Director file. It contains the associated assets and instructions, originally written in LINGO.

Challenge files

Finding the logic

The frustrating part was combing through forum discussions older than myself hoping to find some specifications. We were lucky enough to stumble across a LINGO decompiler but it only worked for .dir files.

Hunt was on for a .dcr to .dir converter, and this wee project on GitHub had a tool called DCR2DIR. With that, the flag checking logic was decompiled.

on check_flag(flag)
  if flag.length <> 42 then
    return(0)
  end if
  checksum = 0
  i = 1
  repeat while i <= 21
    checksum = bitXor(checksum, zz(charToNum(flag.getProp(#char, i * 2 - 1)) * 256 + charToNum(flag.getProp(#char, i * 2))))
    i = 1 + i
  end repeat
  if checksum <> 5803878 then
    return(0)
  end if
  check_data = [[2, 5, 12, 19, 3749774], [2, 9, 12, 17, 694990], [1, 3, 4, 13, 5764], [5, 7, 11, 12, 299886], [4, 5, 13, 14, 5713094], [0, 6, 8, 14, 430088], [7, 9, 10, 17, 3676754], [0, 11, 16, 17, 7288576], [5, 9, 10, 12, 5569582], [7, 12, 14, 20, 7883270], [0, 2, 6, 18, 5277110], [3, 8, 12, 14, 437608], [4, 7, 12, 16, 3184334], [3, 12, 13, 20, 2821934], [3, 5, 14, 16, 5306888], [4, 13, 16, 18, 5634450], [11, 14, 17, 18, 6221894], [1, 4, 9, 18, 5290664], [2, 9, 13, 15, 6404568], [2, 5, 9, 12, 3390622]]
  repeat while check_data <= 1
    x = getAt(1, count(check_data))
    i = x.getAt(1)
    j = x.getAt(2)
    k = x.getAt(3)
    l = x.getAt(4)
    target = x.getAt(5)
    sum = zz(charToNum(flag.getProp(#char, i * 2 + 1)) * 256 + charToNum(flag.getProp(#char, i * 2 + 2)))
    sum = bitXor(sum, zz(charToNum(flag.getProp(#char, j * 2 + 1)) * 256 + charToNum(flag.getProp(#char, j * 2 + 2))))
    sum = bitXor(sum, zz(charToNum(flag.getProp(#char, k * 2 + 1)) * 256 + charToNum(flag.getProp(#char, k * 2 + 2))))
    sum = bitXor(sum, zz(charToNum(flag.getProp(#char, l * 2 + 1)) * 256 + charToNum(flag.getProp(#char, l * 2 + 2))))
    if sum <> target then
      return(0)
    end if
  end repeat
  return(1)
  exit
end

The checker makes use of a recursive function zz.

on zz(x)
  return(zz_helper(1, 1, x).getAt(1))
  exit
end

on zz_helper(x,y,z)
  if y > z then
    return([1, z - x])
  end if
  c = zz_helper(y, x + y, z)
  a = c.getAt(1)
  b = c.getAt(2)
  if b >= x then
    return([2 * a + 1, b - x])
  else
    return([2 * a + 0, b])
  end if
  exit
end

We figured out some specifics with a language guide and rewrote the logic in python.

Solving

At this point, it was around 6 in the morning and I wasn’t functioning well. The zz function is pretty complicated for a SMT solver, so some tweaking would be needed. Our approach solves for the zz output values in the first step. It then takes those values and does a reverse look up.

solve1.py

rom z3 import *

zz_arr = [z3.BitVec('flag_%d' % i, 32) for i in range(21)] #21 zz(x) values, where x correspodns to those shitty number experssion

def zz(x):
    return zz_helper(1, 1, x)[0]

def zz_helper(x, y, z):
    if y > z:
        return (1, z - x)
    c = zz_helper(y, x + y, z)
    a = c[0]
    b = c[1]
    if b >= x:
        return (2 * a + 1, b - x)
    else:
        return (2 * a + 0, b)

# Create a look up table
zz_table = [zz(i) for i in range(0x10000)]

def check_flag(flag):
    checksum = 0
    for i in flag:
        checksum = checksum ^ i
    solver.add(checksum == 5803878)

    check_data = [[2, 5, 12, 19, 3749774],
                  [2, 9, 12, 17, 694990],
                  [1, 3, 4, 13, 5764],
                  [5, 7, 11, 12, 299886],
                  [4, 5, 13, 14, 5713094],
                  [0, 6, 8, 14, 430088],
                  [7, 9, 10, 17, 3676754],
                  [0, 11, 16, 17, 7288576],
                  [5, 9, 10, 12, 5569582],
                  [7, 12, 14, 20, 7883270],
                  [0, 2, 6, 18, 5277110],
                  [3, 8, 12, 14, 437608],
                  [4, 7, 12, 16, 3184334],
                  [3, 12, 13, 20, 2821934],
                  [3, 5, 14, 16, 5306888],
                  [4, 13, 16, 18, 5634450],
                  [11, 14, 17, 18, 6221894],
                  [1, 4, 9, 18, 5290664],
                  [2, 9, 13, 15, 6404568],
                  [2, 5, 9, 12, 3390622]]

    for i, j, k, l, target in check_data:
        solver.add(flag[i] ^ flag[j] ^ flag[k] ^ flag[l] == target)

solver = z3.Solver()
check_flag(zz_arr)

c = solver.check()
flag_zzs = []
if c == z3.sat:
    model = solver.model()
    for c in zz_arr:
      flag_zz = zz_table.index(model.eval(c))
      flag_zzs.append(flag_zz)
      print(flag_zzs)
else:
    print('Unsatisfiable')

solve1.py gave a list of 21 integers that can be used to solve stage 2.

solve2.py

import z3
zzs = [20547,21574,31559,29236,28776,12611,21343,17459,21353,18286,24393,29535,29778,21868,22879,19833,24400,24947, 13673, 28494, 8573]

password_len = 42
flag_chars = [z3.Int('flag_%d' % i) for i in range(password_len)]
solver = z3.Solver()

for c in flag_chars:
    solver.add(c >= 0x20)
    solver.add(c < 0x7f)

for i, zz in enumerate(zzs):
    solver.add(flag_chars[i*2] * 256 + flag_chars[i*2+1] == zz)

c = solver.check()
print(c)
if c == z3.sat:
    print('SAT')
    sol = ''
    m = solver.model()
    for c in flag_chars:
        sol += chr(m[c].as_long())
    print(sol)

Running the script gave us the flag: PCTF{Gr4ph1CS_D3SiGn_Is_tRUlY_My_Pas5ioN!}.


In hindsight, my main issue was with implementing a look up table in z3. This could be better done with a Function. Here’s a better script, probably.

solve.py

import z3
import itertools

def zz(x):
    return zz_helper(1, 1, x)[0]

def zz_helper(x, y, z):
    if y > z:
        return [1, z - x]
    c = zz_helper(y, x + y, z)
    a = c[0]
    b = c[1]
    if b >= x:
        return [2 * a + 1, b - x]
    else:
        return [2 * a + 0, b]

def check_flag(flag):

    # Flag length 42
    checksum = z3.BitVecVal(0, 32)
    for i in range(1, 22):
        c1 = flag[i * 2 - 2]
        c2 = flag[i * 2 - 1]
        checksum ^= zz_func(c1, c2)

    solver.add(checksum == 5803878)

    check_data = [[2, 5, 12, 19, 3749774],
                  [2, 9, 12, 17, 694990],
                  [1, 3, 4, 13, 5764],
                  [5, 7, 11, 12, 299886],
                  [4, 5, 13, 14, 5713094],
                  [0, 6, 8, 14, 430088],
                  [7, 9, 10, 17, 3676754],
                  [0, 11, 16, 17, 7288576],
                  [5, 9, 10, 12, 5569582],
                  [7, 12, 14, 20, 7883270],
                  [0, 2, 6, 18, 5277110],
                  [3, 8, 12, 14, 437608],
                  [4, 7, 12, 16, 3184334],
                  [3, 12, 13, 20, 2821934],
                  [3, 5, 14, 16, 5306888],
                  [4, 13, 16, 18, 5634450],
                  [11, 14, 17, 18, 6221894],
                  [1, 4, 9, 18, 5290664],
                  [2, 9, 13, 15, 6404568],
                  [2, 5, 9, 12, 3390622]]

    for i, j, k, l, target in check_data:
        s = zz_func(flag[i * 2], flag[i * 2 + 1])
        s ^= zz_func(flag[j * 2], flag[j * 2 + 1])
        s ^= zz_func(flag[k * 2], flag[k * 2 + 1])
        s ^= zz_func(flag[l * 2], flag[l * 2 + 1])
        solver.add(s == target)

password_len = 42

flag_chars = [z3.BitVec(f'flag_{i}', 8) for i in range(password_len)]
flag = z3.Concat(*flag_chars)
solver = z3.Solver()

# Generate the table
zz_func = z3.Function('zz_func', z3.BitVecSort(8), z3.BitVecSort(8), z3.BitVecSort(32))
for a, b in itertools.product(range(256), range(256)):
    solver.add(zz_func(a, b) == zz(a*256+b))

print('Done putting the massive table into z3')

# Add the flag constraints
check_flag(flag_chars)
print('Done adding constraints')
c = solver.check()

# Dump results if found
print(c)
if c == z3.sat:
    m = solver.model()
    print(m.eval(flag).as_long().to_bytes(password_len, 'big'))