MT19937在连续输出存在截断的情况下利用z3符号执行推导内部状态以及等价种子

本文主要是介绍MT19937在连续输出存在截断的情况下利用z3符号执行推导内部状态以及等价种子，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

传统针对MT19937的逆向往往需要得到连续且完整的624个随机数，从而逆向出所有内部状态。但在实际场景中，想得到连续且完整的624个随机数是比较困难的，大部分情况下得到的是一些截断的数（例如得到连续的624个数，每个数是原始随机输出中的前16比特）。这种情况下，我们可以利用z3的符号执行推导部分内部状态，甚至可以推导一个“部分等价”的初始种子。本文针对python的random底层c库实现做了详细的分析，并给出了所有中间代码。

关键词：

• MT19937逆向
• MT19937基于z3的内部状态求解
• 复原部分历史随机数生成
• 从伪随机数的输出构造等价种子

---

---

1.MT19937及其逆向

1.1 梅森旋转

先给出维基百科的解释[1]：

为什么叫梅森旋转？

• 算法实现的过程中，参数的选取取决于梅森素数。
• 整个算法的核心操作，是针对状态的旋转。

1.2 MT19937

最为广泛使用Mersenne Twister的一种变体是MT19937，可以产生32位整数序列，其周期非常长，达到$2^{19937}-1$ 。
有关MT19937的所有细节请参考原文：http://www.math.sci.hiroshima-u.ac.jp/m-mat/MT/ARTICLES/mt.pdf

简要实现如下：

def _int32(x):return int(0xFFFFFFFF & x)class MT19937:# 依据seed初始化内部状态（共624个state）def __init__(self, seed):self.mt = [0] * 624self.mt[0] = seedself.mti = 0for i in range(1, 624):self.mt[i] = _int32(1812433253 * (self.mt[i - 1] ^ self.mt[i - 1] >> 30) + i)# 提取一个伪随机数def extract_number(self):if self.mti == 0:self.twist()y = self.mt[self.mti]y = y ^ y >> 11y = y ^ y << 7 & 2636928640y = y ^ y << 15 & 4022730752y = y ^ y >> 18self.mti = (self.mti + 1) % 624return _int32(y)# 旋转状态def twist(self):for i in range(0, 624):y = _int32((self.mt[i] & 0x80000000) + (self.mt[(i + 1) % 624] & 0x7fffffff))self.mt[i] = (y >> 1) ^ self.mt[(i + 397) % 624]if y % 2 != 0:self.mt[i] = self.mt[i] ^ 0x9908b0df

1.3 MT19937的逆向

从上述MT19937的源码中，不难看出，其两个关键的函数都是可逆的。

对extract_number四个关键操作的逆向函数：

