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()

基本变量

基本关系

MT19937

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]
    }
}

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;
 }
}

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

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

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

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

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()

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

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