1157 words
6 minutes
CodeVinci CTF 2026 - 🤓 - Cryptography Writeup
Category: Cryptography
Flag: CodeVinci{I_hop3_y0u_d1dn7_sl0p_th1s_ch4lL_w1th_claude_uFf}
Challenge Description
just a nerdy chall
Analysis
The zip was tiny, so the first thing I did was confirm exactly what files were inside and whether this was source-first or artifact-first.
unzip -l nerdy.zipArchive: nerdy.zip Length Date Time Name--------- ---------- ----- ---- 0 2025-09-15 23:58 nerdy/ 5601 2025-09-15 22:37 nerdy/nerd.py 9364 2025-09-15 22:37 nerdy/server.py--------- ------- 14965 3 filesThat immediately told me this challenge was about understanding service logic, not brute forcing ciphertext blobs. I connected once to see the protocol surface and target identity exposed by the server.
timeout 8 nc nerd.codevinci.it 9984nerd service ready.Commands: diag <n> | issue <user_id> | validate <token> | help | quitTarget user: ctf>I then pulled out the key lines in nerd.py that control the whole game: how diagnostics are computed, how token material is derived, and how validation is decided.
from pathlib import Path
p = Path('/home/LIGHT/Downloads/nerdy_chal/nerdy/nerd.py')lines = p.read_text().splitlines()for i, l in enumerate(lines, 1): if any(k in l for k in [ 'def _derive', 'def diag_line', 'def validate', 'if token == self.target_token', 'y_prev = self.history[self.count - 2]' ]): print(f"{i}: {l}")96: def diag_line(self) -> tuple[int, int]:100: y_prev = self.history[self.count - 2]105: def _derive(self, user_id: str) -> Token:148: def validate(self, token_b64: str) -> tuple[bool, bool]:154: if token == self.target_token:The important part is that validate does not recompute token authenticity from scratch; it checks equality against the precomputed target token. At the same time, diag_line leaks correlated values of consecutive MT19937 outputs. The target token is generated once at startup (t=2000), and the first issue uses that same timeline slot, which leaks the same nonce source context. From there, the solve path is: recover tempered outputs from diag, untemper to MT state words, solve missing prefix words with Z3 while modeling in-place twist semantics correctly, reconstruct y1990..y1993 for the AES key, forge exact target token bytes, and submit with validate.
Getting the MT constraints right was the painful part; a naïve non-in-place twist model made Z3 go UNSAT repeatedly even with correct output reconstruction.
Once the in-place twist dependency was fixed in the solver, the exploit became clean and deterministic.
Running the final script gave the flag directly.
python solve_nerdy.pyCodeVinci{I_hop3_y0u_d1dn7_sl0p_th1s_ch4lL_w1th_claude_uFf}Solution
import base64import reimport socketfrom dataclasses import dataclass
from Crypto.Cipher import AESfrom z3 import BitVec, BitVecVal, If, LShR, Solver, sat
MASK32 = 0xFFFFFFFFPROMPT = b"\n> "
def u32(x: int) -> int: return x & MASK32
def rotl32(x: int, r: int) -> int: r &= 31 return u32((x << r) | (x >> (32 - r)))
def rotr32(x: int, r: int) -> int: r &= 31 return u32((x >> r) | (x << (32 - r)))
def pack_u32(x: int) -> bytes: return u32(x).to_bytes(4, "big")
def temper(x: int) -> int: y = u32(x) y ^= y >> 11 y ^= (y << 7) & 0x9D2C5680 y ^= (y << 15) & 0xEFC60000 y ^= y >> 18 return u32(y)
def undo_right_shift_xor(y: int, shift: int) -> int: x = 0 for i in range(31, -1, -1): yb = (y >> i) & 1 xb = yb j = i + shift if j <= 31: xb ^= (x >> j) & 1 x |= xb << i return u32(x)
def undo_left_shift_xor_and(y: int, shift: int, mask: int) -> int: x = 0 for i in range(32): yb = (y >> i) & 1 xb = yb j = i - shift if j >= 0 and ((mask >> i) & 1): xb ^= (x >> j) & 1 x |= xb << i return u32(x)
def untemper(y: int) -> int: x = undo_right_shift_xor(y, 18) x = undo_left_shift_xor_and(x, 15, 0xEFC60000) x = undo_left_shift_xor_and(x, 7, 0x9D2C5680) x = undo_right_shift_xor(x, 11) return u32(x)
def pkcs7_pad(data: bytes, block_size: int = 16) -> bytes: p = block_size - (len(data) % block_size) return data + bytes([p]) * p
@dataclassclass Tube: sock: socket.socket buf: bytes = b""
def recv_until(self, marker: bytes) -> bytes: while marker not in self.buf: chunk = self.sock.recv(65536) if not chunk: raise EOFError("connection closed") self.buf += chunk idx = self.buf.index(marker) + len(marker) out = self.buf[:idx] self.buf = self.buf[idx:] return out
def cmd(self, s: str) -> bytes: self.sock.sendall(s.encode() + b"\n") return self.recv_until(PROMPT)
def parse_diag_block(blob: bytes, n: int): text = blob.decode("utf-8", "replace") pairs = [] for ln in text.splitlines(): ln = ln.strip() if re.fullmatch(r"[0-9a-f]{8} [0-9a-f]{8}", ln): a, b = ln.split() pairs.append((int(a, 16), int(b, 16))) if len(pairs) < n: raise RuntimeError("diag parse failed") return pairs[:n]
def recover_outputs_from_diag(pairs): n = len(pairs) a = [p[0] for p in pairs] b = [p[1] for p in pairs] H = 0xFFF00000 L = 0x00000FFF
candidates = [] for mid in range(256): y1 = u32((b[0] & H) | (mid << 12) | (b[1] & L)) y0 = rotr32(y1 ^ a[0], 11) if (y0 & L) != (b[0] & L): continue seq = [y0, y1] ok = True for i in range(1, n): yi = seq[i] yip1 = u32(a[i] ^ rotl32(yi, 11)) if (yip1 & H) != (b[i] & H): ok = False break if i + 1 < n and (yip1 & L) != (b[i + 1] & L): ok = False break seq.append(yip1) if ok: candidates.append(seq)
if len(candidates) != 1: raise RuntimeError("diag reconstruction ambiguous") return candidates[0]
def recover_s4_prefix_with_z3(s4_suffix, s5_full): A = 0x9908B0DF x = [BitVec(f"x{i}", 32) for i in range(128)]
def s4(i): if i < 128: return x[i] return BitVecVal(s4_suffix[i], 32)
solver = Solver() for i in range(624): xi = s4(i) if i == 623: xip1 = BitVecVal(s5_full[0], 32) else: xip1 = s4(i + 1)
if i >= 227: xi397 = BitVecVal(s5_full[i - 227], 32) else: xi397 = s4(i + 397)
y = (xi & BitVecVal(0x80000000, 32)) | (xip1 & BitVecVal(0x7FFFFFFF, 32)) mag = If((xip1 & BitVecVal(1, 32)) == BitVecVal(1, 32), BitVecVal(A, 32), BitVecVal(0, 32)) nxt = xi397 ^ LShR(y, 1) ^ mag solver.add(nxt == BitVecVal(s5_full[i], 32))
if solver.check() != sat: raise RuntimeError("z3 unsat")
model = solver.model() s4_full = [0] * 624 for i in range(128): s4_full[i] = model.evaluate(x[i]).as_long() & MASK32 for i in range(128, 624): s4_full[i] = s4_suffix[i] return s4_full
def forge_target_token(target_user: str, nonce: bytes, y1990: int, y1991: int, y1992: int, y1993: int) -> str: key = pack_u32(y1990) + pack_u32(y1991) + pack_u32(y1992) + pack_u32(y1993) pt = pkcs7_pad(target_user.encode() + nonce, 16) mac = AES.new(key, AES.MODE_ECB).encrypt(pt)[:16] raw = bytes([len(target_user)]) + target_user.encode() + nonce + mac return base64.b64encode(raw).decode()
def main(): s = socket.create_connection(("nerd.codevinci.it", 9984), timeout=10) s.settimeout(30) t = Tube(s) banner = t.recv_until(PROMPT).decode("utf-8", "replace") target_user = re.search(r"Target user:\s*(\S+)", banner).group(1)
issue_resp = t.cmd("issue a").decode("utf-8", "replace") token_line = next(ln.strip() for ln in issue_resp.splitlines() if re.fullmatch(r"[A-Za-z0-9+/=]+", ln.strip())) raw = base64.b64decode(token_line, validate=True) nonce = raw[1 + raw[0]:1 + raw[0] + 8]
pairs = parse_diag_block(t.cmd("diag 1120"), 1120) outputs = recover_outputs_from_diag(pairs)
s4_suffix = {j % 624: untemper(outputs[j - 2000]) for j in range(2000, 2496)} s5_full = [0] * 624 for j in range(2496, 3120): s5_full[j % 624] = untemper(outputs[j - 2000])
s4_full = recover_s4_prefix_with_z3(s4_suffix, s5_full) y1990 = temper(s4_full[118]) y1991 = temper(s4_full[119]) y1992 = temper(s4_full[120]) y1993 = temper(s4_full[121])
forged = forge_target_token(target_user, nonce, y1990, y1991, y1992, y1993) out = t.cmd(f"validate {forged}").decode("utf-8", "replace") print(re.search(r"CodeVinci\{[^}]+\}", out).group(0))
if __name__ == "__main__": main()python solve_nerdy.pyCodeVinci{I_hop3_y0u_d1dn7_sl0p_th1s_ch4lL_w1th_claude_uFf} CodeVinci CTF 2026 - 🤓 - Cryptography Writeup
https://fuwari.vercel.app/posts/81/codevinci-ctf-2026-nerdy-cryptography-writeup/