GhostKey - EH4X CTF 2026

Category: Reverse Engineering / Crypto Points: 477 Author: benzo Solves: Post-CTF

Note: We solved this challenge after the CTF ended. We were participating in two CTFs simultaneously and couldn't allocate enough time to this beast during the competition window. The approach documented here took significant computational effort (~11 minutes of SAT solving alone).

Challenge

We're given a single Go binary ghost (ELF 64-bit, statically linked, not stripped). Running it prompts for a 32-character key and validates it through multiple checks before decrypting a flag.

Step 1: Reverse Engineering the Binary

Using Ghidra/IDA on the Go binary, we identified 8 sequential validation checks on the 32-byte key. Each byte must be printable ASCII (0x20 - 0x7e).

Validation Pipeline

Step 2: Understanding Each Constraint

2.1 LFSR Check (Linear Feedback Shift Register)

The binary runs the key through a 16-bit LFSR with initial state 0xACE1 and feedback polynomial 0xB400. The final state must equal 0x4358.

A 16-bit Fibonacci LFSR. The key bits are fed as input, XORed with the feedback. (Source: Wikipedia - LFSR)

def lfsr_final(input_bits):
    state = 0xACE1  # Initial state
    for byte_idx in range(32):
        bv = 0
        for bit in range(8):
            bv |= (input_bits[byte_idx * 8 + bit] << bit)
        for bit in range(8):
            fb = ((bv >> bit) & 1) ^ (state & 1)
            state >>= 1
            if fb:
                state ^= 0xB400  # Feedback polynomial
    return state
# Must equal 0x4358

Key insight: The LFSR is a linear function over GF(2), meaning it produces 16 linear equations over the 256 key bits. This is exploitable!

2.2 Tag XOR (8 Groups)

The 32 bytes are divided into 8 groups of 4. The XOR of each group must match a target:

This gives 64 more linear (GF(2)) equations (8 groups × 8 bits).

2.3 Nibble XOR (4 Groups)

For each group of 8 bytes, XOR the low nibble with the high nibble of every byte:

Another 16 linear equations.

2.4 Pair Sums (Modular Arithmetic)

12 pairs of key bytes must satisfy sum-modulo constraints:

7 pairs have two valid sums (bold), creating 2^7 = 128 branches to explore. This is the main source of complexity — these are non-linear constraints (addition, not XOR).

2.5 Column Sums (mod 97)

The key is viewed as a 4×8 matrix. Each column sum mod 97 must match:

2.6 S-Box XOR

The standard AES S-Box (Rijndael) is applied to every even-indexed byte, and the XOR of all results must equal 0x66:

AES SubBytes operation — each byte is substituted via the S-Box lookup table. (Source: Wikipedia - AES)

This is the hardest constraint — the S-Box is non-linear (multiplicative inverse in GF(2^8) followed by an affine transformation).

Step 3: Solution Strategy — SAT Solving

After trying multiple approaches (GF(2) Gaussian elimination, constraint propagation, Z3, OR-Tools, brute-force C), we settled on SAT solving with a universal encoding.

Why SAT?

The problem mixes linear (XOR) and non-linear (modular arithmetic, S-Box) constraints. SAT solvers excel at finding solutions in these mixed constraint spaces through:

DPLL/CDCL search tree — the solver explores variable assignments, backtracks on conflicts, and learns clauses to prune the search. (Source: Wikipedia - CDCL)

3.1 Variable Encoding

Each key bit becomes a SAT variable:

Total: 256 primary variables (vars 1-256) for the 32-byte key.

3.2 Constraint Encoding

Linear Constraints → XOR Clauses

LFSR, Tag XOR, and Nibble XOR are all linear over GF(2), encoded as native XOR clauses for CryptoMiniSat or via Tseitin transformation for pure CNF solvers:

Pair Sums → Bit-Blasted Addition + Table Constraint

For each pair (a, b), we:

1. Bit-blast the addition: 8-bit ripple-carry adder using half/full adder gates
2. Constrain the 9-bit sum to allowed values using indicator variables (av())

def add_bits(ab, bb, n):
    """Ripple-carry adder in CNF via Tseitin gates."""
    res = []; carry = None
    for i in range(n):
        if carry is None:
            s, carry = ha(ab[i], bb[i])  # Half adder
        else:
            s, carry = fa(ab[i], bb[i], carry)  # Full adder
        res.append(s)
    res.append(carry)
    return res

S-Box → Table Constraint with Indicator Variables

For each even-indexed byte, we create indicator variables for each possible printable ASCII value:

for c in PRINTABLE:  # 0x20 to 0x7E (95 values)
    ind = new_var()
    # If ind is true, key_bits must equal c AND sbox_out must equal SBOX[c]
    for j in range(8):
        clauses.append((-ind, key_bits[j]) if (c >> j) & 1 else (-ind, -key_bits[j]))
        clauses.append((-ind, out_bits[j]) if (SBOX[c] >> j) & 1 else (-ind, -out_bits[j]))
clauses.append(tuple(all_indicators))  # At least one must be true

3.3 Universal Encoding — All 128 Branches at Once

Instead of running 128 separate SAT instances (one per branch), we built a single universal encoding that allows the solver to explore all branches simultaneously:

The key function is av() (allow values) — instead of fixing a pair sum to one specific value, it introduces indicator variables for each valid sum:

def av(bits, vals, nb):
    """Allow bits to equal any value in vals."""
    if len(vals) == 1:
        # Fix directly
        for i in range(nb):
            clauses.append((bits[i],) if (vals[0]>>i)&1 else (-bits[i],))
    else:
        # Create indicator for each allowed value
        inds = []
        for v in vals:
            ind = new_var()
            inds.append(ind)
            for i in range(nb):
                clauses.append((-ind, bits[i]) if (v>>i)&1 else (-ind, -bits[i]))
        clauses.append(tuple(inds))  # At least one value must be chosen

3.4 Running the Solvers

We ran three SAT solvers in parallel on the universal encoding:

CaDiCaL won the race! Its advanced CDCL engine with inprocessing (variable elimination, subsumption, vivification) cracked the 5,878-variable, 39,922-clause formula in ~11 minutes.

Step 4: Extracting the Key and Decrypting

The Key

From CaDiCaL's satisfying assignment, we extracted the 32-byte key:

Verification — All 8 Checks Pass

Decryption

aes_key = SHA256(key[:16])   # SHA256("Gh0stK3y-R3v3rs3")
iv      = MD5(key[16:])      # MD5("-M3-1f-U-C4n!!!!")
cipher  = AES.new(aes_key, AES.MODE_CBC, iv)
flag    = cipher.decrypt(encrypted_flag)

Flag

Failed Approaches (Honorable Mentions)

During the solve process, we tried 28+ different solver scripts before landing on the winning approach:

The lesson: when you have a mix of linear and non-linear constraints, encode everything as SAT and let a state-of-the-art CDCL solver handle it.

Tools Used

• Ghidra — Go binary reverse engineering
• CaDiCaL 2.x — SAT solver (winner)
• CryptoMiniSat 5.11 — SAT solver with native XOR support
• Kissat 4.0 — SAT solver
• Python 3 — Constraint encoding and solution extraction
• PyCryptodome — AES-CBC decryption

References

• Wikipedia - Linear Feedback Shift Register
• Wikipedia - Rijndael S-Box
• Wikipedia - Conflict-Driven Clause Learning
• CaDiCaL SAT Solver
• CryptoMiniSat
• Tseitin Transformation