crack random numbers using z3-solver

在 CTF 密码学竞赛题目中，大多数情况下我们都需要先分析代码，然后再利用各种定理、公式对问题进行规约简化，最后我们再编写代码进行题目的解答。不过在编写代码的时候，如果能善于利用一些现成的工具则会让我们事半功倍。这个系列的文章则是介绍这些由密码学“巨人”们已经开发好的“神器”，如果使用得好有时还会与出乎意料的效果。

这篇文章我们将介绍对称密码学中的“神器”——z3-solver，首先我们简单介绍其基本的用法，然后我们将使用 z3-solver 破解MT19937这个著名的伪随机数生成器以展示其“威力”。

---

基本用法

基本流程

以python中为例，我们使用 z3-solver 的一个基本流程：

首先初始化一个约束器：sol = Solver()，

然后向其中添加各种约束 sol.add(x+y==c)，

最后我们检查是否有解：sol.check()，其会返回三个状态：sat，unsat，unknown， 只有等于 sat 时我们才能获取解，

获取解：m = s.model()

基本流程就是这样，剩下我们需要学习的，就是怎么添加约束，以及一些添加约束的技巧。在此之前，我们还要了解一下 z3-solver 中的基本变量。

---

基本变量

Int(name) ：（注意所有的变量开头都是大写）整数，也就是我们数学中使用的那种，没有字节长度限制，等价于 python 中的 int。例 x = Int('x')；也可以一次性定义多个变量，例 x,y=Ints('x y')

BitVec(name,size) ：比特向量，第一个参数是自定义的变量名称，第二个参数size则为比特长度，相当于 C 语言中的 int。例 a = BitVec('BitVec_1',8)

Bool(name) ：布尔值，只有两个状态，True 或者 Fasle。例 FLAG = Bool("FLAG")

Real(name)：实数类型。例 x = Real('x')

---

基本关系

基本关系自然是 与 和 或：

And([expr1,expr2,])：要求所有表达式都为 True

Or([expr1,expr2,])：要求至少一个表达式为 True‍

---

MT19937

接下来我们先简单介绍一下 MT19937 的整个算法流程，然后就开始讲解如何在某些特定情况下使用 z3-solver 对其进行破解。

---

首先 srand 会根据输入的种子 seed 以一定的线性变换生成一组 state

void srand(int seed)
{
 index=0;
 isInit=1;
 MT[0]=seed;
 //对数组的其它元素进行初始化
    for(inti=1;i<624;i++)
    {
        int t=1812433253*(MT[i-1]^(MT[i-1]>>30))+i;
        MT[i]=t&0xffffffff;//取最后的32位赋给MT[i]
    }
}

---

generate 会根据当前的 state 生成下一组 state

void generate()
{
 for(inti=0;i<624;i++)
 {
  //2^31=0x80000000
  //2^31-1=0x7fffffff
  int y=(MT[i]&0x80000000)+(MT[(i+1)%624]&0x7fffffff);
  MT[i]=MT[(i+397)%624]^(y>>1);
  if(y&1)
   MT[i]^=2567483615;
 }
}

---

最后，一个 state 通过线性变换后可以生成一个 32 字节的随机数。

int rand() 
{ 
    if(!isInit) 
    srand((int)time(NULL)); 
 if(index == 0) 
 generate(); 
 int y = MT[index]; 
 y = y ^ (y >> 11); 
 y = y ^ ((y << 7) & 2636928640); 
 y = y ^ ((y << 15) & 4022730752); 
 y = y ^ (y >> 18); 
 index = (index + 1) % 624; 
 return y; 
} 

---

破解 MT19937

破解 MT19937 即意味着能够预测后续的随机数，或者是恢复前序的随机数。那么正常来说我们只需要 624 个连续的完整 32 字节的随机数，我们就能够逆向 rand 函数和 generate 函数，从而恢复 state，也就掌握了所有的随机数。但是如果给出的随机数不够完整呢？由于所有的操作都是线性的，于是这里我们可以使用z3-solver来还原 state。而使用 z3-solver 还有一个好处就是，我们完全可以根据流程正向的构造代码（也就是照猫画虎），而不需要自己动脑子去想逆向的解密函数。

接下来我们还是先使用 z3-solver 来解决常规情况，即拥有 624 个连续的完整 32 字节的随机数，如何恢复state。

---

在 random 的最后一步，有一系列的自异或和与运算的操作，我们称这过程为 tamper，于是我们根据随机数恢复state的过程就称之为 untamper。

