This is one of the hardest CTF I’ve been in. My team did really well to qualify for the finals in Sweden, and I wish them all the best as I will not be joining them.

The Gambler

This was a DotNet binary, we so could use DNSpy to inspect the full source code

In the main file, we had to key in a value, which was used as a seed for creating a random number generator.

This random number generator is then used to generate a whole bunch of different numbers, specifically int a, int b, and int c.

The generator is then passed into Program.play(), which looks like this

Play generates random numbers, and takes one bit from a location specified by mask, which is a list of 208 integers, and adds it to num

Looking at the main function, num must be equals to 95.

The program then validates a, b and c in this function

We can derive c and b pretty easily, and a looks pretty crazy to solve. Fortunately, my team mate knew of an approach called Z3 https://github.com/Z3Prover/z3 which essentially takes in a bunch of constrains, and gives the value that meets those constrains.

With that, a = 793646200, b = 254483726 and c = 973340155

Using these values, we brute force the seed value. Crazy huh, but possible. It gives us the seed value of 866551920

We now enter the seed to the program, and the flag value is actually in the Program.play() function. Instead of adding the 1s and 0s to num, we extract those values out, and convert them from binary to ASCII

We edit the method to look something like this, and run it with 866551920 as the input

Convert the binary to ASCII to get the flag!