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.
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.
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'))
