JavascriptCore Math.random predictor

Lately, I decided to take a look at how Math.random work and how we could try to predict the value.

So just like anyone else, I tried to search for already existing Math.random predictors and found:

Then, I saw that the author TACIXAT said in the README:

Set the browser in main() to Chrome or Firefox. (Safari hasn’t updated yet.)

Thus, it seems like a good excercise for me to try looking into Math.random of Safari.

Webkit

Safari is browser built into the Apple’s OS, and its engine is Webkit, and the underline JS engine of Webkit is JavascriptCore (JSC).

Thankfully, LiveOverflow has published a video on how to debug Webkit / JSC on video so it’s easy for me to start from there.

Frustration attempts

Showing the result PoC is cool, but for me it’s cooler if readers can see how much frustration I had within this journey.

Readers: just shut up and show me the PoC !!! Okay here 😢

1st attempt: setting breakpoints

First, I tried tracing in the source code on how JSC call Math.random(). By reading source code I found that the function is triggered at:

Thus, I hapily setting breakpoint in gdb and wait for magic to happen:

Breakpoint in WeakRandom.h not hit

WTF? Even though I’ve setup the breakpoint but no matter how I do, the breakpoint couldn’t be hit. You can see I even change the Webkit source code and try to do some printf in the double get function but I got no luck, there’s no output being printed.

Tried changing JSC source

2nd attempt: copy-paste JSC Math.random

At this point, I tried copy-paste the WeakRandom.h to another file to check if Math.random() behave exactly like how it is implemented (or I’m looking at the wrong code?):

#include <stdint.h>
#include <cstdio>
#include <cmath>
#include <cstring>

unsigned m_seed;
uint64_t m_low;
uint64_t m_high;

uint64_t nextState(uint64_t x, uint64_t y)
    {
        x ^= x << 23;
        x ^= x >> 17;
        x ^= y ^ (y >> 26);
        return x;
    }

uint64_t advance()
{
    uint64_t x = m_low;
    uint64_t y = m_high;
    m_low = y;
    m_high = nextState(x, y);
    return m_high + m_low;
}

double get()
{
    uint64_t value = advance() & ((1ULL << 53) - 1);
    return value * (1.0 / (1ULL << 53));
}

void setSeed(unsigned seed)
{
    m_seed = seed;

    // A zero seed would cause an infinite series of zeroes.
    if (!seed)
        seed = 1;

    m_low = seed;
    m_high = seed;
    advance();
}


int main(int argc, char **argv)
{
    setSeed(1337);
    for (int i = 0; i < 10; ++i)
    {
        double k = get();
        printf("%.12lf\n", k);
    }

    return 0;
}

The above program code first call setSeed(1337) and then output 10 first random values. This is its output:

$ c++ jsc.cpp -o main
$ ./main
0.000001245188
0.445313745787
0.890626246274
0.895725289653
0.451399313092
0.137931930495
0.837726360333
0.470502978679
0.532515356442
0.079062741176

Then, I get back to the real JSC and try to setSeed(1337) before calling Math.random(). Luckily in JSC there’s a function to set the seed which called setRandomSeed(<seed>) defined at: https://github.com/WebKit/WebKit/blob/08e4dc175b88c43782fd9d8f1f3f73166a090ff8/Source/JavaScriptCore/jsc.cpp#L1837-L1846

This is the output when I run the real JSC:

./jsc
>>> setRandomSeed(1337)
undefined
>>> Math.random()
0.0000012451879418673428
>>> Math.random()
0.44531374578659877
>>> Math.random()
0.8906262462736768
>>> Math.random()
0.8957252896526161
>>> Math.random()
0.4513993130918518
>>> Math.random()
0.8723069304951169
>>> Math.random()
0.18149526315413556
>>> Math.random()
0.5404527925639941
>>> Math.random()
0.467484617730592
>>> Math.random()
0.5534826395406868

WTF? Are you seeing what I’m seeing 👀 ? In the first 5 attempts, the copy-pasted code returns exactly the same with the real JSC, whereas from the 6th attempt to 10th attempt its value is different.

3rd attempt: implement my own function into JSC

On this 3rd attempt, I was hopeless because I’m quite new to debugging low-level programming language like C/C++, prior to this I only did high-level exploiting (Java/Javascript/Python etc).

Thus, I tried putting breakpoints wherever I find it suitable, and tried calling Math.random to see if it hits my breakpoint. Heck! I even tried implementing my own function which call the function double get(), it looks something like this:

Implement my own random function into JSC

Then, I go to jsc binary and tried running my function, and what is this ?

$ ./jsc
>>> getMyRandom()
duma: 1814795562 1814795562 15223638817340558
0.6901636153078781
>>>

It is running the printf("duma: %i %ld %ld\n" ...); that I put into before 😱. Thus, this indicates that the file WeakRandom.h is a honeypot and Math.random won’t hit into the double get function 😡.

Just kidding, I think there’re some optimization, and based on some architecture it will use WeakRandom.h, while on my machine it would use another place for optimizing. So now the obstacle is clear, I’ve been looking at the wrong code so I’d need to look for the real random implementation 😳

Found real random function

Because now I know some pattern of the random function:

  • It’s using XorShift128+
  • It’s implementation should look-alike with WeakRandom.h

So by Ctrl+Shift+F on multiple keywords, and setting breakpoints, I’ve found the Math.random() is actually defined in: https://github.com/WebKit/WebKit/blob/08e4dc175b88c43782fd9d8f1f3f73166a090ff8/Source/JavaScriptCore/jit/AssemblyHelpers.cpp#L497-L547

Now I’d only need to find out why the first 5 attempts my code returns correct but from the 6th attempt it returns wrong. Thus after some error-prone, I found out that: The shift right function jit.rshift64 is arithmetic shift right, not a logical shift right like v8.

Ah ! So that’s why when the m_low and m_high is large enough (after 5 attempts), the arithmetic shift right of m_low and m_high will cause my code to return different with JSC.

Thus, now I only need to change my code from using uint64_t to int64_t:

#include <stdint.h>
#include <cstdio>
#include <cmath>
#include <cstring>

int64_t m_low;
int64_t m_high;
unsigned m_seed;

int64_t advance()
    {
        int64_t x = m_low;
        int64_t y = m_high;
        m_low = y;
        x ^= x << 23;
        x ^= x >> 17;
        x ^= y ^ (y >> 26);
        m_high = x;
        return m_high + m_low;
    }

double get()
    {
        int64_t value = advance() & ((1ULL << 53) - 1);
        return value * (1.0 / (1ULL << 53));
    }

void setSeed(unsigned seed)
{
    m_seed = seed;

    // A zero seed would cause an infinite series of zeroes.
    if (!seed)
        seed = 1;

    m_low = seed;
    m_high = seed;
    advance();
}


// solve with input m_low and m_high
int main(int argc, char ** argv) {
    setSeed(1337);
    for (int i = 0; i < 10; ++i) {
    double k = get();
    printf("%.12lf\n", k);
    }

    return 0;
}

and run:

$ c++ jsc.cpp -o main
$ ./main
0.000001245188
0.445313745787
0.890626246274
0.895725289653
0.451399313092
0.872306930495
0.181495263154
0.540452792564
0.467484617731
0.553482639541

it would be exactly the same with the value of Math.random in JSC.

Writing z3 solver

This part is boring so please just look at my github repo

Thanks for reading !!!