predict_next_rand.py

from z3 import BitVec, Solver
from subprocess import Popen, PIPE

seed = "B65DD562AAEA877BA21332BC2A782A76"
status =  [seed[i * 8:(i + 1) * 8] for i in range(4)][::-1]

p = Popen(['./tiny_mt'] + status, stdout=PIPE)

TINYMT32_MASK = 0x7fffffff
TINYMT32_SH0 = 1
TINYMT32_SH1 = 10
TINYMT32_SH8 = 8
UINT32_MASK = 0xffffffff
MAT1 = 0x8f7011ee
MAT2 = 0xfc78ff1f
TMAT = 0x3793fdff

def next_rand(state):
    y = state[3]
    x = (state[0] & TINYMT32_MASK) ^ state[1] ^ state[2]
    x ^= (x << TINYMT32_SH0) & UINT32_MASK
    y ^= (y >> TINYMT32_SH0) ^ x
    state[0] = state[1]
    state[1] = state[2]
    state[2] = x ^ ((y << TINYMT32_SH1) & UINT32_MASK)
    state[3] = y
    state[1] ^= (-(y & 1)) & UINT32_MASK & MAT1
    state[2] ^= (-(y & 1)) & UINT32_MASK & MAT2

    t0 = state[3]
    t1 = (state[0] + (state[2] >> TINYMT32_SH8)) & UINT32_MASK
    t0 ^= t1
    t0 ^= (-(t1 & 1)) & UINT32_MASK & TMAT

    return t0

state = [BitVec("state{}".format(i), 64) for i in range(4)]
s = Solver()

for i in range(8):
    output = next_rand(state)
    actual = int(p.stdout.readline())
    s.add(output== actual)

print("poyo")
s.check()
print("poyo")
m = s.model()
print("poyo")

for i in range(8, 8 + 30):
    output = m.evaluate(next_rand(state))
    actual = int(p.stdout.readline())
    print(output, actual, m.evaluate(output == actual))

p.terminate()

tiny_mt.c

#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include "./tinymt32.h"

tinymt32_t tiny_mt;

int main(int argc, char *argv[]) {
    tiny_mt.mat1 = 0x8F7011EE;
    tiny_mt.mat2 = 0xFC78FF1F;
    tiny_mt.tmat = 0x3793fdff;
    tiny_mt.status[0] = strtol(argv[1], NULL, 16);
    tiny_mt.status[1] = strtol(argv[1], NULL, 16);
    tiny_mt.status[2] = strtol(argv[1], NULL, 16);
    tiny_mt.status[3] = strtol(argv[1], NULL, 16);
    while (1) {
        printf("%u\n", tinymt32_generate_uint32(&tiny_mt));
    }
}