Beating the odds with Z3

#javascript, #python, #security, #z3 -

As you should know, Node.JS's Math.random() is not cryptographically random and, as such, you can in theory predict future values if you have previous values.

While there have been articles aimed at cracking Math.random() before, they are aimed at browsers, and have not been tried on real-world scenarios. Many websites use Node.JS for their backend, and few suspect Math.random() of, well, not being random.

The victim

We are looking at a website proudly developed in TypeScript, which provides a point system with a few gambling games to limit inflation. The one where you can win the most in one move is the roulette, where you pick a number between 1 and 10 and if you win, you get 10x what you put in. The house doesn't actually have an edge here, but since the minimal bet is pretty expensive, most just empty their balance again and again.


As it turns out, the website is open source, so we don't have to imagine what the winning algorithm looks like. There are only a few places where Math.random() is called:

Let's start with /roll.


RollPlugin.TICK_MS = Array.from({length: 3000 / 150})
    .map((_, i) => (1 + i) * 150)
        3048, 3180, 3307, 3440, 3576, 3723, 3881, 4040, 4209,
        4398, 4603, 4834, 5084, 5372, 5744, 6413, 7621

this.currentGame.ballPosition = Math.floor(Math.random() * 10);

// Initialize board
this.updateGameMessage();'roll', { state: true });
await waitTimeout(100);

// The timeout will increase randomly until reaching maxTimeout
for (const tickMs of RollPlugin.TICK_MS) {
    setTimeout(() => {
        // Move ball to next slot
        this.currentGame!.ballPosition = (++this.currentGame!.ballPosition) % 10;

        // Redraw game
    }, tickMs);

// Wait for latest tick to complete
await waitTimeout(RollPlugin.TICK_MS[RollPlugin.TICK_MS.length - 1]);

This displays a fancy rolling animation, but we're only interested in the result. The only non-deterministic part here is the initial position of the ball: all this code can be reduced to Math.floor(Math.random() * 10) + 37) % 10 (37 being the number of slot updates).

This sounds very promising, but in order to get the seed of Math.random(), we'll need a lot more bits than that.


This command generates a number between 0 and 999, and the player that chose the closest number gets the winnings. While this gives you more bits, it requires other people to be willing to play, and is still not enough to crack Math.random().

File uploading

Why would file upload require random numbers, you ask? Maybe the incriminating line will enlighten you:

const filePath = 'uploads/'
    + date.toISOString().substr(0, 19).replace(/(-|T)/g, '/').replace(/:/g, '-')
    + '-' + Math.floor(1000000000 * Math.random()) + '.' + extension;

This sounds really promising. This gives us 23 (out of 52) bits of data, which should be enough to crack the seed with enough inputs.

Building the hack

We're going to base our work off of this XorShift128+ cracker, which is unfortunately in Python 2, and only targets browsers.

Node.JS's random number generator is the same as Chrome's, so after a quick 2to3 conversion, it should be usable as is. And it is! However, we only have a small portion of the available bits, so we'll have to adapt it a bit.

We'll simply replace the original simulation of ToDouble():

impl = Implies(condition, LShR(sym_state0, 12) == generated)

With one that has to put in more effort:

# We don't have the 12 bits of the mantissa, and we don't have the last 29 bits of the fraction component.
SKYMASK = MASK & (MASK << 29) & (MASK >> 12)

impl = Implies(condition, LShR(sym_state0, 12) & SKYMASK == generated)

Then, we can finally test on a local build of the chat system. After uploading 6 files, and using their filenames, we can successfully crack Math.random(). From there, we are able to guess future filenames, and, excitingly, future winning numbers for the roulette game.

Testing it on the real website

Things don't always go as smooth as expected. It turns out our method doesn't work at all on the remote website - the generated numbers are completely off, and sometimes the cracker doesn't even find the seed.

It turns out, Node.JS's number generator changed between versions - and the one we worked on locally is not the same as the server. Whoops. At the time, Node.JS v10 was still in LTS phase, so I chose to update my code to support it. It is also the same as v11's, so as long as the owned isn't running some obscure out-of-date version, we should cover all available versions.

Take a look at the source code. It seems that v10 uses both state variables, while v12 only uses one. I'm not a cryptographer, but it certainly makes cracking v12 faster with our approach. Let's update our code for v10:

impl = Implies(condition, (sym_state0 + sym_state1) & SKYMASK == generated)

It took us a few second to crack a seed from v12's PRNG, but this will take a few minutes on v10. But since we only need to crack the seed once to be able to simulate Math.random() many, many times, we don't have to look for optimizations - let's try it for real!


Wow, how lucky, we won on our first try! Try not to win every time from now on ;)


This should be obvious, but don't use Math.random() for anything that you don't want the user to guess. Use Node.JS's crypto module, which generates cryptographically secure bytes.

You can read the full source code of the exploit in this gist.