[ Defenit CTF 2020 ] Lord fool song remix

you can look the main ft by Hex-ray...

There are two encrypt functions. I renamed these as "enc1" and "enc2".

However, enc2 function is just the printing algorithm. Before rip enter enc2, the encrypted memory had been written.

So I should analyze the enc1.

 

I looked the enc1 ft. by Hex-ray. But the code was too long and hard to understand. So, I debuged it and look memory carefully. 

enc1 ft have a 3part. First is the changing algorithm which change the input string to binary and record to allocated memory. 

Second part is the parseing and code obfusing part. In this part, the recorded memory(by first part) is parsed to 3. 

And third part is the encrypting part. By bitwise "xor", "and" ... the memory encryted. 

 

This python algorithm is the enc1's algorithm.

output = [638, 1004 ,829 ,320, 666, 526, 593, 247, 940, 790, 1023, 75, 240, 42, 1012, 326, 447, 261, 882 ,881]
b = [0]*200

for i in range(20):
    key = bin(output[i])[2:]
    key = "0" * (10 - len(key)) + key
    for j in range(10):
        b[10*i+j] = int(key[j])


#for i in range(20):
#    print(b[i*10:i*10+10])


stack1 = [0] * 200
stack2 = [0] * 200
stack3 = [0] * 200

input = "aaaabbbb\x00"
tmp = [0] * 72
for i in range(9):
    for j in range(8):
        t = bin(ord(input[i]))[2:]
        tmp[8*i+j] =  int(( "0"*(8-len(t)) + t )[j])

#print(tmp)
    
cnt = 0
for i in range(22,-1,-1):
    stack1[i] = tmp[cnt]
    cnt += 1


for i in range(23,-1,-1):
    stack2[i] = tmp[cnt]
    cnt += 1


for i in range(24,-1,-1):
    stack3[i] = tmp[cnt]
    cnt += 1

#stack ready fin
    
for i in range(23,200):
    stack1[i] = stack1[i-18] ^ stack1[i-23];

for i in range(3,179):
    tmp = stack2[i] ^ stack2[i+1] ^ stack2[i-2] ^ stack2[i-3]    
    stack2[i+21] = tmp
    

for i in range(25,200):
    stack3[i] = stack3[i-22] ^ stack3[i-25]



tmp1 = [0] * 4
tmp2 = [0] * 4
malloc = [0]*200
'''
for i in range(50):
    tmp1 = stack3[i*4:i*4+3]
    tmp2 = stack1[i*4:i*4+3]
    tmp3 = stack2[i*4:i*4+3]
    malloc[i*4:i*4+3] = ( tmp3 & (tmp1 ^ tmp2) ) ^ tmp1'''

for i in range(200):
    malloc[i] = (stack2[i] & (stack3[i]^stack1[i]))^stack3[i]

for i in range(50):
    print(malloc[i*4:i*4+4])

 

By using Z3-solver, I found the flag.

from z3 import*

s = Solver()
input = [BitVec('x{}'.format(i),8) for i in range(9)]

output = [638, 1004 ,829 ,320, 666, 526, 593, 247, 940, 790, 1023, 75, 240, 42, 1012, 326, 447, 261, 882 ,881]
b = [0]*200


for i in range(20):
    key = bin(output[i])[2:]
    key = "0" * (10 - len(key)) + key
    for j in range(10):
        b[10*i+j] = int(key[j])


#for i in range(20):
#    print(b[i*10:i*10+10])


stack1 = [0] * 200
stack2 = [0] * 200
stack3 = [0] * 200

#input = "aaaabbbb\x00"
tmp = [0] * 72
for i in range(9):
    for j in range(8):
        #t = bin(input[i])[2:]
        tmp[8*i+j] =  (input[i] & (2**(7-j))) >> (7-j) #int(( "0"*(8-len(t)) + t )[j])

print(tmp)
    
cnt = 0
for i in range(22,-1,-1):
    stack1[i] = tmp[cnt]
    cnt += 1


for i in range(23,-1,-1):
    stack2[i] = tmp[cnt]
    cnt += 1


for i in range(24,-1,-1):
    stack3[i] = tmp[cnt]
    cnt += 1

#stack ready fin
    
for i in range(23,200):
    stack1[i] = stack1[i-18] ^ stack1[i-23];

for i in range(3,179):
    tmp = stack2[i] ^ stack2[i+1] ^ stack2[i-2] ^ stack2[i-3]    
    stack2[i+21] = tmp
    
for i in range(25,200):
    stack3[i] = stack3[i-22] ^ stack3[i-25]


tmp1 = [0] * 4
tmp2 = [0] * 4
malloc = [0]*200

for i in range(200):
    malloc[i] = (stack2[i] & (stack3[i]^stack1[i]))^stack3[i]

#for i in range(50):
#    print(malloc[i*4:i*4+4])
    
for i in range(200):
    s.add(malloc[i] == b[i])

print(s.check())
print(s.model())

flag = "Defenit{"
for i in range(9):
    flag += chr(int(str(s.model()[input[i]])))
flag += "}"
print(flag)
'''
m = [0]*20
for i in range(20):
    tmp = 0
    for j in range(10):
        if malloc[10*i+(9-j)] == 1:
            tmp += 2**j
    
    m[i]= tmp
    #print(tmp,end=", ")

for i in range(9):
    s.add(m[i] == output[i])


#print(s.model())
'''

Defenit{g3ff3h0ly}