Welcome to my latest adventure! Today, I’ll be taking you through the process of solving a crackme challenge that had me stumped for hours. The challenge was a Windows executable, and the goal was simple: find the correct key to unlock the program. But as with all CTF challenges, the solution was anything but simple.

The first thing I did was load the executable into IDA, to take a closer look at the program’s inner workings. As I began to analyze the code, I quickly realized that simply entering any key wouldn’t work. The program had a specific key length in mind and would reject any input that didn’t match that length. So, without further ado, let’s dive into it!

The program was looking for a specific length of 32 characters. Any input shorter or longer than that would be rejected, and the program would give us message “Wrong Length!” and exit.

With the length check out of the way, I moved on to the next step in the program’s logic. The next check was to read the first 11 characters of the input and compare it to a hardcoded string “Securinets{". If the input matched the hardcoded string, the program would continue to the next check, if not, the program would exit.

With the first 11 characters of the key successfully unlocked, I moved on to the next step of the program’s logic. The next 9 characters of the input were read and the program performed a check to ensure that these characters were digits from 0 to 9. If any of the characters failed this check, the program would exit.

1
2
3
4
5
6

from string import printable
for i in printable:
	if ord(i) - 48 > 9:
		continue
	else:
		print(i) # it will print digits from 0 to 9 and some other characters

The next step was to pass these 9 characters to a function called fnv_1a_32() which is a hash function that returns an integer. This integer was then compared to a hardcoded value of -105269403. If the two values matched, the program would proceed to the next step, if not, it would exit.

The function starts by initializing a variable called **v3** with the value of **-2128831035**. It then enters a loop that iterates through each character of the input. Within the loop, it performs a bitwise XOR operation between v3 and the ASCII value of the current character. The result of this operation is then multiplied by the value of 16777619 and stored back into v3. This process continues until the loop has iterated through all the characters of the input. The final value of v3 is then returned by the function.

 
One of the key steps in solving this challenge was finding the correct 9-character input that only contains digits and satisfies the equation produced by the fnv_1a_32() function.

Using Z3 was a much more efficient approach, and it allowed me to find the correct input in a fraction of the time it would have taken using a brute-force approach.

To begin solving this challenge using Z3, the first step is to define the 9-digit input as a BitVector and add the constraints that the input must satisfy in binary.

1
2
3
4
5
6
7
8
9

from z3 import *

# z3.Solver() designed to determine whether a set of constraints has a solution or not, and if it does, it can return one or more solutions.
# Optimize() designed to find the best solution among a set of constraints
solver = Optimize()
# we need to genereate a 9 character
password = [BitVec("c_%i" % i ,32)  for i in range(9)]
for char in password: # character constrains
	solver.add(And(char - 48 >= 0, char - 48 <= 9))

In this code, we are defining the variable v3 as a BitVector of size 32. This variable v3 will be used to represent the result of the fnv_1a_32(). We also define a variable a with the value of 16777619, which is a constant used in the fnv_1a_32() function. Next, we are adding a constraint to the Z3 solver that represents the logic in the if condition

1
2
3

v3 = BitVec("v3", 32)
a = 16777619
solver.add(v3 == -105269403)

The simulate the loop in the function fnv_1a_32() but in z3

1
2
3
4

v3 = -2128831035
for i in password:
	v3 = 16777619 * (i ^ v3)
solver.add(v3 == -105269403)

With all the pieces in place, it was finally time to put my Z3 script to the test.

1
2
3
4
5
6
7

if solver.check() == sat:
    print("yes")
    password_sol = [solver.model()[char].as_long() for char in password]
    return "".join([chr(i) for i in password_sol])
else:
    print("no sol")
    return 0

With the script finished running and the results was 806470850. so until know we have input Securinets{806470850

With the first and second parts of the key, it was time to move on to the final stage of the challenge: checking the last 12 characters of the input.

I found out that the program passed the last 12 characters of the input through a function called “rot” before comparing it with the string “_Q3eM3tT1t6}”.

The rot() function was a simple rotation function that shifted the letters in the input by a certain number of positions. It took two parameters, the string to be rotated, and the amount of rotation.

One important thing to note is that the rotation didn’t happen on special characters or numbers, it only happened on the alphabetic characters a-z and A-Z.

There are a few different ways to reverse the rot() function and find the correct input. One option is to use a tool like CyberChef. Another option is to write a python script to brute-force the characters.

However, in this case, I used the easy and fast way 🙂.

 

And with that, the challenge was finally complete. The correct input was “Securinets{806470850_K3yG3nN1n6}”, and it was accepted by the program.

I would like to thank you for reading this blog post and following along on my journey. I am happy to have reached the end and I hope you enjoyed it as much as I did. If you have any questions or feedback, please feel free to reach out to me 50r4.