> I couldn’t believe that z3 was the best one can do
It probably never is, but if you don't care about a nice solution or don't care about anything past "is it possible?", then z3 and smt2 are amazing. You often don't even need to understand the whole problem. "take constraints, give solution" works great in those situations.
looking at the CVE report itself, Math.random() not being crypto-level seems to be known? - and vulnerability comes from Node.js using it for some crypto purpose
so OP simply did a good exercise for himself recreating exact weakness of it
I have recently replaced Lua's random for this implemetation
https://nullonerror.org/2025/08/02/replacing-lua-s-math-rand...
Xorshift128+ is not a cryptographic rng though, so at least this isn't a cryptographic attack...
Should programming languages use cryptographic rngs like a ChaCha20 based one in their standard libraries to stop accidental use of non cryptographic rngs for cryptographic purposes? But that comes at the cost of speed
If you represent the state as a 128-long vector of GF(2) elements, you can model the state transition function as a matrix multiplication.
This allows you to describe any output bit (at any offset in the output stream) as a function of the 128 initial state elements.
Treating the initial state vector as 128 unknown variables, you can solve for them (via gaussian elimination) with any 128 bits from the output stream, so long as you know their offsets in the output sequence.
Although, depending on what those offsets are there's a ~50% chance there's no unique solution, in which case you may need a few more bits. For the case of two consecutive 64-bit outputs, you get a unique solution.
For 128 samples, the gaussian elimination can be done in 2^21 steps, or only 2^14 steps if you can put a whole bit-vector in one register (which you can!)
If the offsets are known in advance, you can pre-compute the gaussian elimination work and end up with a constant matrix that, if multiplied by the leaked bits, obtains the initial state vector.