Script to decode jscript from 70a6a7ba56bed99021acc3c9465adf

import sys
import re
import struct
import base64
import binascii
from z3 import *


possible_decodes = [bytearray('(function')]

def solve_docdropper(input, output):
	xor_1 = BitVec('xor_1', 8)
	xor_2 = BitVec('xor_2', 8)
	xor_3 = BitVec('xor_3', 8)
	xor_4 = BitVec('xor_4', 8)

	s = Solver()

	for i in range(0,min(len(input),len(output)),4):
			s.add((BitVecVal(input[i],8)) ^ xor_1 == BitVecVal(output[i],8))
			s.add((BitVecVal(input[i+1],8)) ^ xor_2 == BitVecVal(output[i+1],8))
			s.add((BitVecVal(input[i+2],8)) ^ xor_3 == BitVecVal(output[i+2],8))
			s.add((BitVecVal(input[i+3],8)) ^ xor_4 == BitVecVal(output[i+3],8))
	#s.check()
	return(s)


def decoder(data):
	decoded = ""
	blobs = data.split('\x00\x00\x00\x00')
	blobs = filter(lambda x: len(x) > 1000, blobs)

	done = False

	for encoded in blobs:
		#Try z3 solvers
		a = bytearray(encoded.lstrip('\x00'))
		for poss_decode in possible_decodes:
			s = solve_docdropper(a[:8], poss_decode)
			if s.check() == sat:
				m = s.model()
				for d in m.decls():
					if d.name() == 'xor_1':
						xor1_val = m[d].as_long()
					elif d.name() == 'xor_2':
						xor2_val = m[d].as_long()
					elif d.name() == 'xor_3':
						xor3_val = m[d].as_long()
					elif d.name() == 'xor_4':
						xor4_val = m[d].as_long()
				print("XOR1: "+hex(xor1_val))
				print("XOR2: "+hex(xor2_val))
				print("XOR3: "+hex(xor3_val))
				print("XOR4: "+hex(xor4_val))
				key = [xor1_val, xor2_val, xor3_val, xor4_val]
				for i in range(len(a)):
					temp = a[i] ^ key[i%len(key)]
					if temp < 0x20 or temp > 0x7e:
						break
					else:
						decoded += chr(temp)
	return decoded

if __name__ == "__main__":
	data = open(sys.argv[1],'rb').read()
	out = decoder(data)
	open(sys.argv[1]+'.decoded', 'wb').write(out)