diff --git a/ChromeRandomnessPredictor.py b/ChromeRandomnessPredictor.py new file mode 100644 index 0000000..3d7b534 --- /dev/null +++ b/ChromeRandomnessPredictor.py @@ -0,0 +1,71 @@ +import struct +from z3 import * +from typing import List, Optional + + +class ChromeRandomnessPredictor: + def __init__(self, sequence: List[float]): + self.sequence = sequence + self.__c_state0, self.__c_state1 = None, None + self.__internalSequence = sequence[::-1] + self.__mask = 0xFFFFFFFFFFFFFFFF + self.__solver = z3.Solver() + self.__se_state0, self.__se_state1 = z3.BitVecs("se_state0 se_state1", 64) + self.__s0_ref, self.__s1_ref = self.__se_state0, self.__se_state1 + + for i in range(len(self.__internalSequence)): + self.__xorshift128p_symbolic() + mantissa = self.__recover_mantissa(self.__internalSequence[i]) + self.__solver.add(mantissa == LShR(self.__se_state0, 11)) + + if self.__solver.check() != z3.sat: + return None + + model = self.__solver.model() + self.__c_state0 = model[self.__s0_ref].as_long() + self.__c_state1 = model[self.__s1_ref].as_long() + + def predict_next(self) -> Optional[float]: + if self.__c_state0 is None or self.__c_state1 is None: + return None + out = self.__xorshift128p_concrete_backwards() + return self.__to_double(out) + + def __xorshift128p_symbolic(self) -> None: + se_s1 = self.__se_state0 + se_s0 = self.__se_state1 + self.__se_state0 = se_s0 + se_s1 ^= se_s1 << 23 + se_s1 ^= z3.LShR(se_s1, 17) # Logical shift instead of Arthmetric shift + se_s1 ^= se_s0 + se_s1 ^= z3.LShR(se_s0, 26) + self.__se_state1 = se_s1 + + # Performs the typical XorShift128p but in reverse. + def __xorshift128p_concrete_backwards(self): + """ + - V8 gives us random numbers by popping them off of their cache. + - This is why we have to reverse `sequence` to `__internal_sequence = sequence[::-1]` in the constructor. + - Essentially, they give us random numbers in LIFO order, so we need to process them in reverse (like a simulated FIFO). + + - In order to move forward down the chain, we have to perform our concrete XOR backwards. If we performed + our XOR forwards, we would technically be moving backwards in time, and therefore return numbers to the caller + that they already have. + """ + # Must set resullt here, otherwise we skip numbers by 1 step + result = self.__c_state0 + ps1 = self.__c_state0 + ps0 = self.__c_state1 ^ (self.__c_state0 >> 26) + ps0 = ps0 ^ self.__c_state0 + # Performs the normal shift 17 but in reverse. + ps0 = ps0 ^ (ps0 >> 17) ^ (ps0 >> 34) ^ (ps0 >> 51) & self.__mask + # Performs the normal shift 23 bbut in reverse. + ps0 = (ps0 ^ (ps0 << 23) ^ (ps0 << 46)) & self.__mask + self.__c_state0, self.__c_state1 = ps0, ps1 + return result + + def __recover_mantissa(self, double: float) -> int: + return double * (0x1 << 53) + + def __to_double(self, val: int) -> float: + return (val >> 11) / (2**53) \ No newline at end of file diff --git a/FirefoxAndSafariRandomnessPredictor.py b/FirefoxAndSafariRandomnessPredictor.py new file mode 100644 index 0000000..729f115 --- /dev/null +++ b/FirefoxAndSafariRandomnessPredictor.py @@ -0,0 +1,69 @@ +from z3 import * +from typing import List, Optional + +class FirefoxAndSafariRandomnessPredictor: + def __init__(self, sequence: List[float]): + self.sequence = sequence + self.__mask = 0xFFFFFFFFFFFFFFFF + self.__concrete_state0, self.__concrete_state1 = [None, None] + self.__se_state0, self.__se_state1 = BitVecs("se_state0 se_state1", 64) + self.__s0_ref, self.__s1_ref = self.__se_state0, self.__se_state1 + self.__solver = Solver() + + for i in range(len(sequence)): + mantissa = self.__recover_mantissa(sequence[i]) + self.__xorshift128p_symbolic() + self.__solver.add( + ((self.__se_state0 + self.__se_state1) & 0x1FFFFFFFFFFFFF) + == int(mantissa) + ) + + if self.__solver.check() != sat: + return None + + model = self.__solver.model() + self.__concrete_state0 = model[self.__s0_ref].as_long() + self.__concrete_state1 = model[self.__s1_ref].as_long() + + # We have to get our concrete state up to the same point as our symbolic state, + # therefore, we discard as many "predict_next()" calls as we have len(sequence). + # Otherwise, we would return random numbers to the caller that they already have. + # Now, when we return from predict_next() we get the actual next + for i in range(len(sequence)): + self.__xorshift128p_concrete() + + def predict_next(self) -> Optional[float]: + """ + Predict the next random number. + """ + if self.__concrete_state0 is None or self.__concrete_state1 is None: + return None + out = self.__xorshift128p_concrete() + return self.__to_double(out) + + def __xorshift128p_concrete(self) -> int: + s1 = self.__concrete_state0 & self.__mask # state0 & self.__mask + s0 = self.__concrete_state1 & self.__mask # state1 & self.__mask + s1 ^= (s1 << 23) & self.__mask + s1 ^= (s1 >> 17) & self.__mask + s1 ^= s0 & self.__mask + s1 ^= (s0 >> 26) & self.__mask + self.__concrete_state0 = s0 & self.__mask + self.__concrete_state1 = s1 & self.__mask + return (self.__concrete_state0 + self.__concrete_state1) & self.__mask + + def __xorshift128p_symbolic(self) -> None: + s1 = self.__se_state0 # sym_state0 + s0 = self.__se_state1 # sym_state1 + s1 ^= s1 << 23 + s1 ^= LShR(s1, 17) + s1 ^= s0 + s1 ^= LShR(s0, 26) + self.__se_state0 = self.__se_state1 # sym_state0 = sym_state1 + self.__se_state1 = s1 # sym_state1 = s1 + + def __to_double(self, val: int): + return float(val & 0x1FFFFFFFFFFFFF) / (0x1 << 53) + + def __recover_mantissa(self, double: float) -> float: + return double * (0x1 << 53) diff --git a/xs128p.py b/xs128p.py index aededa9..384dffd 100644 --- a/xs128p.py +++ b/xs128p.py @@ -1,92 +1,29 @@ -import sys import math -import struct -import random from z3 import * -MASK = 0xFFFFFFFFFFFFFFFF +from ChromeRandomnessPredictor import ChromeRandomnessPredictor +from FirefoxAndSafariRandomnessPredictor import FirefoxAndSafariRandomnessPredictor -# xor_shift_128_plus algorithm -def xs128p(state0, state1, browser): - s1 = state0 & MASK - s0 = state1 & MASK - s1 ^= (s1 << 23) & MASK - s1 ^= (s1 >> 17) & MASK - s1 ^= s0 & MASK - s1 ^= (s0 >> 26) & MASK - state0 = state1 & MASK - state1 = s1 & MASK - if browser == 'chrome': - generated = state0 & MASK - else: - generated = (state0 + state1) & MASK - - return state0, state1, generated - -# Symbolic execution of xs128p -def sym_xs128p(slvr, sym_state0, sym_state1, generated, browser): - s1 = sym_state0 - s0 = sym_state1 - s1 ^= (s1 << 23) - s1 ^= LShR(s1, 17) - s1 ^= s0 - s1 ^= LShR(s0, 26) - sym_state0 = sym_state1 - sym_state1 = s1 - if browser == 'chrome': - calc = sym_state0 - else: - calc = (sym_state0 + sym_state1) - - condition = Bool('c%d' % int(generated * random.random())) - if browser == 'chrome': - impl = Implies(condition, LShR(calc, 12) == int(generated)) - elif browser == 'firefox' or browser == 'safari': - # Firefox and Safari save an extra bit - impl = Implies(condition, (calc & 0x1FFFFFFFFFFFFF) == int(generated)) - - slvr.add(impl) - return sym_state0, sym_state1, [condition] - -def reverse17(val): - return val ^ (val >> 17) ^ (val >> 34) ^ (val >> 51) - -def reverse23(val): - return (val ^ (val << 23) ^ (val << 46)) & MASK - -def xs128p_backward(state0, state1, browser): - prev_state1 = state0 - prev_state0 = state1 ^ (state0 >> 26) - prev_state0 = prev_state0 ^ state0 - prev_state0 = reverse17(prev_state0) - prev_state0 = reverse23(prev_state0) - # this is only called from an if chrome - # but let's be safe in case someone copies it out - if browser == 'chrome': - generated = prev_state0 - else: - generated = (prev_state0 + prev_state1) & MASK - return prev_state0, prev_state1, generated # Print 'last seen' random number # and winning numbers following that. # This was for debugging. We know that Math.random() -# is called in the browser zero times (updated) for each page click +# is called in the browser zero times (updated) for each page click # in Chrome and once for each page click in Firefox. # Since we have to click once to enter the numbers # and once for Play, we indicate the winning numbers # with an arrow. -def power_ball(generated, browser): +def power_ball(browser, generated, skip=4): # for each random number (skip 4 of 5 that we generated) - for idx in range(len(generated[4:])): + for idx in range(len(generated[skip:])): # powerball range is 1 to 69 poss = list(range(1, 70)) # base index 4 to skip - gen = generated[4+idx:] + gen = generated[skip + idx :] # get 'last seen' number g0 = gen[0] gen = gen[1:] - # make sure we have enough numbers + # make sure we have enough numbers if len(gen) < 6: break print(g0) @@ -96,112 +33,60 @@ def power_ball(generated, browser): for jdx in range(5): index = int(gen[jdx] * len(poss)) val = poss[index] - poss = poss[:index] + poss[index+1:] + poss = poss[:index] + poss[index + 1 :] nums.append(val) # print indicator - if idx == 0 and browser == 'chrome': - print('--->', end='') - elif idx == 2 and browser == 'firefox': - print('--->', end='') + if idx == 0 and browser == "chrome": + print("--->", end="") + elif idx == 2 and browser == "firefox": + print("--->", end="") else: - print(' ', end='') + print(" ", end="") # print winning numbers - print(sorted(nums), end='') + print(sorted(nums), end="") # generate / print power number or w/e it's called - double = gen[5] + double = gen[skip + 1] val = int(math.floor(double * 26) + 1) print(val) -# Firefox nextDouble(): - # (rand_uint64 & ((1 << 53) - 1)) / (1 << 53) -# Chrome nextDouble(): - # (state0 | 0x3FF0000000000000) - 1.0 -# Safari weakRandom.get(): - # (rand_uint64 & ((1 << 53) - 1) * (1.0 / (1 << 53))) -def to_double(browser, out): - if browser == 'chrome': - double_bits = (out >> 12) | 0x3FF0000000000000 - double = struct.unpack('d', struct.pack('> 12) - elif browser == 'firefox': - recovered = dubs[idx] * (0x1 << 53) - elif browser == 'safari': - recovered = dubs[idx] / (1.0 / (1 << 53)) - generated.append(recovered) + RANDOM_NUMBERS_TO_GENERATE = 10 - # setup symbolic state for xorshift128+ - ostate0, ostate1 = BitVecs('ostate0 ostate1', 64) - sym_state0 = ostate0 - sym_state1 = ostate1 - slvr = Solver() - conditions = [] - - # run symbolic xorshift128+ algorithm for three iterations - # using the recovered numbers as constraints - for ea in range(len(dubs)): - sym_state0, sym_state1, ret_conditions = sym_xs128p(slvr, sym_state0, sym_state1, generated[ea], browser) - conditions += ret_conditions - - if slvr.check(conditions) == sat: - # get a solved state - m = slvr.model() - state0 = m[ostate0].as_long() - state1 = m[ostate1].as_long() - slvr.add(Or(ostate0 != m[ostate0], ostate1 != m[ostate1])) - if slvr.check(conditions) == sat: - print('WARNING: multiple solutions found! use more dubs!') - print('state', state0, state1) - - generated = [] - # generate random numbers from recovered state - for idx in range(15): - if browser == 'chrome': - state0, state1, out = xs128p_backward(state0, state1, browser) - out = state0 & MASK - else: - state0, state1, out = xs128p(state0, state1, browser) - - double = to_double(browser, out) - print('gen', double) - generated.append(double) - - # use generated numbers to predict powerball numbers - power_ball(generated, browser) + if browser == "chrome": + predictor = ChromeRandomnessPredictor(sequence) + elif browser == "firefox" or browser == "safari": + predictor = FirefoxAndSafariRandomnessPredictor(sequence) else: - print('UNSAT') + raise Exception(f"unknown browser {browser}") + + for _ in range(RANDOM_NUMBERS_TO_GENERATE): + next = predictor.predict_next() + generated.append(next) + # use generated numbers to predict powerball numbers + power_ball(browser=browser, generated=generated, skip=len(sequence)) + main()