> For the complete documentation index, see [llms.txt](https://arne-ctf.gitbook.io/ctf/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://arne-ctf.gitbook.io/ctf/2023/htb-cyber-apocalypse/rev-cave-system.md).

# 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!!!}`