Skip to content

Instantly share code, notes, and snippets.

@TrebledJ
Last active September 4, 2023 06:44
Show Gist options
  • Save TrebledJ/eff46dfd7f0cd5cc9ee4b2c2c3b174f6 to your computer and use it in GitHub Desktop.
Save TrebledJ/eff46dfd7f0cd5cc9ee4b2c2c3b174f6 to your computer and use it in GitHub Desktop.
Solve scripts for DUCTF 2023 Wrong Signal. Writeup: https://trebledj.github.io/posts/ductf-2023-wrong-signal/
# 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'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment