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.
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 b, and
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!