Rev - Cave System

Easy

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

4KB

rev_cavesystem.zip

archive

Solution

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

De-compilation of 'cave'

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.

A look at the 's' variable

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.

Set lvar type

The output is something much more read-eable.

After changing variable type

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:

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)

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