def inverse_right(res, shift, bits=32):tmp = resfor i in range(bits // shift):tmp = res ^ tmp >> shiftreturn tmpdef inverse_left(res, shift, bits=32):tmp = resfor i in range(bits // shift):tmp = res ^ tmp << shiftdef inverse_right_mask(res, shift, mask, bits=32):tmp = resfor i in range(bits // shift):tmp = res ^ tmp >> shift & maskreturn tmpdef inverse_left_mask(res, shift, mask, bits=32):tmp = resfor i in range(bits // shift):tmp = res ^ tmp << shift & maskreturn tmp

从而可以根据一个随机数直接逆向出一个状态：

def get_one_state(y):y = inverse_right(y, 18)y = inverse_left_mask(y, 15, 4022730752)y = inverse_left_mask(y, 7, 2636928640)y = inverse_right(y, 11)return _int32(y)

如果能得到连续且完整的624个随机数，即可以恢复出MT19937内部的所有状态，从而能克隆出一个完全一致的随机函数。关于这一逆向，已经有较成熟的开源实现randcrack：https://github.com/tna0y/Python-random-module-cracker

randcrack的代码看起来还是很优雅的，但我对这个模块设计有点奇怪的是，它竟然没有提供一个克隆的random，虽然很简单。所以一般这样使用更舒适：

from randcrack import RandCrack as _RandCrack
from random import Randomclass RandCrack(_RandCrack):def __init__(self):super().__init__()def get_random(self):state = []for i in self.mt[:624]:b = ''for j in i:b += str(j)state.append(int(b, 2))rand = Random()rand.setstate((3, tuple(state+[0]), None))return randrc = RandCrack()
r = Random()for i in range(624):rc.submit(r.getrandbits(32))my_rand = rc.get_random()for i in range(1000):assert r.getrandbits(32) == my_rand.getrandbits(32), f"index: {i}"

4.基于z3的MT19937的内部状态求解

在不逆向算法的前提下，也可以利用z3直接进行求解：

from z3 import *
def solve_one_state(out):y1 = BitVec('y1', 32)y2 = BitVec('y2', 32)y3 = BitVec('y3', 32)y4 = BitVec('y4', 32)y = BitVecVal(out, 32)s = Solver()equations = [y2 == y1 ^ (LShR(y1, 11)),y3 == y2 ^ ((y2 << 7) & 0x9D2C5680),y4 == y3 ^ ((y3 << 15) & 0xEFC60000),y == y4 ^ (LShR(y4, 18))]s.add(equations)s.check()return s.model()[y1].as_long()

2.连续输出存在截断的情况下z3的求解部分内部状态

2.1 原理

假设连续输出若干个伪随机数$p_1,p_2...p_{1248}$，其中，$p_i$为16位。由python random模块的底层c源代码[2]可以看出，每个随机数实际是输出随机数的高16位，相当于每个原始输出随机数的截断了一半。

此时，我们仍然可以利用z3的符号执行去求解可能的内部状态，可以把已知的部分比特位给z3作为约束，尝试求解。因为构造的矩阵是非满秩的，所以得到的状态是满足约束条件的可能解，如果给出的约束足够多，例如上述给出了1248个16位的输出数，也可以得到确定的状态。

例如，假设一个只得到一个随机数的高16位，则可以将其构造为$p_i|{|}^{\prime }{?}^{\prime }\ast 16$传给相应的解析函数处理，解析函数处理后，将其转为z3中的约束。核心就是使用Extact函数（用于从一个位向量（BitVector）中提取一段连续的比特位）。

def get_one_symbolic(out, index):# 参数检查略out = out.zfill(32)guess_state = BitVec(f'symbolic_guess_{index}', 32)out = out[::-1]for i, bit in enumerate(out):if bit != '?':self.solver.add(Extract(i, i, guess_state) == bit)return guess_state

关于这部分工作，在查找资料的时候发现也有前人做了相应的开源：https://github.com/icemonster/symbolic_mersenne_cracker

2.2 应用一：完全推导内部状态

在上述symbolic_mersenne_cracker项目中给出的test，就是一个完全推导内部状态的例子：

def test():'''This test tries to clone Python random's internal state, given partial output from getrandbits'''r1 = Random()ut = Untwister()for _ in range(1337):random_num = r1.getrandbits(16)#Just send stuff like "?11????0011?0110??01110????01???"#Where ? represents unknown bitsut.submit(bin(random_num)[2:] + '?'*16)r2 = ut.get_random()for _ in range(624):assert r1.getrandbits(32) == r2.getrandbits(32)logger.debug('Test passed!')

通过1248个16位的随机数，能完全恢复内部的状态，从而克隆出一个完全等价的伪随机数生成器。

2.3 应用二：部分推导，复原部分历史随机数生成

修改Untwister模块获取random的代码，改为恢复成给定seed后的状态（默认是给出后面输出的状态）：

主要修改点为，参考[3]：

• seed后的index为N=624。
  
• seed后的第一个state为0x80000000。
  

from untwister import Untwister as _Untwister
class Untwister(_Untwister):def __init__(self):super().__init__()self.first_MT = self.MTself.index = 624def get_random(self):self.solver.add(self.first_MT[0] == 0x80000000)self.solver.check()model = self.solver.model()state = [model[x].as_long() if model[x] is not None else 0for x in self.first_MT]result_state = (3, tuple(state+[624]), None)rand = random.Random()rand.setstate(result_state)return rand

这样得到random就是seed后的 random，能够复原部分历史的随机数生成：

ut = Untwister()
r1 = random.Random()
my_r = [r1.randint(0, 6) for i in range(666)]for i in my_r:res = bin(i)[2:].zfill(3) + "?" * 29ut.submit(res)ut_rand = ut.get_random()for i in my_r:assert i == ut_rand.randint(0, 6)

3.生成等价种子

在只得到部分截断连续随机数输出的条件下，想完整的恢复种子是不太可能的，但是可以分析random模块种子的初始化过程，从而生成一个与原始种子不相同，但播种后后续部分输出相同的种子。

分析random底层seed相关的初始化部分：

/* initializes mt[N] with a seed */
static void
init_genrand(RandomObject *self, uint32_t s)
{int mti;uint32_t *mt;mt = self->state;mt[0]= s;for (mti=1; mti<N; mti++) {mt[mti] =(1812433253U * (mt[mti-1] ^ (mt[mti-1] >> 30)) + mti);/* See Knuth TAOCP Vol2. 3rd Ed. P.106 for multiplier. *//* In the previous versions, MSBs of the seed affect   *//* only MSBs of the array mt[].                                *//* 2002/01/09 modified by Makoto Matsumoto                     */}self->index = mti;return;
}/* initialize by an array with array-length */
/* init_key is the array for initializing keys */
/* key_length is its length */
static void
init_by_array(RandomObject *self, uint32_t init_key[], size_t key_length)
{size_t i, j, k;       /* was signed in the original code. RDH 12/16/2002 */uint32_t *mt;mt = self->state;init_genrand(self, 19650218U);i=1; j=0;k = (N>key_length ? N : key_length);for (; k; k--) {mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * 1664525U))+ init_key[j] + (uint32_t)j; /* non linear */i++; j++;if (i>=N) { mt[0] = mt[N-1]; i=1; }if (j>=key_length) j=0;}for (k=N-1; k; k--) {mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * 1566083941U))- (uint32_t)i; /* non linear */i++;if (i>=N) { mt[0] = mt[N-1]; i=1; }}mt[0] = 0x80000000U; /* MSB is 1; assuring non-zero initial array */
}

