The underlying problem seems to be that the PRNG they are emulating is giving away its internal state. I wouldn‘t expect this to work for PCG, for example.

It would also work for PCG. You're simply modeling the PRNG and learning the internal state from outputs.

It's even easier using Z3 or your own SAT solver. I've broken pretty much all non-crypto PRNGS using Z3, and it's trivial to do so. You simply model the PRNG in Z3, with unknown constants, plug in a few values from the output (or even parts of output, or even non-consecutives ones, anything you derive from them, etc - just model how the inputs formed), and ask Z3 to solve for the internal state. It works every time.

How do you pick how many constants and they're relationships?

I think that’s the “You simply model the PRNG in Z3” part.

Whether that’s simple depends is debatable, but for example would be if somebody open-sourced the server-side of their poker dealing site.

It's quite simple. Z3 supports every basic integer option out of the box. You literally write the same code as the original prng. Instead of a uint32, or uint64, or float32, etc., you use the Z3 equivalent type. That's it. You define the state as unknown, but same Z3 type as in C or JavaScript. Then you run the function once. Set it to the output you see, repeat a few observed outputs, then tell Z3 to solve for the original unknown state.

It's absolutely trivial, taking a few lines of code.

I've broken all sorts of code using similar tools.

Do you have a worked example of finding a PRNG's internal state that you could share? (Most people are unfamiliar with Z3 and other SMT solvers. Seeing a relevant worked example would be very illustrative.)

Yeah, I was considering posting one. I've lately switched to Z3 under C# since it's so easy to do things... If I get around to it tonight I'll make a post.

  // Code to demonstrate finding the hidden seed of a PRNG with Z3
  // Chris Lomont Oct 2021
  // Answering this comment on Hacker News https://news.ycombinator.com/item?id=28886698

  // Start by getting Z3, a theorem prover from Microsoft, via nuget. See https://github.com/Z3Prover/z3
  using Microsoft.Z3;
  using System;

  // get a solution
  ulong Solution(Context ctx, BoolExpr f, BitVecExpr seed)
  {
    Solver s = ctx.MkSolver();
    s.Assert(f); // assert constraint into solver
    if (s.Check() == Status.SATISFIABLE)
    {
        var m = s.Model;
        Expr e = m.Evaluate(seed);
        return ulong.Parse(e.ToString());
    }
    else
        throw new Exception("Fatal error");

  }

  // simple PRNG, used in many old C libs
  UInt32 next = 0x1234;
  UInt32 rand()
  {
    next = next \* 214013 + 2531011;
    return (next / 65536) % 32768;
  }

  void Test()
  {
    var R = new Random();
    next = (uint)R.Next();
    var start = next;
    Console.WriteLine($"Starting seed {next:X8}");

    using (var ctx = new Context())
    {
        // 32 bit vector type
        Sort bv_type = ctx.MkBitVecSort(32);

        // unknown seed - we will solve for this
        BitVecExpr seed = ctx.MkBVConst("seed", 32);

        // constants used in the PRNG
        BitVecExpr c214 = (BitVecNum)ctx.MkNumeral("214013", bv_type);
        BitVecExpr c253 = (BitVecNum)ctx.MkNumeral("2531011", bv_type);
        BitVecExpr c65536 = (BitVecNum)ctx.MkNumeral("65536", bv_type);
        BitVecExpr c32768 = (BitVecNum)ctx.MkNumeral("32768", bv_type);

        // track the boolean to satisfy
        BoolExpr be = ctx.MkTrue();

        var next = seed; // start here
        int pass = 0;
        while(true)
        {
            ++pass;
            if (pass > 10) break;
            // the sampled random
            var r = rand();
            BitVecExpr rndBV = (BitVecNum)ctx.MkNumeral(r, bv_type);

            // make this code using Z3 variables
            //next = next * 214013 + 2531011;
            //return (next / 65536) % 32768;
            next = ctx.MkBVAdd(ctx.MkBVMul(next, c214), c253);
            var ret = ctx.MkBVURem(ctx.MkBVUDiv(next, c65536), c32768);

            // add a constraint boolean for this "Z3 ret = returned value"
            be = ctx.MkAnd(be, ctx.MkEq(ret, rndBV));

            // get solution
            var val = Solution(ctx, be, seed);
            // todo - can check unique by adding "seed != soln" to the boolean and checking
            Console.WriteLine($"{pass} : 0x{val:X8}");
            if (val == start)
                break; // done - can also break when shown unique
        }
    }
  }
  Test();