# AlexCTF : Catalyst System WriteUp

This year we got a group together to do AlexCTF. Most all the problems were fun, and overall I enjoyed the event.
Of the initial challenges released Friday, I had the most fun with the Reverse Engineering 3, Catalyst System challenge.

A quick aside about the two tools I used for this challenge; Radare2 and Z3. Radare2 is my favorite binary analysis or debugging tool. There is a bit of a learning curve, but it is powerful and open sourced! (Also, I love that no one knows how to say Radare, so you get all sorts of fun interpretations.) If you are still using gdb, I highly recommend taking the time to get to know it. Z3 is a high-performance theorem prover (it does the math I can’t be bothered with).

In this challenge, we were presented with a binary, that checks for a username and password. If you run this binary, you are going to notice a long load time. We opened the file using the lovely Radare2 and noticed two calls to sleep, right in main. We replaced the calls to sleep with 5 bytes of 0x90 (No Operation). That got rid of the unbearable wait time.

Then we got to the meat of the problem. Here, after accepting the user input and password, the program calls 4 functions, and if all pass the 5th function will create and output the flag.

Note that a pointer to the input username is loaded as an argument to these functions in rdi, and the last three also have a pointer to the password in rsi.

When we follow the execution through fcn.00400c9a, we find that it loops through counting the characters in the username, and passed the total count to function sub.puts_c41.

This function verifies the number of characters in the following steps:

1. Make sure num == ((num >> 2) << 2)
2. Make sure ((num>>4) << 2) != (num >> 2)
3. Make sure (num >> 3) != 0
4. Make sure (num >> 4) == 0

This means that the number of characters in our username can be binary 001100 or binary 001000. This is 12 or 8 characters.

Once we pass that test, we move on to sub.puts_cdd. This function was fun to follow. Here above is some annotated assembly.

This gave us a simple system of 3 equations, with 3 unknowns. Rather than work this out ourselves, we used the following code in Z3.

```(declare-const h10 (_ BitVec 64))
(declare-const h18 (_ BitVec 64))
(declare-const h20 (_ BitVec 64))

(assert (= (bvadd (bvsub h10 h18) h20) #x000000005c664b56))
(assert (= (bvmul h18 h20) #x32ac30689a6ad314))

(check-sat)
(get-model)```

It provided 3 hex numbers out, which we plopped into a python shell and turned into ASCII characters. After we remembered Little Endianness, we found the username.

The next function, sub.puts_8f7, passed fine with the username we found in the previous function. After a quick scan, we didn’t see any side effects in the code, so we moved on to the next function.

sub.puts_977 is the function that evaluates the password, and there are two main parts. First is the logic tree that evaluates each character, making sure that it is in the correct range. It turns out to be a waste of time to care about this section, but I will give a brief overview.
In the node above rbp – 0x14 holds the index into the string, and this node checks if a character is less than or equal to 0x2f. When you simplify the logic for all the nodes, it ends up being a simple check for characters from A-Za-z0-9.

But, like I said, even following that logic is not needed. After all of the characters are checked, and the index points to the null terminator of the password string, random is seeded using srand. The seed is all three four bytes pieces of the username, added together. Then the program produces a random number, subtracts it from 4 bytes of the password, and compares the result with a constant. This is repeated 9 times more, taking in 4 bytes of the password at a time, for a total of 40 characters in the password.
To know the password, we just take the constant and add the random value.  (At first, we wrote a tedious, large Z3 script to find our values, including the character range tests. Later we realized our mistake and did a large face-palm.) Thankfully, the seed is consistent, and we wrote a quick c program that gave us our random values.

```#include <stdlib.h>
#include <stdio.h>

int main() {
int i;
srand(0x454d3e2e); // from username, first4 + mid4 + last4
for (i = 0; i < 10; i++) {
printf("#%d : %x\n", i, rand());
}
return 0;
}```

This gave us our hex values for our password, which we again placed into a string in python, and turned into our ASCII password.

```b_in = bytes.fromhex(hexstring)
bout = b''
for i in range(len(b_in)//4):
rev = b_in[i*4:(i*4)+4]
bout += rev[::-1]
print(bout)```

When we ran the executable again and entered our username and password, the last function in main turned our input into a lovely ALEXCTF{…} flag!

Overall, I enjoyed the problems prepared for AlexCTF. In fact, I thought all of the challenges were well done (except for Cutie Cat, that was a bit gimmicky). Thank you odd_coder and the rest of the AlexCTF team!