Add working Chrome/Firefox/Safari checkers

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)

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)

xs128p.py

@@ -1,72 +1,9 @@
-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.
@@ -76,13 +13,13 @@ def xs128p_backward(state0, state1, browser):
 #   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:]
@@ -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':
+        if idx == 0 and browser == "chrome":
-            print('--->', end='')
+            print("--->", end="")
-        elif idx == 2 and browser == 'firefox':
+        elif idx == 2 and browser == "firefox":
-            print('--->', end='')
+            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('<Q', double_bits))[0] - 1
-    elif browser == 'firefox':
-        double = float(out & 0x1FFFFFFFFFFFFF) / (0x1 << 53) 
-    elif browser == 'safari':
-        double = float(out & 0x1FFFFFFFFFFFFF) * (1.0 / (0x1 << 53))
-    return double
-
 
 def main():
-    # Note: 
+    browser = "chrome"  # | 'safari' | 'firefox'
-        # Safari tests have always turned up UNSAT
+    print("BROWSER: %s" % browser)
-        # Wait for an update from Apple?
-    # browser = 'safari'
-    browser = 'chrome'
-    # browser = 'firefox'
-    print('BROWSER: %s' % browser)
 
     # In your browser's JavaScript console:
-    # _ = []; for(var i=0; i<5; ++i) { _.push(Math.random()) } ; console.log(_)
+    #  - For Chrome/Firefox : `Array.from({ length: 5 }, Math.random);`
-    # Enter at least the 3 first random numbers you observed here:
+    #  - For Safari : `JSON.stringify(Array.from({ length: 5 }, Math.random), null, 2);`
-    # Observations show Chrome needs ~5
+    # Enter at least the 5 first random numbers you observed here:
-    dubs = [
+    # Observations show all browsers need ~5
-        0.5368584449767335, 0.883588766746984, 0.7895949638905317, 
+    sequence = [
-        0.5106241305628436, 0.49965622623126693]
+        0.5368584449767335,
-    if browser == 'chrome':
+        0.883588766746984,
-        dubs = dubs[::-1]
+        0.7895949638905317,
+        0.5106241305628436,
+        0.49965622623126693,
+    ]
 
-    print(dubs)
+    print(sequence)
+    # Add original created random numbers to generated (copy the list)
+    generated = sequence[:]
 
-    # from the doubles, generate known piece of the original uint64 
+    RANDOM_NUMBERS_TO_GENERATE = 10
-    generated = []
-    for idx in range(len(dubs)):
-        if browser == 'chrome':
-            recovered = struct.unpack('<Q', struct.pack('d', dubs[idx] + 1))[0] & (MASK >> 12)
-        elif browser == 'firefox':
-            recovered = dubs[idx] * (0x1 << 53) 
-        elif browser == 'safari':
-            recovered = dubs[idx] / (1.0 / (1 << 53))
-        generated.append(recovered)
 
-    # setup symbolic state for xorshift128+
+    if browser == "chrome":
-    ostate0, ostate1 = BitVecs('ostate0 ostate1', 64)
+        predictor = ChromeRandomnessPredictor(sequence)
-    sym_state0 = ostate0
+    elif browser == "firefox" or browser == "safari":
-    sym_state1 = ostate1
+        predictor = FirefoxAndSafariRandomnessPredictor(sequence)
-    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)
+        raise Exception(f"unknown browser {browser}")
-
-            double = to_double(browser, out)
-            print('gen', double)
-            generated.append(double)
 
+    for _ in range(RANDOM_NUMBERS_TO_GENERATE):
+        next = predictor.predict_next()
+        generated.append(next)
     # use generated numbers to predict powerball numbers
-        power_ball(generated, browser)
+    power_ball(browser=browser, generated=generated, skip=len(sequence))
-    else:
+
-        print('UNSAT')
 
 main()