4 ms·

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'v

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.

tubby12345 5y ago
How do you pick how many constants and they're relationships?
- Someone 5y ago
  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.
  - ChrisLomont 5y ago
    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.
    - tmoertel 5y ago
      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.)
      - ChrisLomont 5y ago
        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.
        ChrisLomont 5y ago
        Here's a simple example finding a hidden seed. It takes around 1, 2, or 3 values in a row and finds the seed. You can adapt this to all sorts of breaking problems, but for some you'll have to learn more about SATs and be careful how you code things. Note the simple PRNG I chose doesn't reveal all the state, yet over time you can deduce all of it. // 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();
    - tubby12345 5y ago
      Oh gotcha. I thought you meant that you were some how modeling the prng using some reduced set of constraints.
  - ChrisLomont 5y ago
    Also, to break unknown/unseen PRNG, model a few popular classes of PRNG, a few common reductions (so for cards the naive val%52 and better rejection sampling), then solve across the states till you get one. Then watch a few more outputs, check that you guessed the source and reduction, and now you've cracked that too. I doubt any poker site uses anything other than a crypto rand for deals because the technique I just explained would eat them alive. They can use fast and insecure PRNG for doing Monte Carlo hand evaluation, though, since that doesn't give you any advantage.
    - downandout 5y ago
      So building on this...many physical casinos use a manual shuffle, especially at higher limits, as bigger players tend to distrust shuffle machines. Even some online casinos with live dealers will shuffle the previous shoe on camera, manually. Since getting a truly random shuffle would take too long, this is a poor method of getting random results. Would it be possible to, at least to some degree, predict the order of the cards using one of these models, given the order of the cards prior to shuffling? I'm thinking something along the lines of being able to say that the odds of a given card being the next one are higher than they should be, not outright predicting the full order of the cards.
      - ChrisLomont 5y ago
        If I recall, something like 7 hand shuffles becomes indistinguishable from random. I'd guess a pro could get this level of mixing in a few shuffles
        downandout 5y ago
        Yeah, but that's 7 shuffles of a single deck. Most casinos use 6 or 8 decks. They are certainly not shuffling 42+ times.
        ChrisLomont 5y ago
        Shuffles don't multiply like that. Mixing is an exponential process. It's why mixing a little paint or a lot of paint isn't multiplicatively more work.
shaicoleman 5y ago
I don't think this will work on PCG. "pcg32, which has state-space size of 2^127 (2^64 period × 2^63 streams) and produces 32-bit outputs." https://www.pcg-random.org/predictability.html https://www.pcg-random.org/predictability.html That said, The PCG author does not recommend to use it for cryptography. "Although it is less trivial to predict than many mainstream generators, that does not mean it should be considered crypographically secure. Exactly how hard it is to break different members of the PCG family is unknown at this time." https://www.pcg-random.org/other-rngs.html https://www.pcg-random.org/other-rngs.html
- ChrisLomont 5y ago
  It trivially works on PCG. The problem is a boolean satisfiability problem, and these are solvable on far harder instances.

tubby12345 5y ago

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

Someone 5y ago
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.
- ChrisLomont 5y ago
  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.
  - tmoertel 5y ago
    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.)
    - ChrisLomont 5y ago
      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.
      - ChrisLomont 5y ago
        Here's a simple example finding a hidden seed. It takes around 1, 2, or 3 values in a row and finds the seed. You can adapt this to all sorts of breaking problems, but for some you'll have to learn more about SATs and be careful how you code things. Note the simple PRNG I chose doesn't reveal all the state, yet over time you can deduce all of it. // 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();
  - tubby12345 5y ago
    Oh gotcha. I thought you meant that you were some how modeling the prng using some reduced set of constraints.
- ChrisLomont 5y ago
  Also, to break unknown/unseen PRNG, model a few popular classes of PRNG, a few common reductions (so for cards the naive val%52 and better rejection sampling), then solve across the states till you get one. Then watch a few more outputs, check that you guessed the source and reduction, and now you've cracked that too. I doubt any poker site uses anything other than a crypto rand for deals because the technique I just explained would eat them alive. They can use fast and insecure PRNG for doing Monte Carlo hand evaluation, though, since that doesn't give you any advantage.
  - downandout 5y ago
    So building on this...many physical casinos use a manual shuffle, especially at higher limits, as bigger players tend to distrust shuffle machines. Even some online casinos with live dealers will shuffle the previous shoe on camera, manually. Since getting a truly random shuffle would take too long, this is a poor method of getting random results. Would it be possible to, at least to some degree, predict the order of the cards using one of these models, given the order of the cards prior to shuffling? I'm thinking something along the lines of being able to say that the odds of a given card being the next one are higher than they should be, not outright predicting the full order of the cards.
    - ChrisLomont 5y ago
      If I recall, something like 7 hand shuffles becomes indistinguishable from random. I'd guess a pro could get this level of mixing in a few shuffles
      - downandout 5y ago
        Yeah, but that's 7 shuffles of a single deck. Most casinos use 6 or 8 decks. They are certainly not shuffling 42+ times.
        ChrisLomont 5y ago
        Shuffles don't multiply like that. Mixing is an exponential process. It's why mixing a little paint or a lot of paint isn't multiplicatively more work.

shaicoleman 5y ago

I don't think this will work on PCG. "pcg32, which has state-space size of 2^127 (2^64 period × 2^63 streams) and produces 32-bit outputs." https://www.pcg-random.org/predictability.html https://www.pcg-random.org/predictability.html That said, The PCG author does not recommend to use it for cryptography. "Although it is less trivial to predict than many mainstream generators, that does not mean it should be considered crypographically secure. Exactly how hard it is to break different members of the PCG family is unknown at this time." https://www.pcg-random.org/other-rngs.html https://www.pcg-random.org/other-rngs.html

ChrisLomont 5y ago
It trivially works on PCG. The problem is a boolean satisfiability problem, and these are solvable on far harder instances.