Tags: rev
Rating: 5.0
# Rev: ArchRide
## First look
We are provided a file ``surprise`` which we notice, after running ``xxd -l 100 surprise``, starts with the header ``42 5a 68 39``. This is recognizable as a BZip2 zipped file. After unzipping it, we are left with an x86-64 ELF file. We throw this into our decompiler of choice and find that it performs a few actions:
- Reads a 14-letter key
- Checks the XOR of various sets of 3 letters with some data embedded in the program
- If all this is satisfied, it overwrites the file ``surprise`` with a section of data in the program XORed with the key, repeating every 13 letters
## Solving first layer
It is clear that we need to find a printable key that satisfied the XOR checks in the program. To do this, we can manually extract the 28 XOR check results and the indices of letters that get XORed, or parse this by using a package such as ``r2pipe``. We then simply feed these constraints into a solver such as ``z3``. Upon analyzing the constraints we can see that, for any given first character of the key, there only exists at most one solution. We loop over all printable first characters and look for keys satisying all conditions. The following code is a rough idea of what is needed:
```
from z3 import *
inds = [[0, 4, 2],[2, 4, 6],[4, 6, 8],[6, 8, 10],[8, 10, 12],[10, 12, 1],[12, 1, 3],[1, 3, 5],[3, 5, 7],[5, 7, 9],[7, 9, 11],[9, 11, 13],[0, 11, 13],[0, 13, 2],[0, 1, 2],[1, 2, 3],[2, 3, 4],[3, 4, 5],[4, 5, 6],[5, 6, 7],[6, 7, 8],[7, 8, 9],[8, 9, 10],[9, 10, 11],[10, 11, 12],[11, 12, 13],[0, 12, 13],[0, 13, 1]]
sol = Solver()
key = [BitVec(str(i), 8) for i in range(14)]
keyr = []
dat = [] # insert check bytes here
for i in range(len(inds)):
ind = inds[i]
sol.add(key[ind[0]] ^ key[ind[1]] ^ key[ind[2]] == dat[i])
for i in range(30, 128):
sol.push()
sol.add(key[0] == i)
if sol.check() == sat:
keyr = [sol.model()[key[i]].as_long() for i in range(14)]
sol.pop()
```
This gives us a key of ``JCE1aWJApiDO5K``. Running the program and inputting this indicates success, and upon further investigation we see the file ``surprise`` has changed. Decompressing again, we find that this time the file is an x86 ELF. Continuing this process eventually leads us to discover that it repeats over and over again with different ELF architectures, including ``x86-64``, ``x86``, ``ARM32``, ``ARM64`` and ``PowerPC``.
## Automating layer solves
First off, we tried writing different disassembly parsers for all architectures, but soon realised that this is more effort than it is worth, and that for each architecture, the XOR check addresses and data start address are distinct. Just hardcoding these addresses is sufficient to extract the next layer from any ELF. It is worth noting that the endianness is also different for ``PowerPC``. We use these addresses to read the relevant checks from the ELF, then generate the key and XOR it with the data starting at the correct address. It is also worth noting that the ending doesn't matter, as the BZip2 stream includes a terminator. Decompressing this and saving allows us to repeat until we reach the final executable. Code is as follows (supply with the first executable as ``temp``)
```
import r2pipe
from bz2 import decompress
from z3 import *
from subprocess import check_output
import sys
while True:
inds = [[0, 4, 2],[2, 4, 6],[4, 6, 8],[6, 8, 10],[8, 10, 12],[10, 12, 1],[12, 1, 3],[1, 3, 5],[3, 5, 7],[5, 7, 9],[7, 9, 11],[9, 11, 13],[0, 11, 13],[0, 13, 2],[0, 1, 2],[1, 2, 3],[2, 3, 4],[3, 4, 5],[4, 5, 6],[5, 6, 7],[6, 7, 8],[7, 8, 9],[8, 9, 10],[9, 10, 11],[10, 11, 12],[11, 12, 13],[0, 12, 13],[0, 13, 1]]
sol = Solver()
key = [BitVec(str(i), 8) for i in range(14)]
dat = []
ver = check_output(["file", "temp"]).decode().split(", ")[1].split(", ")[0]
r2 = r2pipe.open("temp")
endian = "little"
if ver == "x86-64":
dat = [hex(0x202020), hex(0x202060)]
start = 0x20a0
elif ver == "Intel 80386":
dat = [hex(0x3020), hex(0x3060)]
start = 0x20a0
elif ver == "ARM aarch64":
dat = [hex(0x12010), hex(0x12048)]
start = 0x2080
elif ver == "ARM":
dat = [hex(0x11008), hex(0x11040)]
start = 0x01078
elif ver == "64-bit PowerPC or cisco 7500":
dat = [hex(0x10020130), hex(0x10020168)]
start = 0x101a0
endian = "big"
dat = [eval(r2.cmd("pf [14]d @" + addr).split(" = ")[1]) for addr in dat]
dat = dat[0] + dat[1]
if dat[0] > 255:
print(check_output(["./temp"]).decode())
sys.exit(0)
keyr = []
for i in range(len(inds)):
ind = inds[i]
sol.add(key[ind[0]] ^ key[ind[1]] ^ key[ind[2]] == dat[i])
for i in range(30, 128):
sol.push()
sol.add(key[0] == i)
if sol.check() == sat:
keyr = [sol.model()[key[i]].as_long() for i in range(14)]
sol.pop()
fdat = open("temp", "rb").read()[start:]
fdat = [(int.from_bytes(fdat[i*8:(i+1)*8], endian) ^ keyr[i%13]) & 0xff for i in range(0, len(fdat)//8)]
try:
fdat = decompress(bytes(fdat))
out = open("temp", "wb")
out.write(fdat)
out.close()
except:
out = open("temp", "wb")
out.write(bytes(fdat))
out.close()
```
# Final layer
Executing the final ELF gives us the flag, ``inctf{x32_x64_ARM_MAC_powerPC_4rch_maz3_6745}``
