CER FRUMOS

crypto

Challenge

The server generates 625 random values using Python's random.getrandbits, outputs them, then uses further PRNG output to derive an AES key and nonce to encrypt the flag. We're given the 625 observed values and the encrypted flag.

Each observed output is a 48-bit value from random.getrandbits(48) followed by a discarded 16-bit random.getrandbits(16). Python's random module uses Mersenne Twister (MT19937) internally.

Understanding MT19937

MT19937 maintains 624 internal 32-bit state words. Each call to getrandbits(k) consumes some of those words, tempering them before output. A 48-bit getrandbits(48) uses 2 words (64 bits total, top 48 kept), and a 16-bit call uses a third word (top 16 bits kept).

The tempering transform is invertible, but since we only see 48 of 64 bits from the first two words, we set up a symbolic system and let Z3 solve for the full state.

Setting Up Z3 Constraints

A symbolic MT19937 emulator is built in Z3: all 624 state words become BitVec variables. For each observed 48-bit output x, we express the two tempered output words symbolically and add constraints:

class SymMT19937:
    def __init__(self):
        self.state = [z3.BitVec(f's_{i}', 32) for i in range(624)]
        self.index = 0

    def get32(self):
        if self.index >= 624:
            self.twist()
            self.index = 0
        y = self.state[self.index]
        y = y ^ z3.LShR(y, 11)
        y = y ^ ((y << 7) & 0x9d2c5680)
        y = y ^ ((y << 15) & 0xefc60000)
        y = y ^ z3.LShR(y, 18)
        self.index += 1
        return y

for i, x in enumerate(xs):
    w1 = mt.get32()
    w2 = mt.get32()
    mt.get32()           # discarded 16-bit call
    solver.add(w1 == (x & 0xffffffff))
    solver.add(z3.Extract(31, 16, w2) == (x >> 32))

Recovering the State

Once Z3 finds a satisfying assignment, we extract the 624 original state words. The key subtlety: after the twist operation, mt.state[i] holds a complex Z3 expression rather than a plain variable. We must query the model using the original symbolic names s_0 ... s_623:

m = solver.model()
# Correct: ask for original symbolic vars by name
state = [m[z3.BitVec(f's_{i}', 32)].as_long() for i in range(624)]

Querying m[s] on a post-twist expression fails with a Z3Exception — you must always address the original leaf variables.

Rederiving the Key

With the 624-word state restored into Python's random module, we fast-forward through the same number of outputs the challenge script consumed, then replicate its key/nonce derivation:

random.setstate((3, tuple(state + [0]), None))

# Replay the observed outputs
for _ in range(625):
    random.getrandbits(48)
    random.getrandbits(16)

# Replicate 10 more discarded calls from chall script
for i in range(10):
    random.getrandbits(32)

key_seed   = random.getrandbits(64)
nonce_seed = random.getrandbits(64)

key   = hashlib.sha256(str(key_seed).encode()).digest()
nonce = hashlib.sha256(str(nonce_seed).encode()).digest()[:16]

cipher    = AES.new(key, AES.MODE_CBC, iv=nonce)
decrypted = cipher.decrypt(bytes.fromhex(enc_flag))
print("Flag:", decrypted.decode('utf-8', errors='ignore'))

Result

Flag: TFCCTF{...}