Solve scripts for DUCTF 2023 Wrong Signal. Writeup: https://trebledj.github.io/posts/ductf-2023-wrong-signal/

solve.py

# DownUnderCTF 2023 – Wrong Signal
# Solve Script by TrebledJ
# WriteUp: https://trebledj.github.io/posts/ductf-2023-wrong-signal/

import z3


# Func to extract crumbs from bytes.
crumbs = lambda bs: [(b >> (2 * i)) & 0b11 for b in bs for i in range(4)]

def to_byte(cs):
    """Convert symbolic crumb to byte."""
    # Note: crumbs are accessed in reverse, so remember to reverse the reverse in this reverse.
    # Also remember to ZeroExt(end) our bitvecs, so that they are 8 bits long.
    [c0, c1, c2, c3] = map(lambda c: z3.ZeroExt(6, c), cs)
    return (c3 << 6) | (c2 << 4) | (c1 << 2) | c0

# Func to convert crumb to address offset.
func = lambda sym: z3.If(sym == 0, -0x15000, z3.If(sym == 1, -0x1000, z3.If(sym == 2, 0x1000, 0x15000)))


# Static bytes extracted from the binary.
mangle_buf = b'\xc2\xea\x96\xb6\x0c\x9c\x92\xe5\x72\xff\xe9\x3d\x11\x54\xc1\x9f'
mangle_crumbs = crumbs(mangle_buf)

# Inaccessible regions. Avoid putting our pointer in these areas.
# These regions can be obtained from GEF vmmap.
blacklist_regions = [
    (0x1338b000, 0x1338c000), (0x13399000, 0x1339f000), (0x133a0000, 0x133a8000), (0x133a9000, 0x133b0000),
    (0x133b9000, 0x133ba000), (0x133c3000, 0x133cd000), (0x133ce000, 0x133d2000), (0x133d3000, 0x133da000),
    (0x133e4000, 0x133e5000), (0x133ed000, 0x133f5000), (0x133f6000, 0x13400000), (0x13401000, 0x13404000),
    (0x1340c000, 0x1340d000), (0x13413000, 0x13414000), (0x13417000, 0x13419000), (0x1341a000, 0x13423000),
    (0x13424000, 0x13427000), (0x13428000, 0x1342b000), (0x1342c000, 0x1342e000), (0x1343b000, 0x1343c000),
]

# Construct symbols for input.
inp = [z3.BitVec(f'inp_{i}', 2) for i in range(64)]

# Construct a mangled version of the symbols.
inpm = [sym ^ m for sym, m in zip(inp, mangle_crumbs)]

# Obtain a byte representation of every 4 crumbs.
inp_bytes = [to_byte(inp[4*i:4*(i+1)]) for i in range(len(inp)//4)]

# Throw everything at the solver.
s = z3.Solver()

# -- Printable ASCII constraints. --
for b in inp_bytes:
    s.add(0x20 <= b, b <= 0x7F)

# -- Target address constraint. --
offsets = [func(sym) for sym in inpm]
s.add(z3.Sum(offsets) == 0x12000)

# -- Readable regions constraint. --
# Compute intermediate accumulations.
accs = [offsets[0]]
for sym in offsets[1:]:
    accs += [accs[-1] + sym]

# Accumulations should NEVER appear in a blacklisted region.
# Otherwise, we would get a SIGSEGV due to failed read.
for a in accs:
    s.add(0x13386000 <= a, a <= 0x13441000)
    for start, end in blacklist_regions:
        s.add(z3.Not(z3.And(start <= 0x13386000 + a, 0x13386000 + a < end)))

assert s.check() == z3.sat

# Construct flag.
m = s.model()

out = ''.join(chr(m.eval(b).as_long()) for b in inp_bytes)
print(out)
assert out == 'hElCYi8OxUF7PAA5'