> For the complete documentation index, see [llms.txt](https://sayonara.gitbook.io/writeups/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://sayonara.gitbook.io/writeups/ctf/ensa-sics-ctf-2023/reverse-engineering-challenges/r3v_m3.md).

# R3v\_m3

## <mark style="color:red;">Downloading Challenge Files</mark>

here is the executable file to download

{% file src="/files/Wy8g5k5j90mcesqiMuLm" %}

## <mark style="color:red;">Basic EXE Reconnaissance</mark>

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

<div align="left"><figure><img src="/files/mWGrG7QHT2gQzuBPBcfq" alt=""><figcaption></figcaption></figure></div>

## <mark style="color:red;">Reverse Engineering</mark>

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

## ![](/files/rs2RFsfZ0JXoCF7Pwa0M)

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

<div align="left"><figure><img src="/files/HeDaJWZ7FHSY1w9bAwQp" alt=""><figcaption></figcaption></figure></div>

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&#x20;

<div align="left"><figure><img src="/files/6isWObBeRD5AXLGPvO4K" alt=""><figcaption></figcaption></figure></div>

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&#x20;

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 <mark style="color:blue;">**DEFENSYS{r3v\_c4n\_b3\_c00l}**</mark>

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

<div align="left"><figure><img src="/files/uDkiKEMdxgFqemoxLq8s" alt=""><figcaption></figcaption></figure></div>

## <mark style="color:red;">**FLAG**</mark>

**DEFENSYS{r3v\_c4n\_b3\_c00l}**

## <mark style="color:red;">**Z3 (Theorem Prover Library)**</mark>

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&#x20;

<div align="left"><figure><img src="/files/zLVPuSgsbGmnQiIvMs1Q" alt=""><figcaption></figcaption></figure></div>

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

```python
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

<div align="left"><figure><img src="/files/RJuNbEtSONA640A0hL6x" alt=""><figcaption></figcaption></figure></div>

Greetings from [<mark style="color:blue;">**Sayonara**</mark>](https://github.com/ismail-arame/)