Captain Morgan - Rev

Points: 267 | Flag: BCCTF{Y00_hO_Ho_anD_4_B07Tl3_oF_rUm} | Solved by: Smothy @ 0xN1umb

what we got

Single python file chall.py - one absolute monster of a one-liner. Takes input, checks if it's the flag, prints "correct" or "incorrect".

the solve

Opening the file you get hit with this wall of obfuscated python. But breaking it down it's actually pretty straightforward:

1. Checks flag format BCCTF{...}
2. Converts the inner content to a big integer via int.from_bytes()
3. Extracts individual bits through a massive chain of walrus operators (:=) and right shifts (>>bhy) - 230 shifts total
4. Runs ~2000 boolean operations (&, |, ^) on those bits
5. Final variable bfu controls output: print("in"*bfu+"correct")

so basically its a boolean circuit that validates the flag bit by bit. bfu needs to be 0 for "correct"

threw z3 at it lol. the key insight was that you can just exec() the original walrus chains with a z3 BitVec instead of parsing them manually:

from z3 import *

code = open('chall.py').read()
stmts = code.split(';')

BW = 300
ari = BitVec('ari', BW)
bhy = 1  # correct prefix
aja = 1  # correct suffix

# exec everything except input() and print()
exec_code = '\n'.join(s.strip() for s in stmts[4:] if not s.strip().startswith('print('))
ns = {'ari': ari, 'bhy': bhy, 'aja': aja}
exec(exec_code, ns)

solver = Solver()
solver.add(ns['bfu'] == 0)
solver.add(ari > 0)
solver.add(ari < (1 << 250))

# printable ascii per byte
for i in range(32):
    b = (ari >> (i * 8)) & 0xFF
    solver.add(Or(b == 0, And(b >= 0x20, b <= 0x7e)))

solver.check()  # sat
m = solver.model()
val = m[ari].as_long()
flag_bytes = val.to_bytes((val.bit_length() + 7) // 8, 'big')
print(f"BCCTF{{{flag_bytes.decode()}}}")

first solve had an extra @ at the start from unconstrained high bits (the circuit only checks 231 bits but z3 was free to set bits above that). dropped it and got the real flag

flag

BCCTF{Y00_hO_Ho_anD_4_B07Tl3_oF_rUm}

yo ho ho and a bottle of rum indeed captain morgan 🏴‍☠️

smothy out ✌️