R3v_m3

Downloading Challenge Files

here is the executable file to download

3KB

R3v_m3.rar

Basic EXE Reconnaissance

the executable is 64 bit that means that addresses will be 8 bytes and the exe is stripped that means we can view the function names

Reverse Engineering

as we have done in the S31r14l_Br34k3r challenge open ghidra and import the R3v_m3 binary into ghidra to analyze it after doing this open the functions and take a look at the exe functions

now open the main function and let's take a look the program code

the program takes the password input from the user and stores it into the password variable and then passes it into the check_password() function and if it passes the check then access granted will be outputed and if not access denied will be outputed

let's check the check_password function code in the first look it looks hard and overwhelming but it's way easier than it looks like

let's explain this code, so the program first takes the password the user inputed which is the param_1 and checks whether the length is 25 and then compares each character in the password with some character

so we can start collecting the password based on the array's index so *param_1 == 'D' means that the first character of the password should be D param_1[0x1] == 'E' means that the second character should be E and so on until we gather the whole password which is DEFENSYS{r3v_c4n_b3_c00l}

let's check whether this is the right flag or not by running the program and submiting the flag as the password and yep it's since we have got Access Granted

FLAG

DEFENSYS{r3v_c4n_b3_c00l}

Z3 (Theorem Prover Library)

so we can automate this using a z3 library that solves mathematical equations

in some cases in reverse engineering we can find way more complicated equations not just a simple isEqual (==) check like this

so we cannot waste time trying to find the flag variable that meets all these mathematical conditions so we have to automate this task and make the computer do that for us

so here the z3 library in python comes handy

from z3 import *  

flag = [Int(f'f_{i}') for i in range(25)]
solver = Solver()

solver.add(flag[0x0] == ord('D'), flag[0x5] == ord('S'), flag[0xa] == ord('3'))
solver.add(flag[0xf] == ord('n'), flag[0x14] == ord('c'), flag[0x1] == ord('E'))  
solver.add(flag[0x6] == ord('Y'), flag[0xb] == ord('v'), flag[0x10] == ord('_'))  
solver.add(flag[0x15] == ord('0'), flag[0x2] == ord('F'), flag[0x7] == ord('S'))
solver.add(flag[0xc] == ord('_'), flag[0x11] == ord('b'), flag[0x16] == ord('0'))  
solver.add(flag[0x3] == ord('E'), flag[0x8] == ord('{'), flag[0xd] == ord('c'))  
solver.add(flag[0x12] == ord('3'), flag[0x17] == ord('l'), flag[0x4] == ord('N'))  
solver.add(flag[0x9] == ord('r'), flag[0xe] == ord('4'), flag[0x13] == ord('_'))
solver.add(flag[0x18] == ord('}'))  

# checks whether z3 can solve those equations or not
if solver.check() == sat: 
	m = solver.model()
	out = [chr(m.evaluate(flag[i]).as_long()) for i in range(25)]                          
	print("".join(out))
else:
	print("this equations are not satisfiable")

and the z3 library will do all the work and generate the flag that meets those conditions let's run the python exploit

Greetings from Sayonara