def symbolic_untamper(self, solver, y):
    name = next(SYMBOLIC_COUNTER)

    y1 = BitVec('y1_%d'%(name), 32)
    y2 = BitVec('y2_%d'%(name), 32)
    y3 = BitVec('y3_%d'%(name), 32)
    y4 = BitVec('y4_%d'%(name), 32)

    equations = [
        y2 == y1 ^ (LShR(y1, 11)),
        y3 == y2 ^ ((y2 << 7) & 0x9D2C5680),
        y4 == y3 ^ ((y3 << 15) & 0xEFC60000),
        y == y4 ^ (LShR(y4, 18))
    ]

    solver.add(equations)
    return y1

首先我们定义四个变量 y1,y2,y3,y4，由于总共有624个数，为了区分，每一组都用计数器 SYMBOLIC_COUNTER 来命名。然后根据 tamper 的规则对这几个变量进行约束，使结果等于我们的 y，最后将这些约束添进solver中。然后直接就能够获取 state，之后根据 state 的状态更新公式进行更新，再做 tamper 就可以生成后续的随机数了。

不过如果我们拿到完整的随机数，也可以写一个简单的逆算法来恢复 state，这里并不能体现 z3-solver 有什么厉害之处。那么如果我们手里的随机数不够完整呢？

---

利用不完整的随机数恢复破解 MT19937

假设我们的 32 个比特随机数是不完整的，类似于 "?11????0011?0110??01110????01???"。

那么第一步，我们还是定义变量，

def get_symbolic(self, guess):
    name = next(SYMBOLIC_COUNTER)
    ERROR = 'Must pass a string like "?1100???1001000??0?100?10??10010" where ? represents an unknown bit'

    assert type(guess) == str, ERROR
    assert all(map(lambda x: x in '01?', guess)), ERROR
    assert len(guess) <= 32, "One 32-bit number at a time please"
    guess = guess.zfill(32)

    self.symbolic_guess = BitVec('symbolic_guess_%d'%(name), 32)
    guess = guess[::-1]

    for i, bit in enumerate(guess):
        if bit != '?':
            self.solver.add(Extract(i, i, self.symbolic_guess) == bit)

    return self.symbolic_guess

首先为了区分还是使用了计数器，然后是一些对输入 guess 的一些类型合法性判定。

之后由于大小端的问题，我们将 guess 反转，然后开始添加约束，主要是将那些不为 "?" 的确定比特约束下来，得到 symbolic_guess。

然后同样的，我们使用 symbolic_untamper ，根据 symbolic_guess 约束获得 symbolic_state

接着再根据 symbolic_state 约束原本的状态组 MT，

我们先定义状态组 MT。

def __init__(self):
    name = next(SYMBOLIC_COUNTER)
    self.MT = [BitVec('MT_%d_%d'%(i,name), 32) for i in range(624)]
    self.index = 0
    self.solver = Solver()

然后复写一遍 generate，记为symbolic_twist

def symbolic_twist(self, MT, n=624, upper_mask=0x80000000, lower_mask=0x7FFFFFFF, a=0x9908B0DF, m=397):
    '''
        This method models MT19937 function as a Z3 program
    '''
    MT = [i for i in MT] #Just a shallow copy of the state

    for i in range(n):
        x = (MT[i] & upper_mask) + (MT[(i+1) % n] & lower_mask)
        xA = LShR(x, 1)
        xB = If(x & 1 == 0, xA, xA ^ a) #Possible Z3 optimization here by declaring auxiliary symbolic variables
        MT[i] = MT[(i + m) % n] ^ xB

    return MT

具体的约束规则为

def submit(self, guess):
    '''
        You need 624 numbers to completely clone the state.
            You can input less than that though and this will give you the best guess for the state
    '''
    if self.index >= 624:
        name = next(SYMBOLIC_COUNTER)
        next_mt = self.symbolic_twist(self.MT)
        self.MT = [BitVec('MT_%d_%d'%(i,name), 32) for i in range(624)]
        for i in range(624):
            self.solver.add(self.MT[i] == next_mt[i])
        self.index = 0

    symbolic_guess = self.get_symbolic(guess)
    symbolic_state = self.symbolic_untamper(self.solver, symbolic_guess)
    self.solver.add(self.MT[self.index] == symbolic_state)
    self.index += 1

先将状态组 MT 进行约束  self.MT[self.index] == symbolic_state，当 624 个填满了后，我们根据 symbolic_twist 更新 MT next_mt = self.symbolic_twist(self.MT)， self.MT[i] == next_mt[i]

然后继续约束 self.MT[self.index] == symbolic_state

最后我们solve，等待，就可以解出当前的 state 了，继而可以进行后续的随机数生成了。

完整的文件可见 github 项目：GitHub - icemonster/symbolic_mersenne_cracker: Models the mersenne twister used by Python Random as a symbolic program. This allows recovering the state given a few outputs

       

原文始发于微信公众号（山石网科安全技术研究院）：密码学 ｜ 使用z3-solver破解随机数