# Table of Contents

# Challenge

This is it. The last group test of the year. Dr. J patched his prng again so numbers won't repeat, so I guess Leaf won't get to know the group test pairs ahead of time... oh WEYL. Who knew middle square could make such a good prng?

`nc shell.2019.nactf.com 31382`

We're also given the source of the running application:

```
#include <stdio.h>
#include <stdint.h>
#include <sodium.h>
#include <stdbool.h>
#include <string.h>
#define NUM_CORRECT 10
uint64_t x = 0, w = 0, s = 0xb5ad4eceda1ce2a9;
uint32_t nextRand() {
w += s;
x = x*x + w;
x = (x>>32) | (x<<32);
return x % (1UL<<32);
}
void init_seed() {
uint64_t r1 = (uint64_t) randombytes_random();
uint64_t r2 = (uint64_t) randombytes_random();
x = (r1 << 32) + r2;
r1 = (uint64_t) randombytes_random();
r2 = (uint64_t) randombytes_random();
w = (r1 << 32) + r2;
}
void print_flag() {
FILE *f = fopen("flag.txt", "r");
char flag[100];
fgets(flag, sizeof(flag), f);
printf("%s\n", flag);
fflush( stdout );
return;
}
const char *messages[NUM_CORRECT] =
{ "\nHmm... lucky guess...\n",
"\nWow, that was coincidental!\n",
"\nWhat? How did you guess that?\n",
"\nThat's right, but you won't be able to guess right again!\n> ",
"\nStrangely, that's correct...\n"
};
int main() {
setvbuf(stdout, NULL, _IONBF, 0);
init_seed();
printf("\nWelcome to Dr. J's Random Number Generator v3! We have received reports of "
"a vulnerability involving repetition of output. This vulnerability has since been patched, "
"and Dr. J's RNG is now 100%% secure. \n"
"[r] Print a new random number \n"
"[g] Guess the next ten random numbers and receive the flag! \n"
"[q] Quit \n\n");
char line[100];
while (true) {
printf("> ");
fgets (line, sizeof(line), stdin);
line[strcspn(line, "\n")] = 0;
if (!strcmp("r", line)) {
uint64_t r = nextRand();
printf("%lu\n", r);
}
if (!strcmp("g", line)) {
printf("\nGuess the next ten random numbers for a flag! "
"The chance of guessing all ten numbers correctly is 1/(2*10^96). I hope you're lucky! "
"\nEnter Guess 1:\n> ");
for (int i = 0; i < NUM_CORRECT; i++) {
uint64_t guess = 0;
fgets (line, sizeof(line), stdin);
sscanf(line, "%lu", &guess);
if (guess == nextRand()) {
int m = randombytes_uniform(5);
printf("%s", messages[m]);
if (i < NUM_CORRECT-1) {
printf("Enter Guess %d:\n> ", i+2);
}
else {
printf("What sorcery is this? That's impossible! I guess you deserve this flag:\n");
print_flag();
break;
}
}
else {
printf("That's incorrect. Get out of here!\n");
break;
}
}
break;
}
if (!strcmp("q", line)) {
printf("\nGoodbye!\n");
break;
}
}
return 0;
}
```

# Solution

This is solvable mathematically as the lower 32 bits of `x`

are given after each iteration. However, I chose to use `z3`

instead of solving this by hand.

We only need to implement the `nextRand()`

function in python because the internal state of the PRNG is only changed here:

```
so = Solver()
x = BitVec('x', 64)
w = BitVec('w', 64)
def nextRand():
global x, w
w += 0xb5ad4eceda1ce2a9
x = x * x + w
x = LShR(x, 32) | (x << 32) # x = b, a
return Extract(31, 0, URem(x, 1 << 32))
```

An important thing to note with `z3`

is the python right shift operator (`>>`

) acts as if the bit vector is signed. To treat the bit vector as unsigned, you need to use `LShR`

. After implementing this function, we simply need to constrain the output of the function with `z3`

:

```
rand = [
3482268774,
3733492975,
1914513130,
577823218,
3863315458,
820480830,
4172394928,
1278770144,
3099743734,
3093365285
]
generated = [BitVecVal(x, 32) for x in rand]
for k in generated:
so.add(nextRand() == k)
```

And finally, we can print out the produced model:

```
if so.check() == sat:
print(so.model())
else:
print('unsat')
```

In testing, I found that this would not return the same initial `x`

and `w`

values, but the values produced by the PRNG were correct for at least the next 20 values. After we find the values of `x`

and `w`

, we can use those in the given source in the `init_seed()`

function to get the next 10 numbers.

### Full Script

```
from z3 import *
so = Solver()
x = BitVec('x', 64)
w = BitVec('w', 64)
def nextRand():
global x, w
w += 0xb5ad4eceda1ce2a9
x = x * x + w
x = LShR(x, 32) | (x << 32) # x = b, a
return Extract(31, 0, URem(x, 1 << 32))
rand = [
3482268774,
3733492975,
1914513130,
577823218,
3863315458,
820480830,
4172394928,
1278770144,
3099743734,
3093365285
]
generated = [BitVecVal(x, 32) for x in rand]
for k in generated:
so.add(nextRand() == k)
if so.check() == sat:
print(so.model())
else:
print('unsat')
```