Solve script for the DUCTF 2022 ezpz-rev reverse engineering challenge. Writeup: https://trebledj.github.io/posts/ductf-2022-ezpz-rev/

ezpz-rev-solve.py

import z3

# Initialisation procedure.
encoded = '5a4b3c2d5a4b4c1d2a1e3a3b4c1d2a1e1f2a3b3c1g1d3e5f1b2c2g1d1f2e4f6g1d7f3h3g1d4f6h3g1d2f1i4j1h2k2l1m1d3i2j5k2l2m2i3j4k3l2m2i3j4k3l2m1i5j2k2n2l2m1i4j5n4l'
chars = ''
for i in range(len(encoded) // 2):
    skip, char = encoded[2*i:2*i+2]
    chars += int(skip) * char

assert len(chars) == 0xc4

# print('\n'.join(''.join(chars[size*i:size*(i+1)]) for i in range(size)))

# Create a bunch of symbols.
inputs = [z3.Int(f'g_{i}') for i in range(196)]

# Create a constraint solver object.
s = z3.Solver()

size = 14

# Constrain possible input. We just care about the 1s, really.
for sym in inputs:
    s.add(z3.Or(sym == 0, sym == 1))

# Constraint 1: row-wise constraint.
for i in range(size):
    s.add(z3.Sum(inputs[size*i:size*(i+1)]) == 3)
    
# Constraint 2: col-wise constraint.
for i in range(size):
    s.add(z3.Sum(inputs[i::size]) == 3)

# Constraint 3: mask constraint.
letters = 'abcdefghijklmn'
for l in letters:
    # Find all indices in chars which have letter `l`, then sum the corresponding Int symbols from `inputs`.
    indices = [i for i, c in enumerate(chars) if c == l]
    s.add(z3.Sum([inputs[i] for i in indices]) == 3)

# Constraint 4: check orthodiagonal adjacents.
for index, sym in enumerate(inputs):
    x = index % size
    y = index // size

    # Build list of adjacent indices. Bounds checking mania.
    orthodiag = []
    if y > 0:
        orthodiag += [-14]
        if x > 0:
            orthodiag += [-15]
        if x < size - 1:
            orthodiag += [-13]
    if y < size - 1:
        orthodiag += [14]
        if x > 0:
            orthodiag += [13]
        if x < size - 1:
            orthodiag += [15]
    if x > 0:
        orthodiag += [-1]
    if x < size - 1:
        orthodiag += [1]
    
    # If this cell is 1 --> surrounding cells can't be one.
    for od in orthodiag:
        s.add(z3.Implies(sym == 1, inputs[index + od] != 1))

assert s.check() == z3.sat

# Construct payload.
payload = ''
m = s.model()
for sym in inputs:
    payload += str(m.eval(sym).as_long())

print(payload)
# 0101000000001000000101010000101000000001000000000101000110100000000100000010101000000100000000100100001010100000001000000010101000101000000000000000101010010101000000000000000001010100010101000000