Zh3r0 CTF V2 | import numpy as MT

#zh3ro_CTF_2021

#good_challenges_2021

import os
from numpy import random
from Crypto.Cipher import AES
from Crypto.Util.Padding import pad
from secret import flag

def rand_32():
    return int.from_bytes(os.urandom(4),'big')

flag = pad(flag,16)

for _ in range(2):
    # hate to do it twice, but i dont want people bruteforcing it
    random.seed(rand_32())
    iv,key = random.bytes(16), random.bytes(16)
    cipher = AES.new(key,iv=iv,mode=AES.MODE_CBC)
    flag = iv+cipher.encrypt(flag)


print(flag.hex())

• numpy は独自の mersenne twister を実装していてなんかできる。だいたい z3 でなんとかする

from struct import pack,unpack
from numpy import random
from Crypto.Cipher import AES
from z3 import *

(w, n, m, r) = (32, 624, 397, 31)
a = 0x9908B0DF
(u, d) = (11, 0xFFFFFFFF)
(s, b) = (7, 0x9D2C5680)
(t, c) = (15, 0xEFC60000)
l = 18
f = 1812433253
lower_mask = (1<<r)-1
upper_mask = 1<<r

def tamper_state( y):
    y = y ^ (LShR(y, u) & d)
    y = y ^ ((y << s) & b)
    y = y ^ ((y << t) & c)
    y = y ^ (LShR(y, l))
    return y

def untamper(num):
    S = Solver()
    y = BitVec('y', 32)
    y = tamper_state(y)
    S.add(num == y)
    if S.check() == sat:
        m = S.model()
        return m[m.decls()[0]].as_long()

def twist_state(MT):
    for i in range(n):
        x = (MT[i] & upper_mask) + (MT[(i + 1) % n] & lower_mask)
        xA = LShR(x, 1)
        xA = If(x & 1 == 1, xA ^ a, xA)
        MT[i] = simplify(MT[(i + m) % n] ^ xA)

def recover_seed(outputs):
    MT = [BitVec(f'MT[{i}]',32) for i in range(n)]
    SEED = BitVec('seed', 32)
    MT[0] = SEED
    for i in range(1, n):
        temp = f * (MT[i - 1] ^ (LShR(MT[i - 1], (w - 2)))) + i
        MT[i] = temp & ((1 << w) - 1)
    twist_state(MT)
    untampered = list(map(untamper,outputs))
    S = Solver()
    for a,b in zip(untampered,MT):
        S.add(a==b)
    if S.check()==sat:
        m = S.model()
        seed = m[m.decls()[0]].as_long()
        return seed

output = input('enter output in hex:\n')
for _ in range(2):
    output = bytes.fromhex(output)
    iv,flag_enc = output[:16],output[16:]
    rand_outputs = unpack('<4I',iv)

    rand_seed = recover_seed(rand_outputs)
    random.seed(rand_seed)
    iv2,key = random.bytes(16),random.bytes(16)
    cipher = AES.new(key,iv=iv,mode=AES.MODE_CBC)
    output = cipher.decrypt(flag_enc)
    print(output)
    output = output.hex()

別解

from binascii import unhexlify

from Crypto.Cipher import AES
from Crypto.Util.number import bytes_to_long
from numpy import random
from z3 import *

enc_flag = unhexlify(
    "c70defb4147c32dec3d174ffef4c243168b65fb94783fd208291836880a3fd4e03083460ea63e1f7db2faa1854f12554d36d826da680cf45c95dbdbd04016dfbbf0b553547a82a2c2b5063055f12e0dcfafb61b0b9e104023d5ee5c12e0efa39297b1d4970888ff7546974563eeb440c61436df893f046d60a2ed560db39d789"
)


def untemper(x):
    x = unBitshiftRightXor(x, 18)
    x = unBitshiftLeftXor(x, 15, 0xEFC60000)
    x = unBitshiftLeftXor(x, 7, 0x9D2C5680)
    x = unBitshiftRightXor(x, 11)
    return x


def unBitshiftRightXor(x, shift):
    i = 1
    y = x
    while i * shift < 32:
        z = y >> shift
        y = x ^ z
        i += 1
    return y


def unBitshiftLeftXor(x, shift, mask):
    i = 1
    y = x
    while i * shift < 32:
        z = y << shift
        y = x ^ (z & mask)
        i += 1
    return y


# https://github.com/numpy/numpy/blob/main/numpy/random/src/mt19937/mt19937.c
def set_seed(seed):
    RK_STATE_LEN = 624
    seed &= 0xFFFFFFFF
    key = [None] * RK_STATE_LEN
    for pos in range(RK_STATE_LEN):
        key[pos] = seed
        seed = (1812433253 * (seed ^ (seed >> 30)) + pos + 1) & 0xFFFFFFFF
    return key


def update_mt(mt):
    N = 624
    M = 397
    MATRIX_A = 0x9908B0DF
    UPPER_MASK = 0x80000000
    LOWER_MASK = 0x7FFFFFFF
    for kk in range(N - M):
        y = (mt[kk] & UPPER_MASK) | (mt[kk + 1] & LOWER_MASK)
        mt[kk] = mt[kk + M] ^ (y >> 1) ^ (y % 2) * MATRIX_A
    for kk in range(N - M, N - 1):
        y = (mt[kk] & UPPER_MASK) | (mt[kk + 1] & LOWER_MASK)
        mt[kk] = mt[kk + (M - N)] ^ (y >> 1) ^ (y % 2) * MATRIX_A
    y = (mt[N - 1] & UPPER_MASK) | (mt[0] & LOWER_MASK)
    mt[N - 1] = mt[M - 1] ^ (y >> 1) ^ (y % 2) * MATRIX_A


s = Solver()
x = BitVec("x", 33)
mt = set_seed(x)
update_mt(mt)
iv = enc_flag[:16]
for i in range(0, 4):
    s.add(mt[i] == untemper(bytes_to_long(iv[4 * i : 4 * (i + 1)][::-1])))
assert s.check() == sat
m = s.model()
second_seed = m[x].as_long()
random.seed(second_seed)
iv_, key = random.bytes(16), random.bytes(16)
assert iv_ == iv
cipher = AES.new(key, iv=iv_, mode=AES.MODE_CBC)
enc_flag_2 = cipher.decrypt(enc_flag[16:])


s = Solver()
x = BitVec("x", 33)
mt = set_seed(x)
update_mt(mt)
iv = enc_flag_2[:16]
for i in range(0, 4):
    s.add(mt[i] == untemper(bytes_to_long(iv[4 * i : 4 * (i + 1)][::-1])))
s.check()
m = s.model()
first_seed = m[x].as_long()
random.seed(first_seed)
iv_, key = random.bytes(16), random.bytes(16)
assert iv_ == iv
cipher = AES.new(key, iv=iv, mode=AES.MODE_CBC)
flag = cipher.decrypt(enc_flag_2[16:])
print(flag)