Cold Beacon Nim key validator solved with z3

rev
flag hiCTF{c0ld_b34c0n_cfg_uns34l3d_fr0m_th3_s4mpl3}

Result

  • Key: C0ldB34c0n::unl0ck::7a3f
  • Flag: hiCTF{c0ld_b34c0n_cfg_uns34l3d_fr0m_th3_s4mpl3}
output 
$ ./cold-beacon 'C0ldB34c0n::unl0ck::7a3f'
hiCTF{c0ld_b34c0n_cfg_uns34l3d_fr0m_th3_s4mpl3}

Files

  • extracted/cold-beacon - ELF x86-64, stripped, non-PIE, dynamically linked, compiled from Nim (evidence: syncio.nim, cmdline.nim, IOError, paramStr, readFile, Nim signal handlers).
  • cold-beacon.zip, chall-info.txt.

Triage / analysis

  • Takes one argument (./cold-beacon <key>). Wrong/absent key prints config sealed.
  • strings/rodata showed:
    • a TracerPid anti-debug: it reads /proc/self/status and bails if TracerPid is non-zero (function 0x403aec).
    • an obfuscated 14-byte string at .rodata 0x405e00 (954<3=z)?;6?>P) - decoded at runtime by XOR 0x5a → "config sealed\n" (function 0x4041f9).
    • SHA-256 (K constants at 0x405e80, IV at 0x405f80, custom compression routine at 0x403de7).
    • an encrypted config blob at .rodata 0x405e40 (47 bytes) and a 32-byte expected SHA-256 value at 0x405e20.

Key check (function 0x4043c0 / 0x403cff / 0x403dc4)

Arguments are the Nim argv string; Nim stores a string as {len; data…} so the key bytes live at argv_ptr + 8, length must be 24.

0x403cff is a table-driven validator over 23 constraint groups. For each group it indexes key bytes via a permutation table (0x405fc0) and applies one of three ops against an expected byte (0x405fa0), with counts (0x406050) and opcodes (0x406070):

  • op 0/3/5 → XOR of the selected key bytes must equal expected
  • op 1/4 → (mod-256) SUM of the selected key bytes must equal expected
  • op 2 → product (low byte) of two selected key bytes must equal expected

0x403dc4 adds three more relations (key index = raw offset − 8):

  • key[10] = (0xa8 - key[9]) & 0xff
  • key[20] = key[12] ^ key[4]
  • (key[12] + key[13]) & 0xff == 0xe3

Solving the whole system (all constraints are linear/byte-local, so any solver works - used with a printable-ASCII constraint):

output 
KEY: C0ldB34c0n::unl0ck::7a3f

Config decryption (function 0x404333)

Once the key passes (and TracerPid == 0):

  1. sha256(key) (0x403de7) is computed into a 32-byte value.
  2. Keystream generated by 0x404119(sha256, 47): repeatedly sha256(state32 || be32(counter)) for counter = 0,1,… concatenating digests until 47 bytes are produced (SHA-256-based DRBG/CTR).
  3. Ciphertext = .rodata 0x405e40 (47 bytes); plaintext = ciphertext XOR keystream.
  4. It first compares sha256(key) against the stored value at 0x405e20 (integrity/self-check). Then prints the decrypted config, i.e. the flag string.

Commands used

bash 
1file extracted/cold-beacon
2readelf -S/-d extracted/cold-beacon
3objdump -d extracted/cold-beacon            # located refs to 0x405e00/0x405e20/0x405e40
4objdump -s -j .rodata extracted/cold-beacon # extracted tables + blobs
5
6# Bypass the TracerPid anti-debug for dynamic analysis (LD_PRELOAD shim
7# redirects /proc/self/status to a file with "TracerPid:\t0");
8# then gdb at 0x403cff / 0x403dc4 to confirm the string ABI and constraint logic.
9
10# Solve key constraints (z3)
11python3 solve.py            # -> C0ldB34c0n::unl0ck::7a3f
12
13./extracted/cold-beacon 'C0ldB34c0n::unl0ck::7a3f'

Notes

  • Non-PIE → absolute addresses in gdb work directly.
  • The TracerPid check only matters under a debugger; a normal run passes it, so the real key alone is sufficient (verified without any preload).

The validators are not enough

One catch: the 23 table groups (0x403cff) + 3 relations (0x403dc4) do not pin the key - they are necessary but not sufficient.

  • Enumerating every printable-ASCII key of length 24 that satisfies all 26 relations yields exactly 4 candidates:
    • C ltB#$c0n::unl0ck::7a3f
    • Cl4Bcdc0n::unl0ck::7a3f`
    • Cpl$Bstc0n::unl0ck::7a3f
    • C0ldB34c0n::unl0ck::7a3f ← only one that unlocks
  • Confirmed in gdb: the first three pass both 0x403cff and 0x403dc4 (al=1 for each) yet the binary prints config sealed. So the validators alone are a decoy-friendly check.
  • The real gate is at 0x4043c8: after decrypting .rodata 0x405e40, it computes sha256(plaintext) and compares against the 32-byte pin at .rodata 0x405e20. The stored pin is sha256 of the flag, NOT sha256(key) (verified: sha256(b"hiCTF{c0ld_b34c0n_cfg_uns34l3d_fr0m_th3_s4mpl3}") == 0502f285…66ad40). Because the keystream is seeded by sha256(key), only the single key whose seed reproduces the pinned plaintext passes — a classic tag-pinned key recovery.
  • Keystream 0x404119: sha256(key) → DRBG sha256(state32 || be32(counter)), counter = 0,1,… concatenated to 47 bytes. pt = ct XOR ks → flag. Reproduced byte-exact offline.

Result

  • Key: C0ldB34c0n::unl0ck::7a3f
  • Flag: hiCTF{c0ld_b34c0n_cfg_uns34l3d_fr0m_th3_s4mpl3}