# Calculation of pseudo-random numbers generator state – on the example of Math. random() from Firefox

In this text:

• We will get to know how pseudo-random number generators operate
• We will learn how the XorShift128Plus algorithm, which is the basis of pseudo-random number generators in all the most popular browsers (Firefox, Chrome, Edge), works.
• We will get to know the Z3Prover tool, thanks to which we will be able to calculate the state of the generator on the basis of three known numbers.

In real cases, knowing the status of a random number generator may allow, for example, to guess subsequent session tokens.

### Inspiration

The direct inspiration for writing this article was from a random4 task with a very interesting set of challenges called return true to win puzzles. Each task contains a short piece of code with a defined function that returns a Boolean value. The task of the solver is to pass such parameters to the function so that it returns “true”. This is not always easy. Usually, it requires knowledge of the nuances of the ECMAScript standard or, going even further, the specific features of JavaScript in browsers. I recommend that you try to face these tasks because they allow you to learn more about the most relevant programming language of the web world. But let’s go back to random4. The code was as follows:

As we can see, a random value generated by Math.random() is assigned to the rand variable. In the next step, we have to call the random4 function with such a parameter that it returns true. In other words, our parameter must be equal to the previous value of Math.random()… Once all the ideas failed and it seemed that no specific feature of Javascript (or browser error) was at stake here, the task came down to another problem: You have to determine the state of the pseudo-random generator!

How do pseudo-random number generators work

Apart from cryptographic applications, where a lot of attention is paid to the fact that random numbers are, in fact, random, in other areas we usually deal with pseudo-random numbers. The methods of generating pseudo-random numbers are different – depending on the algorithm we use – but basically come down to a few steps:

1. We pass the seed to the generator of pseudo-random numbers. This way, the state of the generator is determined by the seed.
2. The generator performs arithmetic operations, on the basis of which it calculates the new state value.
3. On the basis of the generator state, a new pseudo-random value is calculated.

A characteristic feature of pseudo-random number generators is that when the same seed is used, one will receive the exact same sequence of numbers.

Repeatability of pseudo-random generators in the same state is a desirable feature because it allows to re-create the workflow of the program, e.g., in case of an error.

Pseudo-random number generators in web browsers

All the most popular web browsers (i.e. Chrome, Firefox, and Edge) use the same algorithm to generate pseudo-random numbers: XorShift128+. In the next part of the text, however, I will refer only to the implementation from Firefox, due to the fact that in my opinion, it is the most readable.

So let’s see the appropriate fragment of the code from the Gecko engine:

As you can see in the code above, the state of the XorShift128+ generator consists of two 64-bit numbers. The next pseudo-random number is calculated by converting the new value of one of the state numbers (which can be achieved by several bit shifts and XOR operations), and then adding two state numbers to each other.

Insightful readers will notice that XorShift128+ generates 64-bit integers, while Math.random() returns a floating point number in the [0, 1) range. So how is this uint64_t converted to double? This question is answered by another function from the sources: nextDouble.

The code boils down to the fact that from the generated 64-bit value 53 last bits are taken, which are then divided by 253. In this way we have a guarantee that we will get a number from the range [0,1). It did not make sense to divide more bits because the double data type is not able to hold more precision anyway.

While all the most popular browsers use the XorShift128+ algorithm, each of them has its own way to convert unit64_t to double. Therefore, the code we will write for Firefox will not be compatible with other browsers, although it will require only minor corrections.

As a simple exercise, which is the basis for our further operations, let’s rewrite the code generating pseudo-random numbers to Python.

The above code is practically a literal translation of the C++ code into Python. The XorShift128PlusFirefox class in the constructor has two values defining the state of the generator; next() function generates another 64-bit integer, and next_double() generates another floating point-type number in the range [0,1).

In the code of the next_double() function we see the use of Python function float(). Only one floating-point type is defined in Python. It corresponds to the double type known from C/C++, but is called float.

An example of using XorShift128PlusFirefox class can be seen in Picture nr 1. Two pseudo-random numbers were generated based on the given state.

### Z3Prover tool

We already know how the random number generator works in Firefox; we even wrote its implementation in Python. We are slowly approaching the essence of this text, i.e., the determination of the generator’s state based on the knowledge of a few numbers. But let’s get to know the tool we can use to achieve this: Z3Prover. Z3Prover is a SMT solver class tool – it allows for automatic proving of theorems. In short, the tool accepts as an input a set of logical conditions (which may consist of arithmetic and bit operations, among others), and then tries to calculate whether there is input data for which these conditions are met. A few examples we will see below.

