HackTheBox - Shadow Labyrinth
HackTheBox - Shadow Labyrinth
Author: Pyload901
Overview
This challenges takes us through symbolic analysis and VM obfuscation, after this reading you will be able to solve challenges that uses basic symbolic analysis. You will also learn to create a VM disassembler and to conduct an analysis on disassembled code.
Reconnaissance one
After a static analysis, we found in main function at 0x11a0 the following important info:
- The input length is
0x58 - The input may literally starts with
HTB{and finishes with} - A secondary function at
0x1660analyze the input. This function only takes0x54chars so that is the length we will be working.
The secondary function is a little big and it makes 3 important processes detailed as follow:
1. Get the input chars to validate
In this step, the binary doesn’t verify the 0x54 characters, instead it obtains 0x30 characters using the user input like if it was a hashmap where the keys are hardcoded values in the memory.
The code above can be wrote as follows for a better understanding
hard_coded_values = [...]
chars_to_process = ['']*0x30
for i in range(0x30):
index = harcoded_values[i]
chars_to_process[i] = user_input[index]2. Verify the 0x30 chars obtained
To verify that the 0x30 chars before are correct, let buffer be the 0x30 chars obtained before and key1 and key2 be hardcoded data in binary’s memory. The program make a sum of products using key2 and buffer as follows:
$A_k =\sum_{j=0}^{3} b_{4k+j} \cdot key2_{4k+j}$
$[(b_0key2_0+ … +b_3key2_3), …,(b_{44}*key2_{44}+ … +b_{47}*key2_{47})]$
Or what is the same:
vector_A = []
key2 = [...] # <- hardcoded
buff = [...] # <- same as user input
for i in range(0x30):
sum_products = 0
for _ in range(0x4):
bi = buff[i]
key2i = key2[i]
sum_products += bi*key2i
vector_A.append(sum_products)Then every result of this operation (every element in vector_A) is compared against key1_j. If they are not equal, the flag is invalid.
Note that we will have only 12 comparisons because the sum of products consume four characters per iteration, this is $48/4 = 12$. This means that key1 only have 12 elements.
Note that key2 have 48 elements same as buffer.
Finally, if all comparisons are correct the program enters to another branch, that is the following step. We will return to this second step later, but first let’s figure out what happen after this process.
3. Open attached binary, decipher it, uncompress it and start a VM
When flag is correct, the binary starts reserving some memory, then it opens an attached binary to the challenge called file.bin, this file its decoded using XOR with a key stored at local_48 and finally the result is deciphered for AES 256 CBC using the 0x30 characters selected on step one as the key and a hardcoded IV.
The deciphered result is stored on the memory reserved at the beginning and it serves as as opcodes ****for a VM obfuscation.
Note that there is a gap between the memory reserved and file read, I decided to ignore that code because I could not link that logic to the actual flow. I think it is saving the remaining input into another location but I think the decompiler just broke these instructions.
The uncompress function expects a zlib compressed data to works, this was extracted from the OpenSSL lib documentation.
The code above can be translated as follows:
def decode(xor_key, file):
decoded = bytearray()
i = 0
for b in file:
decoded.append(b^xor_key[i&0xf])
i+=1
return decoded
def decipher(decoded_data, key:str, iv):
import Crypto.Cipher
ctx = AES.new(key=key[:32].encode(), iv=iv, mode=AES.MODE_CBC)
deciphered = ctx.decrypt(decoded_data)
return deciphered
def uncompress(deciphered):
import zlib
return zlib.decompress(deciphered)
if __name__ == "__main__":
xor_key = [...] # <- obtained later
iv = bytearray(...) # hardcoded on the binary
key = bytearray(...) # same as 0x30 chars obtained from user_input
with open('./file.bin', 'rb') as file:
data = decode(xor_key, file)
data = decipher(data, key, iv)
data = uncompress(data)
with open('./result.bin', 'wb') as result:
result.write(data)At this point we are almost ready to decipher file.bin, we only need some data to replace it in the code and our exploit will emulate the binary.
Exploitation one
Returning to step 2
In the step two we review the process that check the flag, as the process make some sum of products to verify the selected 0x30 characters of the flag and we don’t know part of every equation (the input chars) the problem is to solve some linear equations, this can be done with a symbolic analyzer like z3. In this case we will use Angr because it is easier to set it up and obtain the those 0x30 characters of the flag.
But before writing our script we may find out what are the 0x30 selected chars in order to correctly set up the symbolic variables. So let’s inspect the hardcoded data at 0x22c0.
from pwn import *
p = ELF('./shadow_labyrinth')
data = p.read(0x22c0, 0x30)
# in the decompiler we may see that we are dealing with bytes (8bits/1byte/char)
extracted = list(map(lambda x:int(x), data))
extracted.sort()
print(extracted)
"""
Expected output:
[
0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18,
19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35,
36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47
]
"""After inspection, we may figure out that binary basically selects the first 0x30 of the input to verify them. Then we can build an Angr script with the first 0x30 chars as symbolic variables.
import angr
import claripy
prefix = claripy.BVV(b"HTB{") # We already know this part of the flag
variables = [claripy.BVS(f"v{i}", 8) for i in range(0x30)]
final_part_of_flag = ("."*(0x53-0x30)+"}").encode() # we only need to solve the 0x30 chars, the other chars can be ignored rigth now
suffix = claripy.BVV(final_part_of_flag)
proj = angr.Project('./shadow_labyrinth', auto_load_libs=False)
base_addr = proj.loader.main_object.min_addr
stdin = claripy.Concat(prefix, *variables, suffix)
# create state
state = proj.factory.entry_state(stdin=stdin, add_options={
angr.options.ZERO_FILL_UNCONSTRAINED_MEMORY,
angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS
})
# add constraints
for v in variables:
state.solver.add(v>=0x20)
state.solver.add(v<=0x7b)
# create simulation manager
smgr = proj.factory.simulation_manager(state)
good = base_addr + 0x1730
bad = base_addr + 0x18f5
smgr.explore(find=good, avoid=bad)
# check if solved
if smgr.found:
print("Solution found: ")
found = smgr.found[0]
flag = found.solver.eval(stdin, cast_to=bytes)
print(flag.decode())
else:
print("No solution found")
This scripts will take some minutes (less than 5 minutes) to solve the flag, this is because of the loop that creates the linear equations. To have a faster script we may hook the while loop but i think it is not necessary, wait 1 or 2 minutes worth.
Now we have the first part of the flag but we already need the missing 0x23 characters, so we may continue by successfully deciphering the attached file.bin.
Returning to step 3
To successfully decipher the file.bin we may return to the script in Reconnaissance 3 and gather all missing information to complete the script.
- XOR Key
The key used to XOR the file.bin was in a non trackable variable, but now that we know the flag we can do a dynamic analysis to capture that key and use it on our script. If you go to the XOR line at 0x1808 you will notice that the data is stored at RSP + 0x400130 so we can go to our favorite dynamic analyzer and extract the data in that address.
In my case I just modified the Angr script to set up the correct flag and then just inspect the memory at that point.
# CODE
flag = claripy.BVV(b"HTB{by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy...................................}")
# CODE
state = proj.factory.entry_state(stdin=flag, add_options={
angr.options.ZERO_FILL_UNCONSTRAINED_MEMORY,
angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS
})
# CODE
good = base_addr + 0x17f6
# CODE
if smgr.found:
print("Solution found: ")
found = smgr.found[0]
dir = found.regs.rsp + 0x400130
data = found.memory.load(
dir,
16,
) # As we are reading bytes we may use Big Endian
data = found.solver.eval(data, cast_to=bytes)
with open('xor_key', 'wb') as xor_key:
xor_key.write(data)
else:
print("No solution found")
"""
Expected: 4g_dp____1dp41tn
"""Now we have the XOR key in a file called xor_key.
- Hardcoded IV
This step is quite simple, just read the 16 hardcoded bytes at 0x40c0
def getIV(program):
return program.read(0x40c0, 0x10)- AES256 Key
In Reconnaissance 3 we learned that the key are the selected 0x30 characters, then to build this key is quite simple.
def getHashMapKeys(program):
data = program.read(0x22c0, 0x30)
# in the decompiler we may see that we are dealing with bytes (8bits/1byte/char)
extracted = list(map(lambda x:int(x), data))
return extracted
def getAESKey(flag, program):
harcoded_values = getHashMapKeys(program)
chars_to_process = ['']*0x30
for i in range(0x30):
index = harcoded_values[i]
chars_to_process[i] = flag[index]
return ''.join(chars_to_process)We have all the required information and now we can finish the script.
from pwn import *
from Crypto.Cipher import AES
def getIV(program):
return program.read(0x40c0, 0x10)
def getHashMapKeys(program):
data = program.read(0x22c0, 0x30)
# in the decompiler we may see that we are dealing with bytes (8bits/1byte/char)
extracted = list(map(lambda x:int(x), data))
return extracted
def getAESKey(flag, program):
harcoded_values = getHashMapKeys(program)
chars_to_process = ['']*0x30
for i in range(0x30):
index = harcoded_values[i]
chars_to_process[i] = flag[index]
return ''.join(chars_to_process)
def decode(xor_key, data):
decoded = bytearray()
for i in range(len(data)):
decoded.append(data[i]^xor_key[i&0xf])
return decoded
def decipher(decoded_data, key:str, iv):
import Crypto.Cipher
ctx = AES.new(key=key[:32].encode(), iv=iv, mode=AES.MODE_CBC)
deciphered = ctx.decrypt(decoded_data)
return deciphered
def uncompress(deciphered):
import zlib
return zlib.decompress(deciphered)
if __name__ == "__main__":
program = ELF('./shadow_labyrinth')
flag = "by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy"
# retreive XOR key from file
xor_key = open('xor_key', 'rb').read()
iv = getIV(program)
key = getAESKey(flag, program)
# decipher
with open('./file.bin', 'rb') as file:
data = file.read()
data = decode(xor_key, data)
data = decipher(data, key, iv)
data = uncompress(data)
with open('./result.bin', 'wb') as result:
result.write(data)The expected output is the deciphered and uncompressed file used in the program to continue the execution.
Reconnaissance two
Note: this section was assisted by Gemini 3.0, specifically the understanding of some instructions like
getchar,suborjmp.
Understanding some instructions
Before we found that the binary does a VM obfuscation, because it executes functions in a jump table and the opcodes are in the file that we just extracted.
Note that the notation
pointer * 4means “access the value atpointerindex”.
Looking the jump table at 0x3ce0 we may find several functions, we will discuss some of them to understand how this VM works.
- The
getcharat0x3d48→0x15d0is used to obtain one character from the buffer: this function uses an stored pointer to measure the last queried index, and also uses the offsets0x40008cto store a read character and0x4000ccto extract the character.
Please note that
param_1is the opcode extracted fromfile.bin
- The
storeat0x3d20→0x14f0is used to save a value from some place after0x400000to some place inside the memory reserved for the opcodes.
Please note that we are finding several offsets, these can be used to create an structure and have a cleaner view of the code.
As you can see, in param_1 + 0x4000f0 we marked an IP (instruction pointer), this is assumed because the binary uses this variable like it was an instruction pointer, then we can be proof that param_1 + 0x4000f0 is an IP in a dynamic analysis. Let’s place a breakpoint on 0x18dd in your favorite analyzer, when program breaks you may inspect RBX and RSP+0x400100.
- RBX: may have the reserved memory where the deciphered
file.binis allocated. - RSP+0x400100: may have the value of
j
You may found that RBX+0x4000f0 = RSP+0x400100. This is a proof that j = ip
- The
subat0x3d10→0x1480is used to subtract two values, when the operation is performed a flag inparam_1 + 0x4000f4is set.
Note that right now the code is hard to read and to understand but we can make an struct type to make it readable, this will help us to find out what the other functions does to write our disassembler.
Creating our struct
Right now we know some offsets and we can work with them, this will make it easier. The following illustration represent how the memory is distributed when VM is working, consider the sections 0x400000 to 0x40008c and 0x40008c to 0x4000cc unified, this will make it simpler, just think in that memory like memory to save data.
Then we can make our structure type.
Finally the VM functions are more readable. Look the add function at 3d08 → 0x1450 as an example of how it looks.
After reversing all functions the jump table is as follows.
As you can see, this VMs allows the basic operations to be a Turing Complete machine and most important, we can make our disassembler.
Exploitation two
The first step is to make a dictionary of these instructions, this will help to match the instructions in our disassembler (This step can be skipped but I recommend it to make a readable code).
I extracted the following table using Ghidra and awk, you can paste it in a file if you like or extract your own.
00103ce0 clr
00103ce8 set_one
00103cf0 addi
00103cf8 subi
00103d00 shl
00103d08 add
00103d10 sub
00103d18 xor
00103d20 store
00103d28 load
00103d30 jne
00103d38 je
00103d40 jmp
00103d48 getchar
00103d50 print
00103d58 exitThen, using the following function in python we can make the dictionary
def getVMDictionary():
with open('vm_off', 'r') as file:
start_addr = 0x00103ce0
instructions = {}
for line in file:
line = line.strip()
addr = int(line.split(' ')[0], 16)
instruction = line.split(' ')[1]
idx = addr - start_addr
instructions[idx] = instruction
return instructions
"""
Expected: {0: 'clr', 8: 'set_one', 16: 'addi', 24: 'subi', 32: 'shl', 40: 'add', 48: 'sub', 56: 'xor', 64: 'store', 72: 'load', 80: 'jne', 88: 'je', 96: 'jmp', 104: 'getchar', 112: 'print', 120: 'exit'}
"""Then we may create the disassembler and read the result.bin extracted before, to translate the instructions. The following script creates a file disas and write the instructions there, this was useful for a better understanding of the opcode and for validating the disassembler.
from pwn import *
def getVMDictionary():
with open('vm_off', 'r') as file:
start_addr = 0x00103ce0
instructions = {}
for line in file:
line = line.strip()
addr = int(line.split(' ')[0], 16)
instruction = line.split(' ')[1]
idx = addr - start_addr
instructions[idx] = instruction
return instructions
def getUnpackedInstructions():
with open("result.bin", "rb") as file:
data = file.read()
return [u32(data[i:i+4], "little") for i in range(0,len(data),4)]
with open("disas", "w") as f:
unpacked = getUnpackedInstructions()
vm = getVMDictionary()
memory_inside = []
i=0
ip = 1
while i < len(unpacked) and ip < len(unpacked):
u = unpacked[i]
instruction = vm[int(u)*8] if vm.get(int(u)*8) else u
writable = ""
if i in memory_inside:
writable = f"mem {hex(u)}"
else:
match instruction:
case "getchar":
writable = instruction
case "store":
mem = unpacked[ip+1]+ip+2
memory_inside.append(mem)
writable = f"store ({mem}, regs[{unpacked[i+1]}])"
ip+=2
case "load":
mem = unpacked[ip+1]+ip+2
memory_inside.append(mem)
writable = f"load (regs[{unpacked[i+1]}], {mem})"
ip+=2
case "print":
buffer_start = ip+1+unpacked[ip]
writable = f"print ("
if buffer_start < len(unpacked):
memory_inside.append(buffer_start)
while unpacked[buffer_start] !=0 and buffer_start < len(unpacked):
c = chr(unpacked[buffer_start]) if unpacked[buffer_start] < 0x7f else '_'
writable += f"{c}, "
buffer_start+=1
writable += ")"
ip+=1
case "jmp":
# during the exploitation, truncating the
# ints to 32bits was useful for a better understanding
pos32bits = (ip-1+unpacked[ip])&0xFFFFFFFF
writable = f"jmp {pos32bits+1}"
ip+=1
case "je":
writable = f"if cmpflag = NIL then jmp {ip-1+unpacked[ip]+1}"
ip+=1
case "jne":
writable = f"if cmpflag != NIL then jmp {ip-1+unpacked[ip]+1}"
ip+=1
case "xor":
writable = f"xor (regs[{unpacked[ip]}], regs[{unpacked[ip+1]}])"
ip+=2
case "sub":
writable = f"regs[{unpacked[ip]}] -= regs[{unpacked[ip+1]}];\t"
writable += f"cmpflag = resta === 0"
ip+=2
case "subi":
writable = f"regs[{unpacked[ip]}] -= {unpacked[ip+1]};\t"
writable += f"cmpflag = resta === 0"
ip+=2
case "add":
writable = f"regs[{unpacked[ip]}] += regs[{unpacked[ip+1]}]"
ip+=2
case "addi":
writable = f"regs[{unpacked[ip]}] += {unpacked[ip+1]}"
ip+=2
case "shl":
ipval = unpacked[ip]
writable = f"regs[{ipval}] << {unpacked[ip+1]} & 0x1f"
ip+=2
case "clr":
writable = f"regs[{unpacked[ip]}] = 0"
ip+=1
case "set_one":
writable = f"regs[{unpacked[ip]}] = 1"
ip+=1
case "exit":
writable = "exit"
case _:
c = chr(u) if u < 0x7f else '_'
writable = f"{i} - mem {hex(u)} - {c}"
f.write(f"{i+1} | {writable}\n")
lineas_omitidas = ip-i-1
i=ip
ip+=1
for _ in range(lineas_omitidas):
f.write('-\n')
if i >= len(unpacked)-1 or ip >= len(unpacked)-1:
breakAfter creating the disas we can notice some important information that will lead us to the solution.
- The
getcharinstruction saves the character at0x40008cas discussed before but this memory address is the same asregs[35], you can proof it in a dynamic analysis.
- Strings and simulated memory are at the end of the file, starting at
126843line
- The comparison that decides if flag is correct or flag is wrong is only at the end of the code at line
126840. This means, to validate the flag, we must traverse the complete code.
- The
jneinstruction is used only for loops, the analysis throws that for everyjneinstruction, there is ajmpline that creates the loop. Then there is an extrajmpinstruction that doesn’t follow this rule only at the end of the code.
- The
jeinstruction is only used at the end of the file to check thatregs[0]toregs[34]has a zero value. If any register has a different value, the flag is incorrect.
- The rest of the code are mathematical operations, it doesn’t have any complex flow or something else.
Finally, after reviewing the pseudocode generated we can create the simulation and use z3 to solve these equations. In my case i just used the same disassembler but modifying some instructions to optimize loops and make z3 solver works. The script is as follows.
from pwn import *
from z3 import *
def getVMDictionary():
with open('vm_off', 'r') as file:
start_addr = 0x00103ce0
instructions = {}
for line in file:
line = line.strip()
addr = int(line.split(' ')[0], 16)
instruction = line.split(' ')[1]
idx = addr - start_addr
instructions[idx] = instruction
return instructions
def getUnpackedInstructions():
with open("result.bin", "rb") as file:
data = file.read()
return [u32(data[i:i+4], "little") for i in range(0,len(data),4)]
# useful to make breakpoints during analysis and explore the VM state
breakpoints = []
def bpoint(line, regs):
if line in breakpoints:
print(f"Breakpoint reached at {line}")
for idx,reg in enumerate(regs):
print(f"reg{idx} = {reg}", sep='\t')
input('--- Enter to continue ---')
def areInts(op1,op2):
return isinstance(op1, int) and isinstance(op2,int)
def interpret():
unpacked = getUnpackedInstructions()
vm = getVMDictionary()
# variables to control de simulation
symvars = []
mem_inside_offset = 126843
memory_inside = [0]*(126949 - mem_inside_offset)
regs = [0]*37
inLoop = False
multiplierLoop = 0
i=0
ip = 1
s = Solver()
while i < len(unpacked) and ip < len(unpacked):
# just break when reach the final comparison statements
if i > 126656:
break
u = unpacked[i]
instruction = vm[int(u)*8] if vm.get(int(u)*8) else u
writable = ""
# if instruction == "jne":
# breakpoints.append(i+1)
bpoint(ip,regs)
match instruction:
case "getchar":
# we use a 32 bits BitVec because we are dealing with 32 bits numbers on the VM
# using a 8bits will throw no solution due to integer granting
var = BitVec(f"v{int(random.random()*10000)}", 32)
s.add(
Or(
And(var>=0x61,var<=0x7a),
And(var>=0x30, var<=0x39),
var==0x5F
)
)
symvars.append(var)
regs[35] = var
case "store":
mem = unpacked[ip+1]+ip+2
regI = unpacked[i+1]
memory_inside[mem-mem_inside_offset] = regs[regI]
ip+=2
case "load":
mem = unpacked[ip+1]+ip+2
regs[unpacked[i+1]] = memory_inside[mem-mem_inside_offset]
writable = f"load (regs[{unpacked[i+1]}], {mem})"
ip+=2
case "print":
ip+=1
case "jmp":
pos32bits = (ip-1+unpacked[ip])&0xFFFFFFFF
writable = f"jmp {pos32bits+1}"
ip+=1
case "je":
writable = f"if cmpflag = NIL then jmp {ip-1+unpacked[ip]+1}"
ip+=1
case "jne":
# manage loops in an efficient way, this is just a product, no loop is needed
multiplierLoop = regs[35]
inLoop = True
writable = f"if cmpflag != NIL then jmp {ip-1+unpacked[ip]+1}"
ip+=1
case "xor":
regs[unpacked[ip]] = simplify(regs[unpacked[ip]] ^ regs[unpacked[ip+1]])
writable = f"xor (regs[{unpacked[ip]}], regs[{unpacked[ip+1]}])"
ip+=2
case "sub":
# manage loops in an efficient way, this is just a product, no loop is needed
if inLoop:
if areInts(regs[unpacked[ip]], regs[unpacked[ip+1]]*multiplierLoop):
regs[unpacked[ip]] = (regs[unpacked[ip]] - regs[unpacked[ip+1]]*multiplierLoop)&0xFFFFFFFF
else:
regs[unpacked[ip]] = simplify(regs[unpacked[ip]] - regs[unpacked[ip+1]]*multiplierLoop)
inLoop = False
else:
regs[unpacked[ip]] -= regs[unpacked[ip+1]]
writable = f"regs[{unpacked[ip]}] -= regs[{unpacked[ip+1]}];\t"
writable += f"cmpflag = resta === 0"
ip+=2
case "subi":
if inLoop:
if areInts(regs[unpacked[ip]], unpacked[ip+1]*multiplierLoop):
regs[unpacked[ip]] = (regs[unpacked[ip]] - unpacked[ip+1]*multiplierLoop)&0xFFFFFFFF
else:
regs[unpacked[ip]] = simplify(regs[unpacked[ip]], unpacked[ip+1]*multiplierLoop)
inLoop = False
else:
regs[unpacked[ip]] -= unpacked[ip+1]
writable = f"regs[{unpacked[ip]}] -= {unpacked[ip+1]};\t"
writable += f"cmpflag = resta === 0"
ip+=2
case "add":
# manage loops in an efficient way, this is just a product, no loop is needed
if inLoop:
if areInts(regs[unpacked[ip]],regs[unpacked[ip+1]]*multiplierLoop):
regs[unpacked[ip]] = (regs[unpacked[ip]] + regs[unpacked[ip+1]]*multiplierLoop) & 0xFFFFFFFF
else:
regs[unpacked[ip]] = simplify(regs[unpacked[ip]] + regs[unpacked[ip+1]]*multiplierLoop)
inLoop = False
else:
regs[unpacked[ip]] += regs[unpacked[ip+1]]
writable = f"regs[{unpacked[ip]}] += regs[{unpacked[ip+1]}]"
ip+=2
case "addi":
if inLoop:
if areInts(regs[unpacked[ip]], unpacked[ip+1]*multiplierLoop):
regs[unpacked[ip]] = (regs[unpacked[ip]] + unpacked[ip+1]*multiplierLoop) & 0xFFFFFFFF
else:
regs[unpacked[ip]] = simplify(regs[unpacked[ip]] + unpacked[ip+1]*multiplierLoop)
inLoop = False
else:
regs[unpacked[ip]] += unpacked[ip+1]
writable = f"regs[{unpacked[ip]}] += {unpacked[ip+1]}"
ip+=2
case "shl":
ipval = unpacked[ip]
op2 = unpacked[ip+1] & 0x1f
if areInts(regs[ipval], op2):
regs[ipval] <<= op2
regs[ipval] &= 0xFFFFFFFF
else:
regs[ipval] = simplify(regs[ipval] << op2)
writable = f"regs[{ipval}] << {unpacked[ip+1]} & 0x1f"
ip+=2
case "clr":
regs[unpacked[ip]] = 0
writable = f"regs[{unpacked[ip]}] = 0"
ip+=1
case "set_one":
regs[unpacked[ip]] = 1
writable = f"regs[{unpacked[ip]}] = 1"
ip+=1
case "exit":
writable = "exit"
case _:
c = chr(u) if u < 0x7f else '_'
writable = f"{i} - mem {hex(u)} - {c}"
i=ip
ip+=1
if i >= len(unpacked)-1 or ip >= len(unpacked)-1:
break
print("VM finished, starting solver")
for k in range(35):
var = regs[k]
s.add(var == 0)
print("Added final constraints")
print("Starting symbolic analysis")
if s.check() == sat:
model = s.model()
flag = ""
for var in symvars:
res = model[var].as_long()
flag+=chr(res)
print(flag)
else:
print("No solution broooo!")
if __name__ == "__main__":
input_bpoints = input('Enter breakpoints in csv format> ')
if input_bpoints != '':
breakpoints = list(map(lambda x: int(x), input_bpoints.split(',')))
interpret()This codes looks intimidating but it is not, here are some important points for a better understanding.
- Loops are handled by some global vars that identify a loop when a
jneinstruction is reached and saves the multiplier for the sum. Then when the VM reaches theaddinstruction, it just make an addition with the multiplier. This logic was copy pasted to the other math operations (sub,subi,addi). - The simulation ends just right after reach the 126656 line, this is right after the last XOR operation.
- I decided to truncate the result of the math operations just in case, this is for
add,addi,sub,subiandshl. This truncation is applied only when both operands are numeric, because z3 already handles this for BitVec. - The use of
simplifyis important to make the equations as easier as possible, as the VM is not too long there is no problem for applyingsimplifyper operation.
After simulating the VM, and solve the equations, the flag appears.
The simulations took me around 30 minutes.
Finally, the flag is
HTB{by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy_tuturututu_n3v3r_g0nna_g1v3_y0u_up}
