As of late, I haven’t had the opportunity to get any CTF write-ups posted on my blog. Part of the reason is because I’ve begun playing with a much larger team and I’m finding myself with lots of half solutions as I attack problems with groups of people. This would lead to incomplete write-ups and the ensuing confusion. I decided however that there are are a couple of partial solutions I wanted to post anyways as they could be useful on future challenges.
The first snippet I want to share was for the Forensic 100 challenge in HackIM2016 (Nullcon). I have seen variations of this challenge many times and have always wished I had a script to automate it as it is quite annoying. Challenges of this type typically consist of a file that has been compressed dozens of times by over a dozen different compression algorithms. Using the magic library, I scripted up a solution that would make this challenge a little easier. Feel free to extend upon it if you run across a similar challenge.
import magic
import sys
import os
import shutil
comp_types = {"ARC archive data":"nomarch ",
"PPMD archive data":"ppmd d ",
"Microsoft Cabinet archive data":"cabextract ",
"bzip2 compressed data":"bunzip2 ",
"XZ compressed data":"xz -d ",
"7-zip archive data":"7z x ",
"gzip compressed data":"gunzip ",
"POSIX tar archive (GNU)":"tar xvf ",
"Zip archive data":"unzip ",
"KGB Archiver file with compression level 3":"kgb ",
"ARJ archive data":"arj e ",
"rzip compressed data":"rzip -d ",
"ZOO archive data":"zoo e ",
"RAR archive data":"unrar e" }
#decompressed filename
dec_file = "secret"
#Get the unzipped filename, typically it is the same so it can be scripted
if dec_file == None or len(dec_file) == 0:
print "Enter decompressed filename if it is constant:"
dec_file = raw_input()
while(True):
print "n[+] Current directory listing"
print os.listdir(".")
if os.path.isfile(dec_file + ".tmp"):
filename = dec_file + ".tmp"
else :
print_str = "nPlease enter the filename to decompress or q to quit"
if( dec_file != None and len(dec_file) > 0 and os.path.isfile(dec_file + ".tmp") ):
print_str += "(" + dec_file + ".tmp" + "):"
print print_str
filename = raw_input()
if len(filename) == 0:
filename = dec_file + ".tmp"
else:
print_str += ":"
print print_str
filename = raw_input()
if(filename == ‘q’):
exit()
#flags=magic.MAGIC_MIME_TYPE
with magic.Magic() as m:
comp_type = m.id_filename(filename).strip()
try:
idx = comp_type.index(",")
if idx > 0:
comp_type = comp_type[:idx].strip()
except:
pass
print "nFile type: " + comp_type
ex_str = comp_types.get(comp_type)
if ex_str == None:
print "Enter the application name for decompression: "
ex_str = raw_input() + " "
print "Enter any command line switches: "
switches = raw_input()
#concatenate them
if switches != None and len(switches) > 0:
ex_str += switches + " "
comp_types[comp_type] = ex_str
#execute
os.system(ex_str + filename)
#move dest_file
try:
if( dec_file != None and len(dec_file) > 0):
shutil.move(dec_file, dec_file + ".tmp")
except:
if os.path.isfile(dec_file + ".tmp.out"):
shutil.move(dec_file + ".tmp.out", dec_file + ".tmp")
else:
print os.listdir(".")
print "Rename archive file to: "
new_name = raw_input()
if len(new_name) > 0:
shutil.move(dec_file + ".tmp", new_name)
pass
print os.listdir(".")[/sourcecode]
The second snippet is from the Unholy challenge in Boston Key Party 2016. This was a reversing challenge that required you to reverse engineer two algorithms that scrambled the flag. The first algorithm is performed in C and the second is in python. Luckily for me, other members on my team solved the python algorithm and provided me with the outputs that would be produced by the C algorithm. Using these outputs and the provided algorithm I needed to determine the initial inputs. Pseudocode of the algorithm is shown below.
Unlike many others in the competition that solved this challenge, I did not recognize this algorithm as the XTEA block cipher. Therefore the only idea I had to solve it was to use the Z3 SAT solver library. After studying the algorithm a little bit, I saw that it executed exactly 32 times and operated on two integers at a time. I decided to unroll the loop and add constraints to Z3 on each iteration. Since I knew the final outputs, I added the outputs of the algorithm as the last constraint. The final solution can be seen below.
import struct
key = [ 0x74616877, 0x696F6773, 0x6E6F676E, 0x65726568 ]
req_result = [-1304886577, 722035088, 1368334760, 1473172750, 412774077, -908901225, -490967005, 563111828, -952589187, 1306786301]
def get_index( index ):
v11 = index + key[index & 3]
if index >= 0x61C88647:
index -= 0x61C88647
else:
index = 0xffffffff & ((0x10000000000000000 + index) – 0x61C88647)
return (v11, index)
def solve_tuple( first_val, second_val ):
start1 = BitVec(‘start[1]’, 32)
start2 = BitVec(‘start[2]’, 32)
var_arr = []
for i in range(0, 64):
var_arr.append( BitVec(‘var[‘+str(i)+’]’, 32) )
#create solver
solver = Solver()
#round 0
arr = get_index(0)
val = int(str(simplify(LShR( BitVecVal(arr[1], 64), 11 ))))
solver.add( var_arr[0] == (arr[0] ^ (( 16 * start2 ^ ( LShR(start2 , 5))) + start2)) + start1 )
solver.add( var_arr[1] == ((arr[1] + key[ val & 3]) ^ (( 16 * var_arr[0] ^ ( LShR(var_arr[0] , 5))) + var_arr[0] )) + start2)
#round 1
for j in range( 1, 63, 2 ):
arr = get_index(arr[1])
val = int(str(simplify(LShR( BitVecVal(arr[1], 64), 11 ))))
solver.add( var_arr[j+1] == (arr[0] ^ ( (( 16 * var_arr[j] ) ^ ( LShR(var_arr[j], 5 ))) + var_arr[j])) + var_arr[j-1])
solver.add( var_arr[j+2] == ((arr[1] + key[val & 3]) ^ (( ( 16 * var_arr[j+1] ) ^ ( LShR(var_arr[j+1], 5))) + var_arr[j+1] )) + var_arr[j])
solver.add( var_arr[62] == first_val )
solver.add( var_arr[63] == second_val )
solver.check()
s = solver.model()
#Print results
return (int(str(s[start1])) , int(str(s[start2])) )
#Solve it
result = []
for k in range(0, len(req_result), 2 ):
ret_val = solve_tuple( req_result[k], req_result[k+1] )
result.append(ret_val[0])
result.append(ret_val[1])
print "[+] Flag:"
print struct.pack("10I", *result)