To start using Z3Prover, you must first compile its sources or download binary files. I recommend using the second option. After unpacking the binary files, run Python in the same directory in which they were unpacked and call the command:

#### Example 1

We start with a trivial example: We define two symbols, which are Boolean variables, and check when their conjunction will be equal to the ”ture”. Of course, z3 returns to us the answer that the equation is fulfilled when both variables are true.

#### Example 2

In z3 we can also operate on numbers. In this example, we have defined two integers, and then we try to solve the equation: 4*a+7*b=9 with the assumption that a<5 and b>a.

#### Example 3

Another type of data we learn is BitVec – it is an integer with the number of bits we have set. Then we try to solve an equation in which we combine both bit and arithmetic operators.

#### Example 4

Z3 can also be used to simplify certain symbolic expressions instead of calculating them.

### “Cracking” number generator

It’s time to write a “cracker” for the random number generator, which works well for a few elements:

• Using z3 we will save a symbolic figure of three consecutive random numbers generated by the XorShift128+ algorithm,
• Three consecutive floating point numbers generated by Math.random() will be changed to integers,
• Based on the above data, we will generate three equations with variables s0 and s1, the solution of which will allow us to determine the state of the generator of pseudo-random numbers.

We have the Cracker class, in which we define the variables s0 and s1 containing the generator state and the state variable containing the same, but in the form of an array. Field solver stores the Solver class of z3, which takes the equations to solve. To known field we will pass known values of pseudo-random numbers, which we will generate using Math.random() method from Firefox.

So let’s implement the next() generator method:

The next() method looks exactly the same as in the original Firefox code. The only difference is the use of z3.LShR instead of operator >>. This is due to the fact that in z3 the operator >> is an arithmetic bit shift to the right. Consequently, if the character bit is 1, it will be retained. LShR is a logical right shift that ensures that the sign bit will always be set to 0. Let’s see, out of curiosity, what random numbers look like in a symbolic form after the first two calls to the next() function (Picture nr 6).

After the first next() call, the symbolic form is almost exactly the same as we saw in the code of this method. After the second call, the situation starts to get more complicated; we can see a more complicated description of the number, although the only variables to which it refers are s0 and s1.

Now we will generate three random numbers in Firefox:

• The first random number will be equal to the symbolic number form after the first call to next(),
• The second random number will be equal to the form of the symbolic number after the second call to next(),
• The third random number will be equal to the symbolic number form after the third call to next().

We have one important problem to solve: next() function returns a number in the form of uint64_t, and from Firefox we will get floating-point numbers. We will therefore have to convert it back into integers. However, this will not be difficult. As we remember, Firefox pulled out of the 64-bit number its 53 last bits, and then divided it by 253. So we will simply reverse this process. The number we get from Firefox will be multiplied by 253, and from the number we have in a symbolic form, we will extract only 53 bits. As a result, we get two 53-bit integers to compare. Let’s look at the code of the “cracker” itself:

In the above code we iterate after known values of random numbers. Multiply the values of the double type by 253 and compare them with the 53 last bits of the number generated by calling next(). Such equations are thrown into the solver with z3. Then we call the solver. check() method solving the equations given by us. If the method returns the value of z3. sat, it means that the equation has been solved. The calculated values can be extracted by referring to the model. Finally, the function returns s0 and s1, which are the state of the random number generator.

So I generated three consecutive random numbers in Firefox:

• 0.8629073810129263,
• 0.19187870241845773,
• 0.07371019627869657.

Let’s see if our Cracker will be able to determine the state of the generator (Picture nr 7)

Success! Thanks to z3 we reconstructed the generator’s state. Now let’s try to use this state as an argument to the generator we wrote earlier (class XorShift128PlusFirefox) and see if it really will generate the same numbers (Picture nr 8).

We got the same sequence that Firefox generated, which shows that our Python implementation of breaking and generating further pseudo-random numbers is correct.

### Solving problem from random4 task

The problem with the random4 task mentioned at the beginning remains to be solved. Due to the specificity of that task, we could generate as many random numbers as we wanted, but we had to determine what number was generated before our Math.random() calls. It turns out that with the current code the solution to such a problem is easy: After calculating the generator state, we will not call the next() method (it causes the calculation of a new state), but we will generate a number on the basis of the state that we know.

Below is the full code of the solution – the changes described in the paragraph above are reflected in the current_double() method. In addition, a code has been added to the Python script to pass an argument containing three comma-separated numbers generated in Math.random().

As a final test of the correctness of the solution, I will generate four more pseudo-random numbers in Firefox, pass the last three to the cracker, and see if the first one will be generated (Picture nr 9).