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

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

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

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

defsymbolic_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

defget_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, ERRORassert all(map(lambda x: x in'01?', guess)), ERRORassert 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()

defsymbolic_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 statefor 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] ^ xBreturn MT

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

原文始发于微信公众号（SAINTSEC）：使用z3-solver破解密码学随机数