Squish
Category: rev
Description:
oops! i squished my flag.
This looks like a classic binary reversing challenge. Upon running the binary, we are greeted with a prompt that asks for something to squish, then spitting out an out.bmp file.
The output file attached in the challenge description shows a 2 x 124 (very long) image filled with seemingly random monochrome pixels, which very likely implies that the pixel values themselves hold some form of data.
Quickly running through the pixels it seems that the RGB values are the same for each pixel, meaning that each pixel represents 1 byte, i.e. we can treat the squished flag output as a 2 x 124 byte array:
ca ff ff ca fc c1 f6 c9 ea c3 fa b6 e8 f2 d9 e2 c4 f9 ad ff a7 e4 bd e9 ff ff ff da ff ff ff bf ff ac e8 cc ec d2 d1 cd d0 ff ff ff da ff ff ff a7 c8 d3 b5 e8 bb ff ff ff 9d f7 bc dc dc dd d1 c0 ff ff ff a7 ff a3 e8 dd dd eb cd e0 c5 e1 b3 ff aa fe ba db ff ff d5 c4 ff ff eb aa ff ba ff bf ff ff ff ee cf cf c3 f4 b2 ff b6 f0 c8 de ff ff c8 a8 e1 d8 fe bc ff a4 f0 ef f3
e1 e3 ff e8 ff e8 fe ca ed e8 ff e8 ff ff db f2 d3 fe c7 ff c6 fe dd ec e0 e5 ff e9 f0 d5 ff e3 ff e5 ee f1 f7 e9 e9 e9 e5 f1 d3 ff e9 ff d5 f0 d5 e9 f9 e5 f7 dc f3 d2 fe db f8 d3 e6 e8 f3 e8 df ee d7 fe ca ff d5 ee da e6 ff e9 ec dc f1 e1 ff c6 fe d1 ef da ea e0 da ea db f6 ca ff e9 ff e3 fe dc e9 fc e6 f1 d7 fb c9 ff cb fa d8 ed de e7 e9 d4 f2 ce ff ca ff e0 f3 f3 f7To start off, let us decompile the binary! The bulk of the contents is contained within the main function, and I will be breaking it up into chunks:
__int64 __fastcall main(int a1, char **a2, char **a3)
{
int v3;
__int64 v4;
// ...
_BYTE v13[8];
// ...
char s[72];
unsigned __int64 v55;
v55 = __readfsqword(0x28u);
v14 = v13;
puts("what to squish?");
__isoc99_scanf("%64s", s);
v43 = 65; // height_maybe
v3 = strlen(s); // sz
v45 = 92; // width_maybeVery clearly, our input is stored in s. There is an interesting initialisation of 2 integers to 65 and 92, which might come in useful later.
A simple guess, especially with 2 moderately-sized numbers in an image spitter chal, could just be width and height. I’ll label them just that for now.
v44 = (92 - 50 * sz % 92) % 92 + 50 * sz; // sz_expanded
v47 = v44 - 1LL; // sz_expanded_pred
v4 = 3LL * v44; // triple_sz_expanded
v48 = height_maybe - 1LL;
v29 = v44; // sz_expanded_2
v30 = 0LL;
v27 = v44; // sz_expanded_3
v28 = 0LL;
v25 = height_maybe; // height_maybe_2
v26 = 0LL;
v5 = 16 * ((3 * height_maybe * (__int64)v44 + 15) / 0x10uLL);
while ( v13 != &v13[-(v5 & 0xFFFFFFFFFFFFF000LL)] )
;The first line just sets v44 to 50 * sz rounded up to the nearest multiple of 92. Note that with a quick scan of the rest of the decompilation, it seems that 50 and 23 (which is
v6 = alloca(v5 & 0xFFF);
if ( (v5 & 0xFFF) != 0 )
*(_QWORD *)&v13[(v5 & 0xFFF) - 8] = *(_QWORD *)&v13[(v5 & 0xFFF) - 8];
v49 = v13; // buf
for ( i = 0; i < height_maybe; ++i )
{
for ( j = 0; j < sz_expanded; ++j )
{
v49[3 * j + 2 + triple_sz_expanded * i] = -1;
v49[3 * j + 1 + triple_sz_expanded * i] = v49[3 * j + 2 + triple_sz_expanded * i];
v49[3 * j + triple_sz_expanded * i] = v49[3 * j + 1 + triple_sz_expanded * i];
}
}More cleanly in Python:
buf = v13
for i in range(height_maybe):
for j in range(sz_expanded):
for k in range(3):
buf[(i*sz_expanded + j)*3 + k] = -1Classic nested for appears! v49 (buf) is a height_maybe x sz_expanded x 3 array initialised with -1s. We can hence more or less confirm that height_maybe is our height and sz_expanded is our width. We will rename width_maybe to what in the meantime.
v53 = 'pmb.tuo' // filename
for ( k = 0; ; ++k )
{
v7 = k;
if ( v7 >= strlen(s) )
break;
v46 = s[k];
for ( m = 0; m <= 49; ++m )
{
for ( n = 0; n <= 49; ++n )
{
for ( ii = 0; ii <= 2; ++ii )
buf[150 * k + 3 * n + ii + triple_width * (57 - m)] = byte_4020[2500 * v46 + 50 * m + n];
}
}
}Again more cleanly in Python:
for idx, cur in enumerate(s):
for i in range(50):
for j in range(50):
for k in range(3):
buf[((57-i)*width + (idx*50+j))*3 + k] = KEY[(cur*50 + i)*50 + j]This is a slightly more complicated for loop. Firstly for the simpler RHS, KEY (originally byte_4020) is a 128 x 50 x 50 array, containing mostly 0xffs (white) with other values popping up once in a while. Note that k is not referenced at all.
Now for the LHS, recall buf is a height x width x 3 array, with width (renamed from sz_expanded) being 50 * sz rounded up against 92. Perhaps it is cleaner to rewrite to
import numpy as np
buf = np.full((65, round_up(50*len(s), 92), 3), -1)
KEY = np.random.rand(128, 50, 50)
for idx, cur in enumerate(s):
buf[57:7:-1, idx*50:(idx+1)*50] = KEY[cur, :, :, None]*np.ones((1, 1, 3))In which case the indexing looks like
Note the reverse order. This is probably done because .bmp files have y=0 at the bottom instead of the top.
v8 = (unsigned int)(height / 23); // height_new
v50 = width / 23 - 1LL; // width_new_pred
v23 = width / 23; // width_new
v24 = 0LL;
v9 = 3 * v23; // triple_width_new
v51 = (int)v8 - 1LL; // height_new_pred
v21 = v23; // width_new_2
v22 = 0LL;
v19 = (int)v8; // height_new_2
v20 = 0LL;
v17 = v23; // width_new_3
v18 = 0LL;
v15 = (int)v8; // height_new_3
v16 = 0LL;
v10 = 16 * ((3 * (int)v8 * v23 + 15) / 0x10uLL);
while ( v13 != &v13[-(v10 & 0xFFFFFFFFFFFFF000LL)] )
;Here we see that we are now working with a new set of variables, where this time the width and height are scaled down by a factor of 23. This is probably what the “squishing” means.
v11 = alloca(v10 & 0xFFF);
if ( (v10 & 0xFFF) != 0 )
*(_QWORD *)&v13[(v10 & 0xFFF) - 8] = *(_QWORD *)&v13[(v10 & 0xFFF) - 8];
v52 = v13; // arr
for ( jj = 0; jj < height / 23; ++jj )
{
for ( kk = 0; kk < width / 23; ++kk )
{
v34 = 0;
for ( mm = 0; mm <= 22; ++mm )
{
for ( nn = 0; nn <= 22; ++nn )
v34 += (unsigned __int8)buf[69 * kk + 3 * nn + triple_width * (23 * jj + mm)];
}
v34 = (int)v34 / 529;
for ( i1 = 0; i1 <= 2; ++i1 )
{
height_new = v34;
v52[3 * kk + i1 + triple_width_new * jj] = v34;
}
}
}Again more cleanly in Python:
for i in range(height_new):
for j in range(width_new):
tmp = 0
for y in range(23):
for x in range(23):
tmp += buf[((i*23+y)*width + (j*23+x))*3 + 0]
res = tmp//(23**2)
for k in range(3):
arr[(i*width + j)*3 + k] = resWe can honestly just ignore the rgb portion because it’s quite redundant.
import numpy as np
arr = np.zeros((height_new, width_new))
for i in range(height_new):
for j in range(width_new):
arr[i, j] = buf[i*23:(i+1)*23, j*23:(j+1)*23, 0].sum()//(23**2)What this does is that the program simply looks at 23 x 23 chunks from buf and takes the average to be inserted into the corresponding pixel in the output image.
Note that while the width of buf is a multiple of 23 (due to the adjusting from sz_expanded), the height of buf is fixed at 65, which means that the output image will always have a height of 65 // 23 = 2.
sub_12F5(arr, (unsigned int)(height / 23), (unsigned int)(width / 23), &filename, height_new, triple_width_new)
puts("ok it squished");
return 0LL;
}A quick look at the function tells us that this simply creates the required out.bmp image with arr as the pixel data, confirming our guess.
To summarise, the squishing process looks like this:
In words, for each character in the flag, the program looks up the corresponding 50 x 50 byte chunk and loads it into buf (which is initialised with all 0xff). Then the program squishes buf by taking 23 x 23 chunk averages, which gives us our output arr.
To reverse this, notice that for each character (represented as the 50 x 50 large chunk), there will always be at least 2 (top and bottom) output pixels that are fully determined by it. Note that it is possible for 2 different characters to produce the same 2 values, but either
- The checking can be fortified by looking at the data from the previous (already determined) chunk / character, or
- We should still be able to guess the flag if there are very limited clashes
(For simplicity sake, I chose method 2.)
import numpy as np
WIDTH = 124
HEIGHT = 2
DEPTH = 3
with open('out.bmp', 'rb') as f:
out = list(f.read()[-WIDTH*HEIGHT*DEPTH::3])
# top and bottom bytes
top, bottom = out[124:], out[:124]
# retrieve key from binary
START = 0x3020
with open('./squish', 'rb') as f:
KEY = np.array(list(f.read()[START:START+128*50*50])).reshape((128, 50, 50))
def search(cur):
# supposed bounds of the 2 23x23 chunks within key
# that correspond to the top and bottom pixels after squishing
y1 = 57-45
y2 = 57-22
x1 = (cur*23)%50
x2 = ((cur+1)*23)%50
# test all ascii printable bytes and see
# which ones produce the desired squished values
res = bytes(
i
for i in range(32, 127)
if (
KEY[i, y1:y2, x1:x2].sum()//(23**2) == top[cur]
and (KEY[i, y2:, x1:x2].sum()+255*8*23)//(23**2) == bottom[cur]
)
)
# if there are multiple possible characters,
# we display them first and at the end
# see (manually) which flag makes the most sense.
return res if len(res) == 1 else b'[' + res + b']'
idx = 0
flag = b''
while True:
# search for the index of the 23x23
# that lies completely within our current 50x50
cur = (idx*50+23-1)//23
try:
flag += search(cur)
except IndexError:
break
idx += 1
print(flag.decode())With this, the output is
LI[7T]CT[FH]{oops_i_th1nk_i_m[4Y]y_have_squ1sh3d_a_b1t_t0oo[do]_much[]Which we can pretty easily figure out that the supposed flag should be
LITCTF{oops_i_th1nk_i_m4y_have_squ1sh3d_a_b1t_t0ooo_much}ilovepython
Category: rev
Description:
I love Python. In fact, I just spent the last 2d11h36m comprehensively understanding Python’s typing module!
…Say, could you help me finish one line of my code?
When we open the ilovepython.py file, we are greeted with a monster. If we follow the description and the helpful comment at the top we arrive at the “instructions” to get the flag:
# I don't know what type to give var. Thanks! (Please no "object" or "Any"... I want a specific type)
var = _Q0[z[_[z[_[N[_[N[_[J[_[O[_[N[_[V[_[E[_[G[_[Z[_[U[_[Z[_[U[_[U[_[Y[_[C[_[I[_[S[_[T[_[Y[_[G[_[W[_[B[_[G[_[U[_[U[_[Z[_[H[_[W[_[Q[_[V[_[V[_[K[_[M[_[G[_[U[_[W[_[D[_[_L[_[_E]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]()
# just some validation
var = _V[_E]()This challenge makes use of python type hinting, which seems really complicated especially when we face tons of classes, inheritance and nesting. I was initially quite lost and didn’t put too much effort into making sense of the challenge until subsequent hints were released (because it was too hard and still had 0 solves like 2 days into the CTF):
I lied. I didn’t comprehensively understand Python’s typing module. I just figured out what covariance and contravariance really mean for a type checker. Oh, and subtyping too.
Honestly, the hint was kind of cryptic to me at first. It was only after the second hint dropped that I started to pick up on how this challenge works.
from typing import TypeVar, Generic, Never
_Z = TypeVar("_Z")
_P = TypeVar("_P", covariant=True)
_N = TypeVar("_N", contravariant=True)
class _E: ...
class _L(Generic[_N]): ...
class H(Generic[_N]): ...
class I(Generic[_N]): ...
class _(Generic[_N]): ...
class _V(Generic[_Z], _L[_[_Z]], H[_["_V[_Z]"]], I[_["_V[_Z]"]]): ...
var: H[_[I[_[_L[_[_E]]]]]] = _V[_E]()
'''
H[_[I[_[_L[_[_E]]]]]] >= _V[_E]
H[_[I[_[_L[_[_E]]]]]] >= H[_[_V[_E]]] by Inheritance _V[_Z] -> H[_[_V[_Z]]]
_[_V[_E]] >= _[I[_[_L[_[_E]]]]] by Contravariant Unfolding H[_N]
I[_[_L[_[_E]]]] >= _V[_E] by Contravariant Unfolding _[_N]
I[_[_L[_[_E]]]] >= I[_[_V[_E]]] by Inheritance _V[_Z] -> I[_[_V[_Z]]]
_[_V[_E]] >= _[_L[_[_E]]] by Contravariant Unfolding I[_N]
_L[_[_E]] >= _V[_E] by Contravariant Unfolding _[_N]
_L[_[_E]] >= _L[_[_E]] by Inheritance _V[_Z] -> _L[_[_Z]]
_[_E] >= _[_E] by Contravariant Unfolding _L[_N]
_E >= _E by Contravariant Unfolding _[_N]
True by Reflexivity
'''From the original challenge file, we know that our target var also has a similar assignment to _V[_E](), which clearly shows that the type of var should follow a similar format as what is shown in the example hint. In fact, we can actually derive this ourselves, which I will do later!
But first, let us process and understand the hint and how it helps us to solve the challenge:
Suppose var has type T1[T2[T3[T4[T5[...]]]]]. Some notation tweaks for brevity:
- Brackets are omitted:
T1 T2 T3 T4 T5 ... - Spaces are omitted, and types with more than 1 character are surrounded with parentheses:
(T1)(T2)(T3)(T4)(T5)...<- might seem counterintuitive here but will come in handy later
When we instantiate var, in order to not produce an error, the type of the new object must be a subtype of var, or type(var) >= type(whatever()). How does python check if it is valid if the type is a nested mess? Well, we can perform simplification, where there are essentially only 2 main rules:
A[T] >= B[U] <=> A[T] >= A[C[U]], or rewrittenAT >= BU <=> AT >= ACU, whereBUinherits fromACU. Note 4 pointers:- The direction of the
>=, where it is the subtype that “changes” - If
Bdoes not inherit from any form ofA, there’s something wrong with our type :D - Generic typing: In general for this challenge
BUinherits fromACUfor allU, which means when solving we can simply swap outBforAC. - The end result is that the outermost type matches, allowing us to undergo subsequent redution (below).
- The direction of the
AT >= AU <=> T <= / >= Udepending on whetherAhas a covariant (same direction) or contravariant (flip) type parameter. This is our main reduction step.
Note: If you are somewhat lost / need more examples, please visit the appendix at the bottom
In a way, we can look at this as a program with 2 stacks, where the outermost type on the subtype side is our opcode, that on the supertype side is the operand, and the result is pushed onto the subtype stack (opcode and operand are used up since rule 2 almost always succeeds rule 1). We’ll come back to this later.
For now, let’s take a look at this in action, using the validation code var = _V[_E](). _V, with type (V), inherits 2 kinds of classes:
(V) -> x_(V), wherexis any uppercase letter; this allows for some sort of factory (shown in example below)(V) -> (L)_, this essentially acts as the end of the factory
(T1)(T2)(T3)(T4)(T5) >= (V)(E)
A(T2)(T3)(T4)(T5) >= A_(V)(E) ; [rule 1] let (T1) = A
(T2)(T3)(T4)(T5) <= _(V)(E) ; [rule 2] A is contravariant
(T3)(T4)(T5) >= (V)(E) ; [rule 2] (T2) is _, _ is contravariant
(L)(T4)(T5) >= (L)_(E) ; [rule 1] let (T3) = (L)
(T4)(T5) <= _(E) ; [rule 2] (L) is contravariant
(T5) >= (E) ; [rule 2] (T4) is _, _ is contravariant
T ; (T5) is (E)I will not go into detail as to why (T2) and (T4) has to be _, but at this point you can probably see that the validation portion simply requires the type of var to be ([A-z]_)*\(L\)_\(E\) (yes this is regex).
With this knowledge, we can start working the “program” out to figure out how our type gets parsed and checked. I initially started off parsing manually, but here I will use the script I made towards the end of solving.
# see parse.py for full listing
INSTRUCTIONS = {
'_': {
# how this works is:
# suppose we encounter (X) >= _...
# our only logical step forward is to apply rule 1,
# which converts _ to (X)<something>,
# based on what it inherits from.
# over here the inheritance is represented with a nested dict
# such that INSTRUCTIONS['_']['(X)'] gives us the remainder of the inheritance,
# which in this case is (X)a_(L) ---[rule 2]---> a_(L).
'(X)': ['a', '_', '(L)'],
'(Ra0)': ['(Q0)', 'a', '_'],
'(Rab)': ['(Qb)', 'a', '_'],
'(Rad)': ['(Qd)', 'a', '_'],
...
},
...
}
# contravariant and covariant types
CONTRA = {'(X)', '(L)', 'A', 'B', ..., 'z', '_'}
CO = {'(Ra0)', '(Rab)', '(Rad)', '(Rbb)', ..., '(Rzc)'}
# the 2 sides of the subtype equation can be represented with 2 "stacks"
# (front of the "string" is at the end of the list representation)
# since we don't know the flag yet, let us insert a dummy one
s0 = (list('_'.join('LITCTFABCDEFGHIJKLMNOPQRSTUVWXYZABCDE')) + ['_', '(L)', '_', '(E)'])[::-1]
# type of the class provided converted into the second stack below
s1 = (['(Q0)', 'z', '_', 'z', '_', 'N', '_', 'N', '_', 'J', '_', ..., 'D', '_', '(L)', '_', '(E)'])[::-1]
s = [s0, s1]
# function for stepping through the equations.
# op and param are the outermost type on the subtype and supertype sides respectively
def step(op, param):
# over here we are applying rule 2 directly after rule 1.
# the "control" (direction of subtyping) of the stacks for tne next step
# depends on whether param is covariant or contravariant.
assert param in CONTRA or param in CO, f'{param} is invalid'
return (
# if op == param, apply rule 2 directly;
# else apply rule 1 then rule 2
# see the dict at the top of the script to understand the process.
None if op == param else INSTRUCTIONS[op][param][::-1],
param in CONTRA
)
def prettify(stack):
return ''.join(reversed(stack))
ib = 1 # which stack has "control" (contains the opcode)
prev_print = ''
with open('output.txt', 'w') as f:
while True:
prev_print = f'{prettify(s[0])} {">" if ib else "<"}= {prettify(s[1])}\n'
# get our next op and param and step through
res, change = step(s[ib].pop(), s[1-ib].pop())
if res != None:
# "skip steps" by combining all consecutive applications of rule 2
f.write(prev_print)
# append the inherited remainder to the stack with control
s[ib] += res
if change:
ib = 1-ibRunning the script, we get KeyError: 'Z' (which is somewhat expected given we don’t have the correct flag).
We shall now analyse the program by looking at the output:
L_I_T_C_T_F_A_B_C_D_E_..._E_(L)_(E) >= (Q0)z_z_N_N_J_O_N_V_E_...D_(L)_(E)
I_T_C_T_F_A_B_C_D_E_..._E_(L)_(E) >= (Q2)L_z_z_N_N_J_O_N_V_E_...D_(L)_(E)
T_C_T_F_A_B_C_D_E_..._E_(L)_(E) >= (Q2)O_L_z_z_N_N_J_O_N_V_E_...D_(L)_(E)The program starts off relatively straightforward (to understand). If we look at the instructions of opcode (Q[0123]):
INSTRUCTIONS = {
...,
'(Q0)': {
'(L)': ['(X)', '(Q0)'],
'A': ['_', '(Q3)', 'A', '_'], # substitute A with A, then jump to (Q3)
'B': ['_', '(Q1)', 'B', '_'], # substitute B with B, then jump to (Q1)
'C': ['_', '(Q2)', 'C', '_'],
'D': ['_', '(Q3)', 'D', '_'],
...,
'Y': ['_', '(Q3)', 'Y', '_'],
'Z': ['_', '(Q1)', 'Z', '_'],
'a': ['(Ra0)'],
'z': ['_', '(Qa)', 'z', '_']
},
...,
'(Q3)': {
'(L)': ['(X)', '(Q3)'],
'A': ['_', '(Q1)', 'Z', '_'], # substitute A with Z, then jump to (Q1)
'B': ['_', '(Q2)', 'X', '_'], # substitute B with X, then jump to (Q2)
'C': ['_', '(Q3)', 'P', '_'],
'D': ['_', '(Q3)', 'M', '_'],
...,
'Y': ['_', '(Q1)', 'Q', '_'],
'Z': ['_', '(Q3)', 'V', '_'],
'a': ['(Ra0)'],
'z': ['_', '(Qa)', 'z', '_']
},
...
}We can see that their main functionality is simply
MACHINE = list(map(
lambda x: list(zip(x[0], map(int, x[1]))),
[( # Q0
'ABCDEFGHIJKLMNOPQRSTUVWXYZ',
'31231231231231231231231231'
), ( # Q1
'QWERTYUIOPASDFGHJKLZXCVBNM',
'11121322233332313121223113'
), ( # Q2
'PYFGCRLAOEUIDHTNSQJKXBMWVZ',
'33232223212231113131213131'
), ( # Q3
'ZXPMCHRTNSDGKJBWFLAEIOUYQV',
'12332121133313112231222313'
)]
))
def run(inp):
# process always starts off with Q0
cur = 0
res = ''
for x in inp:
# Qn(uppercase_letter) is essentially substitution
new, cur = MACHINE[cur][ord(x)-ord('A')]
res += new
# flipped due to the stack's FILO arrangement
return res[::-1]Which we can very easily reverse with
def rev_run(inp):
# we know that the process always starts off with Q0
cur = 0
res = ''
# again FILO
# the first letter processed is all the way at the end of inp
# but we want to read from first to last letter processed
for x in inp[::-1]:
# we know the output of the substitution and the specific Qn
# which allows us to determine what exactly went into it
# as well as to recover the next Qn for the subsequent letter
new, cur = next(
(i, j)
for i, (y, j) in enumerate(MACHINE[cur])
if y == x
)
res += chr(ord('A')+new)
return resScrolling down the nice zigzag pattern in the output file, we soon realise that the program goes on from z_z_ all the way to z_a_, processing the string twice each, for a total of
(Qa)z_T_Z_R_Z_U_D_...O_a_(L)(E) <= a_N_N_J_O_N_V_...D_(L)_(E)
(Qc)z_z_T_Z_R_Z_U_D_...O_a_(L)(E) <= N_N_J_O_N_V_...D_(L)_(E)
(RzN)z_z_T_Z_R_Z_U_D_...O_a_(L)(E) >= _N_J_O_N_V_...D_(L)_(E)
z_z_T_Z_R_Z_U_D_...O_a_(L)(E) >= (QN)z_N_J_O_N_V_...D_(L)_(E)
z_T_Z_R_Z_U_D_...O_a_(L)(E) >= (QO)z_z_N_J_O_N_V_...D_(L)_(E)
T_Z_R_Z_U_D_...O_a_(L)(E) >= (QT)z_z_z_N_J_O_N_V_...D_(L)_(E)
_Z_R_Z_U_D_...O_a_(L)(E) <= (Rzc)z_z_z_N_J_O_N_V_...D_(L)_(E)The instructions go Qa -> Qc -> _ -> QN -> QO -> QT -> _. Looking at the instructions of above (Q[NOT]):
INSTRUCTIONS = {
...,
'(QN)': {'(L)': ['(X)', '(QN)'], 'N': ['(Rzc)'], 'z': ['_', '(QO)', 'z', '_']},
'(QO)': {'(L)': ['(X)', '(QO)'], 'O': ['(Rzc)'], 'z': ['_', '(QT)', 'z', '_']},
...,
'(QS)': {'(L)': ['(X)', '(QS)'], 'S': ['(Rzc)'], 'z': ['_', '(QN)', 'z', '_']},
'(QT)': {'(L)': ['(X)', '(QT)'], 'T': ['(Rzc)'], 'z': ['_', '(QS)', 'z', '_']},
...
}Ignoring the (L) operand, we see that they essentially do 2 things:
- When the operand is
z(followed by_), they get “moved over” to the other stack (see above output), modifying the current target letter in the process - Once the
z_’s are all shifted over, the program checks the immediate letter operand against the final target letter
In code:
# for the first case we have check('N', 'T')
def check(initial_sample, input_letter):
target = initial_sample
for _ in range(rounds): # number of rounds not known yet
target = shift(target) # N -> O -> T -> S -> N ...
return input_letter == targetSince the checking occurs at the end, we can very easily bypass this by tweaking our step function:
from string import ascii_uppercase as UPPER ### inserted code
def step(op, param):
assert param in CONTRA or param in CO, f'{param} is invalid'
if op.startswith('(Q') and op[2] in UPPER and param in UPPER: ###
print(op[2], end='') ###
return ['(Rzc)'], True ###
return (
None if op == param else INSTRUCTIONS[op][param][::-1],
param in CONTRA
)We get our “target” string, TNXOTVCGHUHUMYEIOTIGKBAUMZZWQVLKUGMWD (_ omitted here). And finally, by plugging this string back into the reverse of the first step:
flag = 'TNXOTVCGHUHUMYEIOTIGKBAUMZZWQVLKUGMWD'
for i in range(26*2):
flag = rev_run(flag)
print(flag) # LITCTFWUNLASTTHINGINSURTBRASEZOKAEBAIOr according to the flag content itself:
LITCTF{WUNLASTTHINGINSURTBRASEZOKAEBAI}Plugging in the flag without the program patch (and without flag braces) we get a pretty clean set of output along with an error saying (obj) is invalid. I’m pretty sure this just signifies the end of the program.
Thanks for reading! I feel that this challenge is really creative and rewarding once you start getting the hang of it. It is also surprising to see the likes of program emulation hidden inside something as innocent as Python type hints … Python is indeed pretty amazing after all :D
Appendix
If you are lost, don’t worry, I was too when I first interacted with the rules (tbh I still kinda am)! But you can gain a lot of intuition just by playing around. As a walkthrough, pretend you are the parser and you want to verify
L[_[I[_[T[_[C[_[_L[_[_E]]]]]]]]]] >= _Q0[z[_[z[_[N[_[N[_[_L[_[_E]]]]]]]]]]]or rewritten,
L_I_T_C_(L)_(E) >= (Q0)z_z_N_N_(L)_(E)is correct. Firstly we cannot deduce anything until we attempt to simplify it, and the best way to do that is to reduce the number of terms!
Applying rule 1, we look at the class declaration for (Q0) and search for one that starts with L:
class _Q0(Generic[_Z], _L[_X["_Q0[_Z]"]], A[_["_Q3[A[_[_Z]]]"]], B[_["_Q1[B[_[_Z]]]"]], C[_["_Q2[C[_[_Z]]]"]], D[_["_Q3[D[_[_Z]]]"]], E[_["_Q1[E[_[_Z]]]"]], F[_["_Q2[F[_[_Z]]]"]], G[_["_Q3[G[_[_Z]]]"]], H[_["_Q1[H[_[_Z]]]"]], I[_["_Q2[I[_[_Z]]]"]], J[_["_Q3[J[_[_Z]]]"]], K[_["_Q1[K[_[_Z]]]"]], L[_["_Q2[L[_[_Z]]]"]], M[_["_Q3[M[_[_Z]]]"]], N[_["_Q1[N[_[_Z]]]"]], O[_["_Q2[O[_[_Z]]]"]], P[_["_Q3[P[_[_Z]]]"]], Q[_["_Q1[Q[_[_Z]]]"]], R[_["_Q2[R[_[_Z]]]"]], S[_["_Q3[S[_[_Z]]]"]], T[_["_Q1[T[_[_Z]]]"]], U[_["_Q2[U[_[_Z]]]"]], V[_["_Q3[V[_[_Z]]]"]], W[_["_Q1[W[_[_Z]]]"]], X[_["_Q2[X[_[_Z]]]"]], Y[_["_Q3[Y[_[_Z]]]"]], Z[_["_Q1[Z[_[_Z]]]"]], a[_Ra0[_Z]], z[_["_Qa[z[_[_Z]]]"]]): ...(Note that the double quotes can be ignored)
We find one (there should only be one) instance, (Q0)(Z) -> L_(Q2)L_(Z) for generic (Z). Hence when we apply this back to our equation
L_I_T_C_(L)_(E) >= (Q0)z_z_N_N_(L)_(E)
L_I_T_C_(L)_(E) >= L_(Q2)L_z_z_N_N_(L)_(E)If you recall how it is formulated AT >= BU <=> AT >= ACU, in this case A is L, B is Q0, C is _(Q2)L_, and T and U is everything else.
Notice now that both sides start off with L_; by applying rule 2 twice we can simplify the terms
L_I_T_C_(L)_(E) >= L_(Q2)L_z_z_N_N_(L)_(E)
_I_T_C_(L)_(E) <= _(Q2)L_z_z_N_N_(L)_(E) ; contravariant
I_T_C_(L)_(E) >= (Q2)L_z_z_N_N_(L)_(E) ; contravariantand allow us to go back to rule 1 to repeat the whole process over and over until we reach the end.
I_T_C_(L)_(E) >= (Q2)L_z_z_N_N_(L)_(E)
I_T_C_(L)_(E) >= I_(Q2)O_L_z_z_N_N_(L)_(E) ; (Q2) -> I_(Q2)O_
_T_C_(L)_(E) <= _(Q2)O_L_z_z_N_N_(L)_(E) ; contravariant
T_C_(L)_(E) >= (Q2)O_L_z_z_N_N_(L)_(E) ; contravariant
...