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()
基本变量
x = Int('x')
;也可以一次性定义多个变量,例 x,y=Ints('x y')
a = BitVec('BitVec_1',8)
FLAG = Bool("FLAG")
x = Real('x')
基本关系
MT19937
srand
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
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;
}
}
rand
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
恢复state
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
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
原文始发于微信公众号(山石网科安全技术研究院):密码学 | 使用z3-solver破解随机数
- 左青龙
- 微信扫一扫
-
- 右白虎
- 微信扫一扫
-
评论