# Rev - Cave System

## Description

Deep inside a cave system, 500 feet below the surface, you find yourself stranded with supplies running low. Ahead of you sprawls a network of tunnels, branching off and looping back on themselves. You don't have time to explore them all - you'll need to program your cave-crawling robot to find the way out...

## Downloads

{% file src="/files/5gqKn1o7YoPah26s8xO6" %}

## Solution

The first thing we see when decompiling the binary is the following:

<figure><img src="/files/C1wDR88oMyjcqeQRZ3Xs" alt=""><figcaption><p>De-compilation of 'cave'</p></figcaption></figure>

This looks like a typical constraint checking challenge which can be easily solved with an SMT solver. Fun fact: I created a similar challenge for Cyberthon 2022 and so I already have a solve script ready.

To feed the decompilation output into my script however, I will need to manipulate the output a little.

<figure><img src="/files/hdhpklXFjMS4ftrNRPyu" alt=""><figcaption><p>A look at the 's' variable</p></figcaption></figure>

It seems like IDA does not know the type of the 's' variable but we know from the `fgets` and `memcmp` function that 's' is likely a character array of length 128. So we tell IDA to explicitly 'Set the type' to `char s[128]` as shown below.

<figure><img src="/files/2E0Yae4uphvJe0iDPBTm" alt=""><figcaption><p>Set lvar type</p></figcaption></figure>

The output is something much more read-eable.

<figure><img src="/files/q1VjsmKSC6lUz1fjsbMz" alt=""><figcaption><p>After changing variable type</p></figcaption></figure>

With this output, I can easily copy it out from IDA and do some minor string replacement using Sublime Text to retrofit it into my Z3 solve script.

The final Z3 script:

{% code lineNumbers="true" %}

```python
from z3 import *

# List of BitVec
s = [BitVec(f'{i}', 8) for i in range(124)]
z = Solver()

z.add(s[48] * s[21] == 20)
z.add(s[32] - s[36] == 0xFA)
z.add(s[37] - s[26] == 0xD6)

# ...
# Redacted for brevity
# ...

z.add(s[3] + s[5] == 0xAB)
z.add(s[35] - s[47] == 0xD2)
z.add((s[33] ^ s[16]) == 16 )

print(z.check())
model = z.model()
flag = ''.join([chr(int(str(model[s[i]]))) for i in range(len(model))])
print(flag)
```

{% endcode %}

Flag: `HTB{H0p3_u_d1dn't_g3t_th15_by_h4nd,1t5_4_pr3tty_l0ng_fl4g!!!}`


---

# 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://arne-ctf.gitbook.io/ctf/2023/htb-cyber-apocalypse/rev-cave-system.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.