用python分别实现：

from z3 import *
prng_N = 624def u32(x):return x & 0xffffffffdef init_genrand(s):mt = [0 for _ in range(prng_N)]mt[0] = BitVecVal(s, 32)mti = 1while mti < prng_N:mt[mti] = u32(1812433253 * (mt[mti-1] ^ LShR(mt[mti-1], 30)) + mti        )mti += 1return mt, mtidef init_by_array(init_key):key_length = len(init_key)mt, mti = init_genrand(19650218)i, j = 1, 0k = prng_N if prng_N > key_length else key_lengthwhile k:mt[i] = u32((mt[i] ^ ((mt[i-1] ^ LShR(mt[i-1], 30)) * 1664525)) + init_key[j] + j)i, j = i + 1, j + 1if i >= prng_N:mt[0] = mt[prng_N-1]i = 1if j >= key_length:j = 0k -= 1k = prng_N - 1while k:mt[i] = u32((mt[i] ^ ((mt[i-1] ^ LShR(mt[i-1], 30)) * 1566083941)) - i)i += 1if i >= prng_N:mt[0] = mt[prng_N-1]i = 1k -= 1mt[0] = 0x80000000return mt

可以发现random模块的流程：

• 如果输入的种子是一个小于32位的数，就会直接把这个种子作为mt[0]，然后生成后续的所有状态。
• 如果输入的种子是一个大于32位的书，就会把输入的种子变成一个数组init_key，每个数组是一个32位数，用这个数组进行一些位操作得到最终的状态，并把第一个状态设置为0x80000000。

假设我们依据2.3得到了一组可能得初始状态（seed后的）init_rand_state，那么我们要构造一个等价种子，使得播种后能产生指定的输出，思路如下：

• 将种子设为长为624的z3向量数组seed_vecs。
• 用python重写底层c的init_by_array和init_genrand函数。
• 将向量数组传入init_by_array函数中参与运算。
• 将这些参与运算完后的向量与init_rand_state做等价约束传入z3中。
• z3解方程，得到可能得seed_vecs。
• 将seed_vecs拼接成一个大数，传入python的random模块中。

通过这些步骤，能得到满足上述要求的种子。代码如下：

def recover_seed(outputs):ut = Untwister()for output in outputs:ut.submit(output)ut_rand = ut.get_random()ut_rand_state = ut_rand.getstate()[1][:-1]seed_vecs = [BitVec(f"seed_{i}", 32) for i in range(624)]seed_rand_state = init_by_array(seed_vecs)s = Solver()for a, b in zip(seed_rand_state, ut_rand_state):s.add(a == b)s.check()model = s.model()seed_init_key = [model[x].as_long() if model[x] is not None else 0for x in seed_vecs]seed_rand_seed = sum([x * (2 ** (idx * 32))for idx, x in enumerate(seed_init_key)])return seed_rand_seed

4.完整代码及工具封装

有关直接对MT19937逆向的代码在第1章已经完全给出，这里仅给出涉及符号执行的代码。

