cracking xorshift128 with Picat ?

[albert...@yahoo.com]

Here is an article that can predict Java math.random after 3 math.random()

Search space is much bigger than SEND + MORE = MONEY, can Picat do this ?

https://blog.securityevaluators.com/hacking-the-javascript-lottery-80cc437e3b7f?gi=4413eba2960a

[albert...@yahoo.com]

Perhaps the problem is too hard for Picat. This is a simpler version

Recover initial state with last bit of 128 xorshift128+ calls:
You still only have 128 bits information, but no need to worry about carry
Here is the equations of first 2 calls

state0 = {x, y}
state0 last bit
= last_bit(x + y) = last_bit(x ^ y) -- no carry for last bit
= x0 ^ y0

After 1 xorshift128+ :
state1 = {y, (x ^ x<<23) ^ y ^ ((x ^ x<<23)>>18) ^ (y>>5)}

state1 last bit
= last_bit(y ^ (x ^ x<<23) ^ y ^ ((x ^ x<<23)>>18) ^ (y>>5))
= last_bit(x ^ (x>>18) ^ (y>>5))
= x0 ^ x18 ^ y5

...

--> 128 equations, 128 unknowns (bits of {x, y})
--> each equation cut down possible states by 50% (last bit is 0 or 1)
--> one unique {x, y} remain after solving all 128 equations

[albert...@yahoo.com]

Turns out, the "simpler" 128 last bits is actually much harder.

Although each equation reduce the search space in half, it does not help at all
We just don't know which half is correct, so it provide no real shortcut.

It is the same as saying each bit is either 0 or 1, which give no useful information.

--> z3 solver is unable to solve xorshift state from 128 last bits.

With 3 math.random(), however, z3 solved it in less than half second.

[albert...@yahoo.com]

the "simpler" 128 last bits might not have an unique solution.
After simplifying the 128 equations, we might have less than 128 equations left.

[Neng-Fa Zhou]

While Picat supports arithmetic on big integers, values of integer domain variables are limited to the range -2^56-1 .. 2^56-1. You can represent a 128-bit vector by using an array of Boolean variables. The following example illustrates how to define shift and xor constraints on bit vectors:

import sat.

main =>

    X = new_array(128),

    Y = new_array(128),

    Z = new_array(128),

    X :: 0..1,

    Y :: 0..1,

    Z :: 0..1,

    shift_left_bv(X,Y),

    xor_bv(X,Y,Z),

    solve({X,Y,Z}),

    println(X),

    println(Y),

    println(Z).

% Y is the result of shifting X to left by 1

shift_left_bv(X,Y) =>

    Y[1] = 0,

    foreach (I in 2..128)

        Y[I] #= X[I-1]

    end.

% Z = xor(X,Y)

xor_bv(X,Y,Z) =>

    foreach (I in 1..128)

        Z[I] #= X[I] #^ Y[I]

    end.

I believe that the sat module is better than the cp and mip modules for this problem. 

I hope this can serve as a good start.

Cheers,

Neng-Fa

[Hakan Kjellerstrand]

I've written a kind of proof-of-concept for implementing bitwise operation using the cp module, mostly since it's quite easy to convert to/from arrays and values using the constraint modules. However, as Neng-Fa mentioned, the cp (and sat) module don't support the full range of 64 bit operations using this approach (max 56 bits).

Nevertheless, here's the (very) experimental program including some small tests (which may or may not be of some use):

       http://hakank.org/picat/bitwise.pi

There are surely a lot of bugs in it, and I'm not even sure if I will publish it on my Picat page. So, now you have been warned....

/Hakan

[albert...@yahoo.com]

Correction to my previous post, 128 xorshift128+ last bit recovered seed is UNIQUE.

Since last bit is a LSFR of degree 128, here is the proof:

https://marc.info/?l=lua-l&m=152458604111833&w=2