Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Why PRNGs are not the same as CSPRNGs
import z3
def sym_xoroshiro128plus(solver, sym_s0, sym_s1, mask, result):
s0 = sym_s0
s1 = sym_s1
sym_r = (sym_s0 + sym_s1)
condition = z3.Bool('c0x%0.16x' % result)
solver.add(z3.Implies(condition, (sym_r & mask) == result & mask))
s1 ^= s0
sym_s0 = z3.RotateLeft(s0, 55) ^ s1 ^ (s1 << 14)
sym_s1 = z3.RotateLeft(s1, 36)
return sym_s0, sym_s1, condition
def find_seed(results_with_masks):
start_s0, start_s1 = z3.BitVecs('start_s0 start_s1', 64)
sym_s0 = start_s0
sym_s1 = start_s1
solver = z3.Solver()
conditions = []
for result, mask in results_with_masks:
sym_s0, sym_s1, condition = sym_xoroshiro128plus(solver, sym_s0, sym_s1, mask, result)
conditions.append(condition)
if solver.check(conditions) == z3.sat:
model = solver.model()
return (model[start_s0].as_long(), model[start_s1].as_long())
else:
return None
find_seed([(0x0, 0x0), (0x206e6172614b2020, 0xffffffffffffffff), (0x2020736e6f794c, 0xffffffffffffff)])
# Output: (12030599390342465081, 17190518429081885642)
def bin2chr(data):
result = ''
while data:
char = data & 0xff
result += chr(char)
data >>= 8
return result
class Xoroshiro128Plus(object):
def __init__(self, seed):
self.seed = seed
@staticmethod
def rotl(x, k):
return ((x << k) & 0xffffffffffffffff) | (x >> 64 - k)
def next(self):
s0 = self.seed[0]
s1 = self.seed[1]
result = (s0 + s1) & 0xffffffffffffffff
s1 ^= s0
self.seed[0] = self.rotl(s0, 55) ^ s1 ^ ((s1 << 14) & 0xffffffffffffffff)
self.seed[1] = self.rotl(s1, 36)
return result
generator = Xoroshiro128Plus([0xb4581c52b5a611f1, 0x849afd73bea7cce9])
print(repr(''.join(bin2chr(generator.next()) for i in range(4))))
# Output: 'ÚÞMtÆ\x19ó8 Karan Lyons 3A?â\x11)ÐÑ{'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment