Reverse Engineering

Challenge	Link
Free Play (495 points)	Here

Free Play (495 points)

Description

-

PoC

• At initial, we try to decompile using ghidra plugin but it fail, also we can't do decompile and converting to wat using wasm2c and wasm2wat

• We found the solution , we set --enable-threads to convert the file to wat

• There is a binary that can convert wat to wasm, so using this approach we try to patch some instruction so we can compiel the wat to wasm and decompile it using ghidra plugin/wasm2c/wasm-decompile

• There are some instruction that can't be converted , so my approach is trying to replacing the instruction and then compile again

• here is the patched main.wat

• After that just open it on ghidra , here is the example of opening checkFlag function on ghidra

• During the competition we use chrome to do dynamic analysis , such as inspecting the value on memory, stack , and register value.

• Here is an example when we try to inspecting the value on stack/argument for func46 which is address of memory

• Here is when we try to inspecting value on address 63984

• Last part before creating the solver, we try to reconstruct the algorithm in python. Here is reconstructed algorithm in python

from Crypto.Util.number import *

def bits_on_count(x):
  return sum(c=='1' for c in bin(x))

def split_bytes(inp):
	return [(inp>>24)&0xff, (inp>>16)&0xff, (inp>>8)&0xff, inp&0xff]

def func_41(list_dec):
	for i in range(0x40): 
		assert(bits_on_count(list_dec[i]) == 0x20)

def func_42(list_dec):
	for i in range(0,0x40,2):
		assert(list_dec[i] != list_dec[i+1])

def func_44(list_dec):
	for i in range(0,4*3,4):
		first = list_dec[i:i+4]
		res_var = []
		for j in first: # ( ~val & (~val >> 1) ) & (~val >> 2)
			not_var = ~j&0xffffffff
			tmp1 = (not_var >> 1) & not_var
			tmp2 = not_var >> 2 
			assert((tmp1 & tmp2) == 0)

def func_43(list_dec):
	for i in range(0,4*3,4):
		first = list_dec[i:i+4]
		res_var = []
		for j in first: # ( val & (val >> 1) ) & (val >> 2)
			not_var = j&0xffffffff
			tmp1 = (not_var >> 1) & not_var
			tmp2 = not_var >> 2 
			assert((tmp1 & tmp2) == 0)

# a var should be static
a = [-128,122,-120,40,93,-25,36,112,54,-48,106,-70,-85,45,29,-43,-122,85,50,-7,83,-88,-8,-41,-55,-43,115,14,79,-108,-119,8,-107,20,127,-101,-77,107,37,32,61,-19,-97,104,8,83,-94,43,-116,-93,6,95,-18,82,110,-14,63,89,-64,-25,70,-14,78,101,64,0,91,84,-103,60,64,37,-11,-4,-10,117,-3,-37,-64,37,-22,45,1,-10,3,15,-42,-107,-128,-91,-104,-63,-113,82,11,-37,42,-50,56,-20,-62,89,-5,5,14,-12,121,47,-128,39,32,105,-54,43,72,14,-8,-33,-71,-98,59,105,-34,-1,103,-49,-102,-91,20,-6,-28,96,-81,92,-76,-93,-6,-17,120,-53,18,72,-28,48,80,98,114,-79,111,-6,89,6,103,-94,-46,-98,95,-3,25,-86,73,127,-91,42,-26,6,-49,-13,26,-122,60,-79,112,-92,-55,53,-23,-110,-20,-105,-57,4,-81,36,81,-23,56,118,87,-115,106,68,-10,-41,33,94,-83,-17,-16,-108,1,123,-91,-77,57,90,-128,-108,105,-9,58,-128,-57,-90,27,-38,-77,26,10,-52,-23,44,30,-46,84,14,22,14,101,42,3,98,-78,86,88,126,-26,16,-106,-43,76,-26,101,45,31,48,59,9,92,8,-108,-61,54,63,-71,51,11,16,85,33,-56,66,65,64,36,-83,1,-110,98,82,2,64,18,64,18,1,-127,0,5,-86,69,72,-116,-76,40,50,106,64,41,-80,82,2,6,0,49,66,18,73,0,75,-120,-106,-52,0,3,-125,32,36,0,34,10,20,-64,96,0,1,96]

ct = [84, 195, 224, 136, 93, 57, 235, 173, 225, 212, 195, 104, 179, 158, 23, 197, 133, 34, 93, 247, 16, 140, 227, 165, 123, 170, 183, 195, 106, 176, 86, 205, 82, 51, 212, 85, 181, 100, 52, 52, 144, 87, 159, 183, 230, 119, 44, 193, 114, 56, 45, 56, 233, 204, 145, 64, 15, 242, 122, 135, 210, 22, 166, 104, 188, 243, 56, 245, 88, 226, 27, 186, 180, 174, 234, 198, 200, 188, 80, 253, 137, 46, 230, 197, 12, 247, 172, 70, 160, 159, 248, 147, 2, 244, 235, 191, 39, 134, 233, 159, 113, 213, 167, 214, 127, 46, 88, 152, 24, 25, 2, 29, 132, 103, 113, 221, 206, 41, 88, 28, 117, 126, 74, 82, 238, 161, 175, 253, 151, 138, 83, 166, 224, 26, 80, 98, 24, 120, 17, 38, 243, 100, 8, 106, 236, 108, 74, 106, 166, 55, 222, 87, 131, 231, 244, 9, 124, 10, 123, 241, 193, 160, 68, 160, 177, 233, 135, 96, 92, 117, 151, 56, 245, 117, 79, 147, 242, 132, 24, 90, 175, 202, 29, 157, 231, 205, 132, 97, 170, 230, 82, 106, 206, 111, 107, 129, 190, 49, 243, 97, 114, 95, 116, 221, 60, 59, 224, 212, 175, 235, 201, 255, 29, 75, 25, 153, 43, 208, 138, 111, 1, 197, 216, 124, 76, 125, 27, 190, 140, 188, 129, 127, 77, 9, 84, 252, 155, 239, 97, 85, 76, 216, 133, 191, 73, 96, 212, 71, 163, 143, 50, 103, 12, 251, 28, 214]
# shift_val should be static
shift_val = [11,16,85,33,-56,66,65,64,36,-83,1,-110,98,82,2,64,18,64,18,1,-127,0,5,-86,69,72,-116,-76,40,50,106,64,41,-80,82,2,6,0,49,66,18,73,0,75,-120,-106,-52,0,3,-125,32,36,0,34,10,20,-64,96,0,1,96,0,0,0,72,-126,69,68,-120,33,8,74,1,66,-94,0,25,-48,-78,-91,-96,12,8,-104,0,0,1,2,-126,16,20,36,8,1,48,8,52,0,-88,17,68,86,1,32,33,-124,4,2,-119,64,5,36,74,-61,16,4,33,-96,36,26,100,42,8,-61,50,8,-120,38,-128,-128,4,66,-111,-128,-56,32,-108,4,8,32,8,8,52,16,66,106,4,0,48,-95,-80,98,-123,50,0,66,12,4,11,26,0,0,36,16,72,9,17,0,2,67,0,84,-76,-80,72,1,-107,-91,17,1,0,16,37,-96,74,82,82,-104,2,10,-119,-112,-96,-96,37,-96,-92,-96,12,10,1,4,26,34,1,-109,96,25,26,-110,4,-123,-128,68,-111,20,12,21,16,16,13,-47,0,41,-111,42,6,100,8,49,-104,-127,2,9,40,-125,-112,72,5,-128,33,32,-64,104,96,2,-64,2,-124,-96,44,-63,10,-111,32,-119,88,80,1,-76,80,-112,18,0,-104,-124,80,4,-120,8,105,108,-92,1,1,-120,12,72,3,68,8,-126,-122,-64,-112,64,12,0,17,4,-122,36,32,8,32,2,6,-124,40,0,-124,4,-126,-87,32,88,2,0,8,10,-108,69,-110,-119,4,8,-128,53,105,-120,64,-126,-124,0,17,74,44,4,4,12,-119,73,2,-103,-126,26,4,-128,100,22,16,64,-112,1,73,96,8,68,54,73,11,1,25,0,38,2,36,-128,68,-124,32,37,-112,16,10,96,4,73,2,0,64,36,37,80,64,-128,0,4,40,75,0,-108,-96,36,1,-88,20,4,0,104,-106,8,16,16,17,108,0,18,8,32,-95,44,64,0,18,-90,76,80,20,-112,37,-76,8,9,18,42,18,-128,68,1,4,34,20,0,73,50,-119,26,-96,-127,32,75,-109,96,6,100,-39,34,36,9,0,73,64,-104,33,65,-117,52,3,33,-112,44,-112,4,32,33,-112,-96,16,68,-128,-120,89,-111,-96,20,40,0,10,10,88,20,34,8,9,-79,-95,0,-92,0,25,-92,-111,96,-74,2,0,1,48,8,22,-128,73,-128,80,32,64,-106,34,-127,20,-112,1,32,32,6,77,2,17,22,26,20,-32,45,-86,-114,35,-87,-82,20,-63,2,-40,37,-100,-119,-7,27,-24,-77,44,-38,120,-9,-24,17,-86,-111,115,3,85,-128,-111,-99,-42,77,-87,-15,-48,105,74,-99,109,-122,119,-124,55,97,49,-67,108,24,-35,-127,-97,-40,-28,75,31,-98,95,-2,-98,127,-97,-34,51,117,-86,58,82,70,101,33,118,-67,28,-5,-58,39,0,74,95,114,99,102,47,-37,-6,-12,88,-17,-119,-47,113,-12,14,-43,-120,-5,87,68,-110,33,108,-42,-114,32,112,93,118,31,-102,-126,53,28,-123,-78,76,79,-109,97,-103,84,-29,60,-124,-93,83,8,90,60,-101,53,104,94,21,-44,107,-101,-11,-33,68,101,-63,-49,56,21,35,-5,-57,26,11,13,58,77,-7,-92,-79,-69,116,-124,-106,-35,-118,-17,-78,-48,-26,-65,-35,44,-9,-117,2,70,-74,-2,104,74,108,-2,-51,-113,-112,83,-75,-95,13,101,-3,116,118,111,79,12,-64,22,74,20,-31,112,-76,-55,100,-55,-24,12,14,-60,69,97,-5,26,26,43,40,-93,97,-62,102,-81,-14,12,-2,-48,46,80,-88,-110,-105,-122,35,20,-35,86,-57,84,42,55,98,91,90,-121,59,-105,-99,100,31,-3,122,76,-46,42,-80,78,-108,112,-89,39,-40,10,39,10,-20,-105,103,99,14,99,37,-27,6,1,82,46,110,66,-80,-89,88,51,-13,124,49,23,66,-106,-13,-97,-18,121,49,-56,-37,-105,93,-35,-112,99,87,-17,105,-22,92,68,-51,-89,-3,-43,-79,-43,74,-110,9,116,83,85,126,64,16,35,-65,45,98,-6,68,-76,-64,-23,-31,96,50,-124,-24,38,116,68,107,95,24,97,-81,63,5,-90,-106,23,-73,-86,-55,-90,36,-50,-32,82,-39,121,-39,26,26,59,-42,-118,39,77,-11,7,-71,34,-3,41,-97,-40,-118,47,41,119,-7,-14,71,-76,-21,40,78,91,78,3,-21,-112,-1,-123,8,-25,-21,103,-50,-109,119,72,103,-42,92,-61,-69,-37,-63,24,-77,7,-54,103,-102,9,-12,-14,-23,-59,-20,95,-78,116,-29,77,-54,37,-128,76,66,-28,90,116,95,-76,12,-116,-103,-128,2,-107,-117,116,-76,-94,-74,71,-52,30,116,-118,-8,-34,45,-64,71,-21,15,72,74,94,-92,-112,63,82,-96,78,84,-23,-46,107,-44,113,-121,106,-39,-105,-10,6,12,-1,81,57,66,67,6,-117,64,121,61,-6,-58,-45,-120,125,52,38,-118,92,-119,73,-36,116,-86,75,124,27,-105,-95,0,-23,-22,96,-28,-117,-18,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

# check_val should be static
check_val = [-32,45,-86,-114,35,-87,-82,20,-63,2,-40,37,-100,-119,-7,27,-24,-77,44,-38,120,-9,-24,17,-86,-111,115,3,85,-128,-111,-99,-42,77,-87,-15,-48,105,74,-99,109,-122,119,-124,55,97,49,-67,108,24,-35,-127,-97,-40,-28,75,31,-98,95,-2,-98,127,-97,-34,51,117,-86,58,82,70,101,33,118,-67,28,-5,-58,39,0,74,95,114,99,102,47,-37,-6,-12,88,-17,-119,-47,113,-12,14,-43,-120,-5,87,68,-110,33,108,-42,-114,32,112,93,118,31,-102,-126,53,28,-123,-78,76,79,-109,97,-103,84,-29,60,-124,-93,83,8,90,60,-101,53,104,94,21,-44,107,-101,-11,-33,68,101,-63,-49,56,21,35,-5,-57,26,11,13,58,77,-7,-92,-79,-69,116,-124,-106,-35,-118,-17,-78,-48,-26,-65,-35,44,-9,-117,2,70,-74,-2,104,74,108,-2,-51,-113,-112,83,-75,-95,13,101,-3,116,118,111,79,12,-64,22,74,20,-31,112,-76,-55,100,-55,-24,12,14,-60,69,97,-5,26,26,43,40,-93,97,-62,102,-81,-14,12,-2,-48,46,80,-88,-110,-105,-122,35,20,-35,86,-57,84,42,55,98,91,90,-121,59,-105,-99,100,31,-3,122,76,-46,42,-80,78,-108,112,-89,39,-40,10,39,10,-20,-105,103,99,14,99,37,-27,6,1,82,46,110,66,-80,-89,88,51,-13,124,49,23,66,-106,-13,-97,-18,121,49,-56,-37,-105,93,-35,-112,99,87,-17,105,-22,92,68,-51,-89,-3,-43,-79,-43,74,-110,9,116,83,85,126,64,16,35,-65,45,98,-6,68,-76,-64,-23,-31,96,50,-124,-24,38,116,68,107,95,24,97,-81,63,5,-90,-106,23,-73,-86,-55,-90,36,-50,-32,82,-39,121,-39,26,26,59,-42,-118,39,77,-11,7,-71,34,-3,41,-97,-40,-118,47,41,119,-7,-14,71,-76,-21,40,78,91,78,3,-21,-112,-1,-123,8,-25,-21,103,-50,-109,119,72,103,-42,92,-61,-69,-37,-63,24,-77,7,-54,103,-102,9,-12,-14,-23,-59,-20,95,-78,116,-29,77,-54,37,-128,76,66,-28,90,116,95,-76,12,-116,-103,-128,2,-107,-117,116,-76,-94,-74,71,-52,30,116,-118,-8,-34,45,-64,71,-21,15,72,74,94,-92,-112,63,82,-96,78,84,-23,-46,107,-44,113,-121,106,-39,-105,-10,6,12,-1,81,57,66,67,6,-117,64,121,61,-6,-58,-45,-120,125,52,38,-118,92,-119,73,-36,116,-86,75,124,27,-105,-95,0,-23,-22,96,-28,-117,76]

xor_val = []
for i in a:
	xor_val.append(i&0xff)

shift_val_2 = []
for i in shift_val:
	shift_val_2.append(i&0xff)

check_val_2 = []
for i in check_val:
	check_val_2.append(i&0xff)

res = []
for i in range(len(ct)):
	res.append(ct[i]^xor_val[i])

list_dec = []
for i in range(0,8*0x40,8):
	tmp = bytes(shift_val_2[i:i+8])[::-1]
	list_dec.append(bytes_to_long(tmp))

list_check = []
for i in range(0,8*0x40,8):
	tmp = bytes(check_val_2[i:i+8])[::-1]
	list_check.append(bytes_to_long(tmp))

local_620 = 0
for i in range(0x40):
	for j in range(0x40):
		if( ((list_check[i] >> ((0x3f - j) & 0x3f)) & 1 ) != 0):
			tmp = ((res[local_620 >> 3] >> (7 - ((local_620 & 7) & 0x1f ))) & 1 )
			www = ((0x3f - j) & 0x3f)
			tmp <<= www
			list_dec[i] |= tmp
			local_620 += 1


list_dec_2 = [0 for _ in range(0x40)]

for i in range(0x40):
	for j in range(0x40):
		list_dec_2[i] <<= 1
		list_dec_2[i] |= (list_dec[j] >> ((0x3f - i) & 0x3f)) & 1

bytes_dec = []
bytes_dec_2 = []

for i in list_dec:
	tmp = long_to_bytes(i)[::-1]
	for j in tmp:
		bytes_dec.append(j)

for i in list_dec_2:
	tmp = long_to_bytes(i)[::-1]
	for j in tmp:
		bytes_dec_2.append(j)

list_42 = []
list_42_2 = []

for i in range(len(list_dec)):
	first = list_dec[i]&0xffffffff
	second = list_dec[i]>>32
	first_2 = list_dec_2[i]&0xffffffff
	second_2 = list_dec_2[i]>>32
	list_42.append(first)
	list_42.append(second)
	list_42_2.append(first_2)
	list_42_2.append(second_2)

func_41(list_dec)
func_41(list_dec_2)
func_42(list_dec)
func_42(list_dec_2)
func_44(list_42)
func_44(list_42_2)
func_43(list_42)
func_43(list_42_2)

• After reconstructing the process the last step is solving it using z3, but in this case we failed to find the flag and the algorithm is weird because its only check partial of value not all.

• But after opening ticket we found that there is an issue from the challenge, so by changing the loop to check all the values we got the flag.

• Here is the final script we used

from Crypto.Util.number import *
from z3 import *
from functools import reduce
from Crypto.Cipher import AES

def sub(b):
    n = b.size()
    bits = [ Extract(i, i, b) for i in range(n) ]
    bvs  = [ Concat(BitVecVal(0, n - 1), b) for b in bits ]
    nb   = reduce(lambda a, b: a + b, bvs)
    return nb

def func_41(list_dec):
	for i in range(0x40):
		s.add(sub(list_dec[i]) == 0x20)
		s.add(sub(list_dec_2[i]) == 0x20)

def func_42(list_dec):
	for i in range(0,0x40,2):
		s.add(list_dec[i] != list_dec[i+1])

def func_44(list_dec):
	for i in range(len(list_dec)):
		not_var = ~(list_dec[i])
		tmp1 = LShR(not_var , 1) & not_var
		tmp2 = LShR(not_var, 2)
		s.add((tmp1 & tmp2) == 0) # 0xD422EB74 >> 1 == 0xEA1175BA weird of unsigned


def func_43(list_dec):
	for i in range(len(list_dec)):
		not_var = list_dec[i]
		tmp1 = LShR(not_var , 1) & not_var
		tmp2 = LShR(not_var, 2)
		s.add((tmp1 & tmp2) == 0) # 0xD422EB74 >> 1 == 0xEA1175BA weird of unsigned

a = [-128,122,-120,40,93,-25,36,112,54,-48,106,-70,-85,45,29,-43,-122,85,50,-7,83,-88,-8,-41,-55,-43,115,14,79,-108,-119,8,-107,20,127,-101,-77,107,37,32,61,-19,-97,104,8,83,-94,43,-116,-93,6,95,-18,82,110,-14,63,89,-64,-25,70,-14,78,101,64,0,91,84,-103,60,64,37,-11,-4,-10,117,-3,-37,-64,37,-22,45,1,-10,3,15,-42,-107,-128,-91,-104,-63,-113,82,11,-37,42,-50,56,-20,-62,89,-5,5,14,-12,121,47,-128,39,32,105,-54,43,72,14,-8,-33,-71,-98,59,105,-34,-1,103,-49,-102,-91,20,-6,-28,96,-81,92,-76,-93,-6,-17,120,-53,18,72,-28,48,80,98,114,-79,111,-6,89,6,103,-94,-46,-98,95,-3,25,-86,73,127,-91,42,-26,6,-49,-13,26,-122,60,-79,112,-92,-55,53,-23,-110,-20,-105,-57,4,-81,36,81,-23,56,118,87,-115,106,68,-10,-41,33,94,-83,-17,-16,-108,1,123,-91,-77,57,90,-128,-108,105,-9,58,-128,-57,-90,27,-38,-77,26,10,-52,-23,44,30,-46,84,14,22,14,101,42,3,98,-78,86,88,126,-26,16,-106,-43,76,-26,101,45,31,48,59,9,92,8,-108,-61,54,63,-71,51,11,16,85,33,-56,66,65,64,36,-83,1,-110,98,82,2,64,18,64,18,1,-127,0,5,-86,69,72,-116,-76,40,50,106,64,41,-80,82,2,6,0,49,66,18,73,0,75,-120,-106,-52,0,3,-125,32,36,0,34,10,20,-64,96,0,1,96]

shift_val = [11,16,85,33,-56,66,65,64,36,-83,1,-110,98,82,2,64,18,64,18,1,-127,0,5,-86,69,72,-116,-76,40,50,106,64,41,-80,82,2,6,0,49,66,18,73,0,75,-120,-106,-52,0,3,-125,32,36,0,34,10,20,-64,96,0,1,96,0,0,0,72,-126,69,68,-120,33,8,74,1,66,-94,0,25,-48,-78,-91,-96,12,8,-104,0,0,1,2,-126,16,20,36,8,1,48,8,52,0,-88,17,68,86,1,32,33,-124,4,2,-119,64,5,36,74,-61,16,4,33,-96,36,26,100,42,8,-61,50,8,-120,38,-128,-128,4,66,-111,-128,-56,32,-108,4,8,32,8,8,52,16,66,106,4,0,48,-95,-80,98,-123,50,0,66,12,4,11,26,0,0,36,16,72,9,17,0,2,67,0,84,-76,-80,72,1,-107,-91,17,1,0,16,37,-96,74,82,82,-104,2,10,-119,-112,-96,-96,37,-96,-92,-96,12,10,1,4,26,34,1,-109,96,25,26,-110,4,-123,-128,68,-111,20,12,21,16,16,13,-47,0,41,-111,42,6,100,8,49,-104,-127,2,9,40,-125,-112,72,5,-128,33,32,-64,104,96,2,-64,2,-124,-96,44,-63,10,-111,32,-119,88,80,1,-76,80,-112,18,0,-104,-124,80,4,-120,8,105,108,-92,1,1,-120,12,72,3,68,8,-126,-122,-64,-112,64,12,0,17,4,-122,36,32,8,32,2,6,-124,40,0,-124,4,-126,-87,32,88,2,0,8,10,-108,69,-110,-119,4,8,-128,53,105,-120,64,-126,-124,0,17,74,44,4,4,12,-119,73,2,-103,-126,26,4,-128,100,22,16,64,-112,1,73,96,8,68,54,73,11,1,25,0,38,2,36,-128,68,-124,32,37,-112,16,10,96,4,73,2,0,64,36,37,80,64,-128,0,4,40,75,0,-108,-96,36,1,-88,20,4,0,104,-106,8,16,16,17,108,0,18,8,32,-95,44,64,0,18,-90,76,80,20,-112,37,-76,8,9,18,42,18,-128,68,1,4,34,20,0,73,50,-119,26,-96,-127,32,75,-109,96,6,100,-39,34,36,9,0,73,64,-104,33,65,-117,52,3,33,-112,44,-112,4,32,33,-112,-96,16,68,-128,-120,89,-111,-96,20,40,0,10,10,88,20,34,8,9,-79,-95,0,-92,0,25,-92,-111,96,-74,2,0,1,48,8,22,-128,73,-128,80,32,64,-106,34,-127,20,-112,1,32,32,6,77,2,17,22,26,20,-32,45,-86,-114,35,-87,-82,20,-63,2,-40,37,-100,-119,-7,27,-24,-77,44,-38,120,-9,-24,17,-86,-111,115,3,85,-128,-111,-99,-42,77,-87,-15,-48,105,74,-99,109,-122,119,-124,55,97,49,-67,108,24,-35,-127,-97,-40,-28,75,31,-98,95,-2,-98,127,-97,-34,51,117,-86,58,82,70,101,33,118,-67,28,-5,-58,39,0,74,95,114,99,102,47,-37,-6,-12,88,-17,-119,-47,113,-12,14,-43,-120,-5,87,68,-110,33,108,-42,-114,32,112,93,118,31,-102,-126,53,28,-123,-78,76,79,-109,97,-103,84,-29,60,-124,-93,83,8,90,60,-101,53,104,94,21,-44,107,-101,-11,-33,68,101,-63,-49,56,21,35,-5,-57,26,11,13,58,77,-7,-92,-79,-69,116,-124,-106,-35,-118,-17,-78,-48,-26,-65,-35,44,-9,-117,2,70,-74,-2,104,74,108,-2,-51,-113,-112,83,-75,-95,13,101,-3,116,118,111,79,12,-64,22,74,20,-31,112,-76,-55,100,-55,-24,12,14,-60,69,97,-5,26,26,43,40,-93,97,-62,102,-81,-14,12,-2,-48,46,80,-88,-110,-105,-122,35,20,-35,86,-57,84,42,55,98,91,90,-121,59,-105,-99,100,31,-3,122,76,-46,42,-80,78,-108,112,-89,39,-40,10,39,10,-20,-105,103,99,14,99,37,-27,6,1,82,46,110,66,-80,-89,88,51,-13,124,49,23,66,-106,-13,-97,-18,121,49,-56,-37,-105,93,-35,-112,99,87,-17,105,-22,92,68,-51,-89,-3,-43,-79,-43,74,-110,9,116,83,85,126,64,16,35,-65,45,98,-6,68,-76,-64,-23,-31,96,50,-124,-24,38,116,68,107,95,24,97,-81,63,5,-90,-106,23,-73,-86,-55,-90,36,-50,-32,82,-39,121,-39,26,26,59,-42,-118,39,77,-11,7,-71,34,-3,41,-97,-40,-118,47,41,119,-7,-14,71,-76,-21,40,78,91,78,3,-21,-112,-1,-123,8,-25,-21,103,-50,-109,119,72,103,-42,92,-61,-69,-37,-63,24,-77,7,-54,103,-102,9,-12,-14,-23,-59,-20,95,-78,116,-29,77,-54,37,-128,76,66,-28,90,116,95,-76,12,-116,-103,-128,2,-107,-117,116,-76,-94,-74,71,-52,30,116,-118,-8,-34,45,-64,71,-21,15,72,74,94,-92,-112,63,82,-96,78,84,-23,-46,107,-44,113,-121,106,-39,-105,-10,6,12,-1,81,57,66,67,6,-117,64,121,61,-6,-58,-45,-120,125,52,38,-118,92,-119,73,-36,116,-86,75,124,27,-105,-95,0,-23,-22,96,-28,-117,-18,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

check_val = [-32,45,-86,-114,35,-87,-82,20,-63,2,-40,37,-100,-119,-7,27,-24,-77,44,-38,120,-9,-24,17,-86,-111,115,3,85,-128,-111,-99,-42,77,-87,-15,-48,105,74,-99,109,-122,119,-124,55,97,49,-67,108,24,-35,-127,-97,-40,-28,75,31,-98,95,-2,-98,127,-97,-34,51,117,-86,58,82,70,101,33,118,-67,28,-5,-58,39,0,74,95,114,99,102,47,-37,-6,-12,88,-17,-119,-47,113,-12,14,-43,-120,-5,87,68,-110,33,108,-42,-114,32,112,93,118,31,-102,-126,53,28,-123,-78,76,79,-109,97,-103,84,-29,60,-124,-93,83,8,90,60,-101,53,104,94,21,-44,107,-101,-11,-33,68,101,-63,-49,56,21,35,-5,-57,26,11,13,58,77,-7,-92,-79,-69,116,-124,-106,-35,-118,-17,-78,-48,-26,-65,-35,44,-9,-117,2,70,-74,-2,104,74,108,-2,-51,-113,-112,83,-75,-95,13,101,-3,116,118,111,79,12,-64,22,74,20,-31,112,-76,-55,100,-55,-24,12,14,-60,69,97,-5,26,26,43,40,-93,97,-62,102,-81,-14,12,-2,-48,46,80,-88,-110,-105,-122,35,20,-35,86,-57,84,42,55,98,91,90,-121,59,-105,-99,100,31,-3,122,76,-46,42,-80,78,-108,112,-89,39,-40,10,39,10,-20,-105,103,99,14,99,37,-27,6,1,82,46,110,66,-80,-89,88,51,-13,124,49,23,66,-106,-13,-97,-18,121,49,-56,-37,-105,93,-35,-112,99,87,-17,105,-22,92,68,-51,-89,-3,-43,-79,-43,74,-110,9,116,83,85,126,64,16,35,-65,45,98,-6,68,-76,-64,-23,-31,96,50,-124,-24,38,116,68,107,95,24,97,-81,63,5,-90,-106,23,-73,-86,-55,-90,36,-50,-32,82,-39,121,-39,26,26,59,-42,-118,39,77,-11,7,-71,34,-3,41,-97,-40,-118,47,41,119,-7,-14,71,-76,-21,40,78,91,78,3,-21,-112,-1,-123,8,-25,-21,103,-50,-109,119,72,103,-42,92,-61,-69,-37,-63,24,-77,7,-54,103,-102,9,-12,-14,-23,-59,-20,95,-78,116,-29,77,-54,37,-128,76,66,-28,90,116,95,-76,12,-116,-103,-128,2,-107,-117,116,-76,-94,-74,71,-52,30,116,-118,-8,-34,45,-64,71,-21,15,72,74,94,-92,-112,63,82,-96,78,84,-23,-46,107,-44,113,-121,106,-39,-105,-10,6,12,-1,81,57,66,67,6,-117,64,121,61,-6,-58,-45,-120,125,52,38,-118,92,-119,73,-36,116,-86,75,124,27,-105,-95,0,-23,-22,96,-28,-117,76]

ct = [BitVec("ct_{}".format(i), 64) for i in range(256)]

s = Solver()

for i in range(256):
	s.add(ct[i]&0xff < 256)

xor_val = []
for i in a:
	xor_val.append(i&0xff)

shift_val_2 = []
for i in shift_val:
	shift_val_2.append(i&0xff)

check_val_2 = []
for i in check_val:
	check_val_2.append(i&0xff)

res = []
for i in range(len(ct)):
	res.append(ct[i]^xor_val[i])

list_dec = []
for i in range(0,8*0x40,8):
	tmp = bytes(shift_val_2[i:i+8])[::-1]
	list_dec.append(BitVecVal(bytes_to_long(tmp),64))

list_check = []
for i in range(0,8*0x40,8):
	tmp = bytes(check_val_2[i:i+8])[::-1]
	list_check.append(bytes_to_long(tmp))

local_620 = 0
for i in range(0x40):
	for j in range(0x40):
		if( ((list_check[i] >> ((0x3f - j) & 0x3f)) & 1 ) != 0):
			tmp = (LShR(res[local_620 >> 3],(7 - ((local_620 & 7) & 0x1f ))) & 1 )
			www = ((0x3f - j) & 0x3f)
			tmp <<= www
			list_dec[i] |= tmp
			local_620 += 1

list_dec_2 = [BitVecVal(0,64) for _ in range(0x40)]

for i in range(0x40):
	for j in range(0x40):
		list_dec_2[i] <<= 1
		list_dec_2[i] |= LShR(list_dec[j] , ((0x3f - i) & 0x3f)) & 1

func_41(list_dec)
func_41(list_dec_2)
func_42(list_dec)
func_42(list_dec_2)
func_44(list_dec)
func_44(list_dec_2)
func_43(list_dec)
func_43(list_dec_2)

print(s.check())

key = bytes([202, 102, 28, 101, 4, 34, 8, 203, 208, 209, 107, 44, 182, 218, 153, 203])
iv = bytes([81, 62, 98, 66, 69, 240, 205, 237, 65, 41, 101, 220, 140, 39, 27, 180])

model = s.model()
list_ct = []
for x in ct:
    list_ct.append(model[x].as_long()&0xff)
result = bytes(list_ct)
cipher = AES.new(key, AES.MODE_CBC, iv)
print(f"CT value : {result.hex()}")
print(f"Flag : {cipher.decrypt(result)}")

• Flag : HackTM{bee3dc52aabec5c1b673d8d2beaeef64fbbf94fbbfe3f7ebcf716e465bd7af2a609a0be0717f6bcbed7c33dcfc95aadaae2f3e046a3b1ee42dbfb7da3687d77fbece4d957b48c3c3fa00d77da8aeffdedbe823bbc89678ded4bfe9f71fdcbf8c9cbd8b84ebffb118eb68b39bee0bfeccd07efbf8cd530b2dadbff4af}