"""
Unpacker for TA505s crypters as outlined in blog:
https://labs.sentinelone.com/breaking-ta505s-crypter-with-an-smt-solver/

By: <NAME>

"""
import sys
import re
import struct
import aplib
from z3 import *

ror = lambda val, r_bits, max_bits=32: \
	((val & (2**max_bits-1)) >> r_bits%max_bits) | \
	(val << (max_bits-(r_bits%max_bits)) & (2**max_bits-1))

rol = lambda val, r_bits, max_bits=32: \
	(val << r_bits%max_bits) & (2**max_bits-1) | \
	((val & (2**max_bits-1)) >> (max_bits-(r_bits%max_bits)))


possible_decodes = [bytearray('M8Z\x90')]

def solve_ta505crypter(input, output):
	xorkey = BitVec('xor1', 32)
	s = Solver()
	s.add(rol(BitVecVal(struct.unpack_from('<I',input)[0], 32) ^ xorkey, 4) + 2004318072 == BitVecVal(struct.unpack_from('<I',output)[0], 32))
	return(s)




data = open(sys.argv[1], 'rb').read()
t = re.findall('\x00\x60..\x00\x60..\x00\x60..\x00\x60..', data, re.DOTALL)
if t == []:
	t = re.findall('\x52\x00..\x52\x00..\x52\x00..\x52\x00..', data, re.DOTALL)


#Should be first match
if t != []:
	off = data.find(t[0])
	#blob = data[off:off+300000]
	blob = data[off:off+0x1d0ad8]

	#Fix data
	i = 0
	j = 0
	t = ""
	while i < len(blob):
		if not(j % 2):
			i += 2
		t += blob[i]
		i += 1
		j += 1
		
	key = None
	for poss_decode in possible_decodes:
		s = solve_ta505crypter(t, poss_decode)
		if s.check() == sat:
			m = s.model()
			for d in m.decls():
				if d.name() == 'xor1':
					key = m[d].as_long()
	if key:
		out = ""
		for i in range(len(t)/4):
			temp = struct.unpack_from('<I', t[i*4:])[0]
			temp ^= key
			temp = rol(temp, 4)
			temp += 2004318072
			out += struct.pack('<I', temp & 0xffffffff)

		open(sys.argv[1]+'_decodedObject', 'wb').write(out)
		if out[:3] == 'M8Z':
			print("Decompressing")
			out2 = aplib.decompress(out).do()
			open(sys.argv[1]+'_decompressed', 'wb').write(out2[0])

"""
Unpacker for TA505s crypters as outlined in blog:
https://labs.sentinelone.com/breaking-ta505s-crypter-with-an-smt-solver/

By: <NAME>

"""
import sys
import re
import struct
import aplib
from z3 import *

ror = lambda val, r_bits, max_bits=32: \
	((val & (2**max_bits-1)) >> r_bits%max_bits) | \
	(val << (max_bits-(r_bits%max_bits)) & (2**max_bits-1))

rol = lambda val, r_bits, max_bits=32: \
	(val << r_bits%max_bits) & (2**max_bits-1) | \
	((val & (2**max_bits-1)) >> (max_bits-(r_bits%max_bits)))


possible_decodes = [bytearray('M8Z\x90')]

def solve_ta505crypter(input, output):
	xorkey = BitVec('xor1', 32)
	s = Solver()
	s.add(rol(BitVecVal(struct.unpack_from('<I',input)[0], 32) ^ xorkey, 4) + 2004318072 == BitVecVal(struct.unpack_from('<I',output)[0], 32))
	return(s)




data = open(sys.argv[1], 'rb').read()
t = re.findall('\x00\x60..\x00\x60..\x00\x60..\x00\x60..', data, re.DOTALL)
if t == []:
	t = re.findall('\x52\x00..\x52\x00..\x52\x00..\x52\x00..', data, re.DOTALL)


#Should be first match
if t != []:
	off = data.find(t[0])
	#blob = data[off:off+300000]
	blob = data[off:off+0x1d0ad8]

	#Fix data
	i = 0
	j = 0
	t = ""
	while i < len(blob):
		if not(j % 2):
			i += 2
		t += blob[i]
		i += 1
		j += 1
		
	key = None
	for poss_decode in possible_decodes:
		s = solve_ta505crypter(t, poss_decode)
		if s.check() == sat:
			m = s.model()
			for d in m.decls():
				if d.name() == 'xor1':
					key = m[d].as_long()
	if key:
		out = ""
		for i in range(len(t)/4):
			temp = struct.unpack_from('<I', t[i*4:])[0]
			temp ^= key
			temp = rol(temp, 4)
			temp += 2004318072
			out += struct.pack('<I', temp & 0xffffffff)

		open(sys.argv[1]+'_decodedObject', 'wb').write(out)
		if out[:3] == 'M8Z':
			print("Decompressing")
			out2 = aplib.decompress(out).do()
			open(sys.argv[1]+'_decompressed', 'wb').write(out2[0])

Unpacker for TA505s crypters as outlined in blog: https://labs.sentinelone.com/breaking-ta505s-crypter-with-an-smt-solver/  By: <NAME> #Should be first match #blob = data[off:off+300000] #Fix data