One of the most widely used random number generators must be the one built into Google. But how random is it? Can you rely on it for your daily dose of entropy? Feeling lucky?

Google random number generator runs in the browser and works like this

``````apparently_random = Math.floor(Math.random() * (max - min + 1)) + min;
``````

The source of perceived randomness comes from `Math.random()`. After taking a look at the docs, this note rings a bell:

Note: Math.random() does not provide cryptographically secure random numbers. Do not use them for anything related to security. Use the Web Crypto API instead, and more precisely the window.crypto.getRandomValues() method.

But don’t be mad at JavaScript. This method is implemented in the browser and varies depending on the engine. Chrome uses the V8 engine, which is open-source. Its pseudo random number generator is based on an algorithm called `xorshift128+`

``````static inline void XorShift128(uint64_t* state0, uint64_t* state1) {
uint64_t s1 = *state0;
uint64_t s0 = *state1;
*state0 = s0;
s1 ^= s1 << 23;
s1 ^= s1 >> 17;
s1 ^= s0;
s1 ^= s0 >> 26;
*state1 = s1;
}
``````

Its name describes it pretty well: it consists of a couple of bitwise XORs and shifts applied to a 128-bit internal state.

Then the 64-bit int is converted to a double. To understand the process, let’s look at the structure of a double. Doubles consist of 64 bits: 1 bit sign, 11 bit exponent, 52 bit mantissa.  The end result is a double in the [0, 1) range. It is derived by manipulating the `state0` value which is right shifted by 12 bits and ORed with `0x3FF0000000000000` setting the exponent to 01111111111 in binary, which is 1023. This produces a value between 1 and 2. Finally, 1 is subtracted to obtain a value in the range (0, 1].

``````static inline double ToDouble(uint64_t state0) {
static const uint64_t kExponentBits = uint64_t{0x3FF0000000000000};
uint64_t random = (state0 >> 12) | kExponentBits;
return bit_cast<double>(random) - 1;
}
``````

In order to predict the next value, all we need is the 128 bit seed stored in `state0` and `state1`. Our goal is to restore the seed from a list of consecutive outputs of the random number generator and predict the next value.

This problem can be tackled using Python and the Z3 library. Z3 is an SMT solver (Satisfiability Modulo Theories) capable of determining whether a set of mathematical expressions is satisfiable and determine a suitable set of inputs. This approach was already used in 2016 for cracking `Math.random()`, but a few things have changed since then. Firstly, the way of converting 64-bit ints into double was changed and described above. Secondly, instead of running the xorshift algorithm on every call, the new implementation uses a cache of 64 values. Calling `Math.random()` pops a value from this cache. When the cache becomes empty, it is refilled again with 64 values generated by xorshift. This means that the list of outputs should be reversed. Moreover, if the cache was refilled in the process of generating values, the list should be split into sublists corresponding to different caches and reversed. I will not implement this procedure to keep things simple.

Z3 works with symbolic values. The symbolic implementation of xorshift128+ is very similar to the C++ code above. Note that in Z3`LShR` is logical right shift and `>>` performs an arithmetic shift.

``````solver = z3.Solver()
state0, state1 = z3.BitVecs("state0 state1", 64)

def xs128p(state0, state1):
s1 = state0
s0 = state1
s1 ^= s1 << 23
s1 ^= z3.LShR(s1, 17)
s1 ^= s0
s1 ^= z3.LShR(s0, 26)

return s0, s1
``````

Functions that are also needed are the Python versions of `ToDouble` and a function which does the opposite and converts doubles into 64-bit ints

``````def to_double(state0):
bits = (state0 >> 12) | 0x3FF0000000000000
return struct.unpack('d', struct.pack('<Q', bits)) - 1

def from_double(val):
return struct.unpack('<Q', struct.pack('d', val + 1)) & 0x3FFFFFFFFFFFFFFF
``````

In the loop over each known output `point`, first the symbolic xorshift is executed. Then `state0` is right shifted by 12 bits like in the `ToDouble` function, which produces the symbolic mantissa

``````points = points[::-1]
for point in points:
state0, state1 = xs128p(state0, state1)
calc = z3.LShR(state0, 12)
``````

Our next goal is to set conditions on the generated mantissa `calc`. I am not aware of a straight-forward way of using floor rounding in this case, so the conditions are set for `calc` to be between a lower and upper value which are derived from `point`. The `point` value was generated by executing `Math.floor(x * (max - min + 1)) + min`, which allows us to determine the lower and upper bounds

``````def normalize(val):
return (val - min) / (max - min + 1)

lower = normalize(point)
upper = normalize(point + 1)
``````

Then these values are converted into 64 bit ints using `from_double`

``````lower = from_double(normalize(point))
upper = from_double(normalize(point + 1))
``````

The part that interests us is the mantissa, that is the last 52 bits. They are extracted by ANDing with `0x000FFFFFFFFFFFFF`, which is 2^52 - 1

``````lower = lower & 0x000FFFFFFFFFFFFF
upper = upper & 0x000FFFFFFFFFFFFF
``````

Finally, the condition is formulated and added to the solver

``````solver.add(z3.And(lower <= calc, calc <= upper))
``````

Did you notice an edge case? With numbers close to the upper limit, calling `from_double(normalize(point + 1))` may produce a number with an exponent of 1024 (not 1023) which will lead to a very different and invalid mantissa corresponding to a number greater or equal to 1 while `Math.random()` lies in [0, 1). This case should be checked. The exponent is extracted by right-shifting 52 bits to get rid of the mantissa, and the last 11 bits are selected by ANDing with `0x7FF` (2^11 - 1)

``````upper_exp = (upper >> 52) & 0x7FF
``````

The modified condition looks like this

``````z3.And(lower <= calc, z3.Or(calc <= upper, upper_exp == 1024))
``````

The final loop that we get

``````for point in points:
state0, state1 = xs128p(state0, state1)
calc = z3.LShR(state0, 12)

lower = from_double(normalize(point))
upper = from_double(normalize(point + 1))
upper_exp = (upper >> 52) & 0x7FF

solver.add(z3.And(lower <= calc, z3.Or(calc <= upper, upper_exp == 1024)))
``````

Now we should check for a valid solution. If it is found, the seed is extracted and the next random number can be predicted

``````if solver.check() == z3.sat:
model = solver.model()
state = {}
for d in model.decls():
state[d.name()] = model[d]
state0 = state["state0"].as_long()
state1 = state["state1"].as_long()

next = math.floor(to_double(state0) * (max - min + 1 )) + min
print(next)
``````

Finally, we can predict the unpredictable. I have set the limits to `min = 1` and `max = 100000`. The bigger the range, the fewer values are required to restore the seed because more information is preserved (a hefty chunk of bits is lost after `math.floor`). It required 10 generated values to work out the correct seed and predict the next value. It works!

As a web developer interested in cryptocurrency, I have heard about `Math.random()` being unsafe, and today I finally saw and tested a specific example proving this fact. Conclusion: please be aware that the Google random number generator is an unreliable source of entropy, especially for people familiar with bitwise operations.