You can attack these using the Z3 theorem prover. I've implemented such an attack in Python in order to predict values in a lottery simulator.
As mentioned previously, XorShift128+ is used in most places now, so that is what we are attacking. You begin by implementing the normal algorithm so you can understand it.
def xs128p(state0, state1):
s1 = state0 & 0xFFFFFFFFFFFFFFFF
s0 = state1 & 0xFFFFFFFFFFFFFFFF
s1 ^= (s1 << 23) & 0xFFFFFFFFFFFFFFFF
s1 ^= (s1 >> 17) & 0xFFFFFFFFFFFFFFFF
s1 ^= s0 & 0xFFFFFFFFFFFFFFFF
s1 ^= (s0 >> 26) & 0xFFFFFFFFFFFFFFFF
state0 = state1 & 0xFFFFFFFFFFFFFFFF
state1 = s1 & 0xFFFFFFFFFFFFFFFF
generated = (state0 + state1) & 0xFFFFFFFFFFFFFFFF
return state0, state1, generated
The algorithm takes in two state variables, XORs and shifts them around, then returns the sum of the updated state variables. What is also important is how each engine takes the uint64 returned and converts it to a double. I found this info by digging through each implementation's source code.
# Firefox (SpiderMonkey) nextDouble():
# (rand_uint64 & ((1 << 53) - 1)) / (1 << 53)
# Chrome (V8) nextDouble():
# ((rand_uint64 & ((1 << 52) - 1)) | 0x3FF0000000000000) - 1.0
# Safari (WebKit) weakRandom.get():
# (rand_uint64 & ((1 << 53) - 1) * (1.0 / (1 << 53)))
Each is a little different. You then can take the doubles produced by Math.random() and recover some lower bits of the uint64 produced by the algorithms.
Next is implementing the code in Z3 so that it can be symbolically executed and the state can be solved for. See the Github link for more context. It looks pretty similar to the normal code except that you tell the solver that the lower bits must equal the recovered lower bits from the browser.
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
calc = (sym_state0 + sym_state1)
condition = Bool('c%d' % int(generated * random.random()))
if browser == 'chrome':
impl = Implies(condition, (calc & 0xFFFFFFFFFFFFF) == 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]
If you supply 3 consecutively generated doubles to Z3 it should be able to recover your state. Below is a snippet from the main function. It is calling the symbolically executed XorShift128+ algorithm on two of Z3's 64 bit integers (the unknown state variables), providing the lower (52 or 53) bits from the recovered uint64s.
If that is successful the solver will return SATISFIABLE and you can get the state variables that it solved for.
for ea in xrange(3):
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()
There is a slightly more detailed writeup here that focuses on using this method to predict winning lottery numbers in a powerball simulator.