0x1 - Learn CTF: Reverse Engineering

2026-02-23 15:30 +0700

re-010 — Network byte-transform checker
re-012 — Constraint-based checker (f1..f8)

re-010 — Network byte-transform checker

Summary

Type: Reversing (ELF64, stripped, PIE)
Behavior: TCP server flag checker
Port: 31338
Expected input length: 37 bytes
Result: :) on success, :( on failure
Flag: CBC{c72b6b1feb2dbb3132380e1a9f967441}

Notes

The binary does not read from stdin directly; it binds/listens and validates client input over a socket.
Validation is split into 3 blocks of 16 transformed-byte checks using constant tables in .rodata.
Recovered plaintext chunks:
- CBC{c72b6b1feb2d
- bb3132380e1a9f96
- 7441}
Combined final flag:

CBC{c72b6b1feb2dbb3132380e1a9f967441}

Validation

# run service
./chall

# in another shell
python3 - << 'PY'
import socket
flag='CBC{c72b6b1feb2dbb3132380e1a9f967441}'
s=socket.create_connection(('127.0.0.1',31338))
print(s.recv(200))
s.sendall(flag.encode()+b'\n')
print(s.recv(200))
PY

Expected response contains :).

Minimal solver (repro)

# recovers: CBC{c72b6b1feb2dbb3132380e1a9f967441}
idx=[3,8,13,2,7,12,1,6,11,0,5,10,15,4,9,14]
adds=[7,8,11,16,23,32,43,56,71,88,107,128,151,176,203,232]
blk1=[0x82,0x3e,0x6d,0x53,0x79,0x85,0x6d,0x6a,0xad,0x9b,0xa2,0xb1,0xfb,0x12,0x2c,0x19]
blk2=[0x38,0x38,0x71,0x43,0x4f,0x59,0x8d,0x6b,0xa8,0xba,0x9d,0xb1,0xcd,0xe3,0x2f,0x20]
blk3=[0x38,0x08,0x0b,0x44,0x17,0x20,0x5f,0x38,0x47,0x8f,0x6b,0x80,0x97,0x2c,0xcb,0xe8]

def inv_byte(out, add):
    for x in range(256):
        if (x + add) % 257 == out:
            return x
    raise ValueError('no solution')

p1=[0]*16
p2=[0]*16
p3=[0]*16
for i in range(16):
    p1[idx[i]] = inv_byte(blk1[i], adds[i])
    p2[idx[i]] = inv_byte(blk2[i], adds[i])
    p3[idx[i]] = inv_byte(blk3[i], adds[i])

flag = (bytes(p1)+bytes(p2)+bytes(p3)).split(b'\x00',1)[0].decode('ascii')
print(flag)

re-012 — Constraint-based checker (`f1..f8`)

Summary

Type: Reversing (ELF64, stripped, PIE)
Behavior: TCP flag-checker server (not stdin checker)
Port: 57005
Final flag: CBC{116c7c40348dcf6385e848d6b49cb2b8}

1) Initial recon

file chall
checksec --file=chall
strings -tx chall | egrep 'Enter flag:|Nope|Congrats|CBC\{'

Findings:

64-bit ELF, dynamically linked, stripped.
Full RELRO, Canary, NX, PIE.
Strings showed:
- Enter flag:
- Nope
- Congrats, flag : CBC{

Running directly looked like a hang. strace showed why:

program binds 0.0.0.0:57005
calls listen() then blocks on accept()

So it is a socket service checker.

2) Confirm I/O model

nc 127.0.0.1 57005

Protocol observed:

server sends Enter flag:
client sends one line
server replies Nope or success string

Also verified checker expects exactly 32 chars for the inside of CBC{...}.

3) Reverse core logic

Disassembly around the checker function (starts near 0x31c5) shows:

Reads input into a C++ string
Rejects unless length is 0x20 (32)
Copies bytes into a 32-byte buffer
Iterates over a table of function descriptors in .data
Calls tiny predicates (f1..f8) at addresses around 0x25e9..0x2f85

Each predicate is a byte-level arithmetic relation over selected indices of the 32-byte input. The .data table contains 48 constraints total.

4) Solve with Z3

Modeled 32 unknown bytes as BitVec(8) and encoded all 48 relations.

Solver output:

116c7c40348dcf6385e848d6b49cb2b8

Final flag:

CBC{116c7c40348dcf6385e848d6b49cb2b8}

5) Validation

Submitting that string to the service returned:

Congrats, flag : CBC{116c7c40348dcf6385e848d6b49cb2b8}

Confirmed correct.

Minimal solver (repro)

from z3 import *
from pathlib import Path
import struct

p = Path('chall').read_bytes()
DATA_OFF = 0x8000
NREC = 48
name_map = {
    0x6008: 'f1', 0x600b: 'f2', 0x600e: 'f3', 0x6011: 'f4',
    0x6014: 'f5', 0x6017: 'f6', 0x601a: 'f7', 0x601d: 'f8'
}

recs = []
for i in range(NREC):
    b = p[DATA_OFF + i*0x40 : DATA_OFF + (i+1)*0x40]
    nameptr = struct.unpack_from('<Q', b, 0x20)[0]
    f = name_map[nameptr]
    a,b1,c,d,k1,k2 = struct.unpack_from('<iiiiii', b, 0x28)
    recs.append((f,a,b1,c,d,k1,k2))

x = [BitVec(f'x{i}', 8) for i in range(32)]
s = Solver()
for xi in x:
    s.add(And(xi >= 0x20, xi <= 0x7e))

for (f,a,b,c,d,k1,k2) in recs:
    A, B = ZeroExt(24, x[a]), ZeroExt(24, x[b])
    if f == 'f1':
        C = ZeroExt(24, x[c]); s.add(((A ^ B) - C) & 0xff == (k1 & 0xff))
    elif f == 'f2':
        C = ZeroExt(24, x[c]); s.add(((A + B) ^ C) & 0xff == (k1 & 0xff))
    elif f == 'f3':
        C = ZeroExt(24, x[c]); s.add(((A - B) ^ C) & 0xff == (k1 & 0xff))
    elif f == 'f4':
        C = ZeroExt(24, x[c]); s.add(((A ^ B) + C) & 0xff == (k1 & 0xff))
    elif f == 'f5':
        C, D = ZeroExt(24, x[c]), ZeroExt(24, x[d])
        s.add((((A + B) ^ C) - D) & 0xff == (k1 & 0xff))
    elif f == 'f6':
        s.add((A ^ B) & 0xff == ((k1 ^ k2) & 0xff))
    elif f == 'f7':
        s.add((A + B) & 0xff == ((k1 - k2) & 0xff))
    elif f == 'f8':
        s.add((A - B) & 0xff == ((k1 + k2) & 0xff))

assert s.check() == sat
m = s.model()
inner = ''.join(chr(m[xi].as_long()) for xi in x)
print('CBC{' + inner + '}')

Zero's Blog