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 | quit
Target 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/rei/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
# solve_nerdy.py
import base64
import re
import socket
from dataclasses import dataclass
from Crypto.Cipher import AES
from z3 import BitVec, BitVecVal, If, LShR, Solver, sat
MASK32 = 0xFFFFFFFF
PROMPT = 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
@dataclass
class 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://blog.rei.my.id/posts/81/codevinci-ctf-2026-nerdy-cryptography-writeup/