# 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/)


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://sayonara.gitbook.io/writeups/ctf/ensa-sics-ctf-2023/reverse-engineering-challenges/r3v_m3.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.