from random import Random
from untwister import Untwister as _Untwister
from z3 import *
from randcrack import RandCrack as _RandCrackprng_N = 624def u32(x):return x & 0xffffffffdef init_genrand(s):mt = [0 for _ in range(prng_N)]mt[0] = BitVecVal(s, 32)mti = 1while mti < prng_N:mt[mti] = u32(1812433253 * (mt[mti-1] ^ LShR(mt[mti-1], 30)) + mti# 1812433253 * (mt[mti-1] ^ (mt[mti-1] >> 30)) + mti)mti += 1return mt, mtidef init_by_array(init_key):key_length = len(init_key)mt, mti = init_genrand(19650218)i, j = 1, 0k = prng_N if prng_N > key_length else key_lengthwhile k:mt[i] = u32((mt[i] ^ ((mt[i-1] ^ LShR(mt[i-1], 30)) * 1664525)) + init_key[j] + j)i, j = i + 1, j + 1if i >= prng_N:mt[0] = mt[prng_N-1]i = 1if j >= key_length:j = 0k -= 1k = prng_N - 1while k:mt[i] = u32((mt[i] ^ ((mt[i-1] ^ LShR(mt[i-1], 30)) * 1566083941)) - i)i += 1if i >= prng_N:mt[0] = mt[prng_N-1]i = 1k -= 1mt[0] = 0x80000000return mtclass RandCrack(_RandCrack):def __init__(self):super().__init__()def get_random(self):state = []for i in self.mt[:624]:b = ''for j in i:b += str(j)state.append(int(b, 2))rand = Random()rand.setstate((3, tuple(state+[0]), None))return randclass Untwister(_Untwister):def __init__(self):super().__init__()self.first_MT = self.MTself.index = 624def get_random_init(self):self.solver.add(self.first_MT[0] == 0x80000000)print(self.solver.check())model = self.solver.model()state = [model[x].as_long() if model[x] is not None else 0for x in self.first_MT]result_state = (3, tuple(state+[624]), None)rand = Random()rand.setstate(result_state)return randdef recover_seed(outputs):ut = Untwister()for output in outputs:ut.submit(output)ut_rand = ut.get_random_init()ut_rand_state = ut_rand.getstate()[1][:-1]seed_vecs = [BitVec(f"seed_{i}", 32) for i in range(624)]seed_rand_state = init_by_array(seed_vecs)s = Solver()for a, b in zip(seed_rand_state, ut_rand_state):s.add(a == b)s.check()model = s.model()seed_init_key = [model[x].as_long() if model[x] is not None else 0for x in seed_vecs]seed_rand_seed = sum([x * (2 ** (idx * 32))for idx, x in enumerate(seed_init_key)])return seed_rand_seed# 根据部分输出恢复可能的种子
def test_recover_seed():# 预设初始种子my_seed = 1173791373my_rand = Random(my_seed)my_outputs = [my_rand.randint(0, 6) for i in range(1000)]my_outputs_sym = [bin(i)[2:].zfill(3) + '?' * 29 for i in my_outputs]guess_seed = recover_seed(my_outputs_sym)guess_rand = Random(guess_seed)assert my_seed != guess_seed# testfor i in range(1000):assert my_outputs[i] == guess_rand.randint(0, 6)print("test recover seed pass!")def test_randcrack():rc = RandCrack()r = Random()for i in range(624):rc.submit(r.getrandbits(32))my_rand = rc.get_random()for i in range(1000):assert r.getrandbits(32) == my_rand.getrandbits(32), f"index: {i}"print("test randcrack pass!")def test_ut():ut = Untwister()r1 = Random()my_r = [r1.randint(0, 6) for i in range(666)]for i in my_r:res = bin(i)[2:].zfill(3) + "?" * 29ut.submit(res)ut_rand = ut.get_random_init()for i in my_r:assert i == ut_rand.randint(0, 6)print("test Untwister pass!")if __name__ == '__main__':test_randcrack()test_ut()#test_recover_seed()

上述代码的能力：

• 1.若得到完整且连续的624个随机数，使用randcrack即可得到一个完全克隆的random。
• 2.若得到不完整且连续的若干个随机数（数量很大），使用Untwister有概率能恢复完整的内部状态。
• 3.若得到不完整且连续的若干个随机数（数量不大），使用Untwister的get_random_init能恢复seed后的状态，能够复原历史的随机数生成。
• 4.在3的基础上，能够恢复一个种子，该种子在seed后能重现给定随机数的生成。

后续考虑封装成pip工具包… 但是封装成工具包涉及易用性和容错性的问题，貌似工作量不小。

---

参考

• [1] https://zh.wikipedia.org/zh-hans/%E6%A2%85%E6%A3%AE%E6%97%8B%E8%BD%AC%E7%AE%97%E6%B3%95
• [2] https://github.com/python/cpython/blob/3.8/Modules/_randommodule.c
• [3] https://imp.ress.me/blog/2022-11-13/seccon-ctf-2022#janken-vs-kurenaif

---

这篇关于MT19937在连续输出存在截断的情况下利用z3符号执行推导内部状态以及等价种子的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---