nkctf逆向

login_system

username用z3解方程，pass前一半异或解密 后一半标准aes换s盒

REEZ

看起来似乎是解密出了个文件，动调的时候在内存发现ELF头

dump出来后发现是关键部分的代码

第一步对输入进行了一大堆运算，第二步有个看不懂的加密，第三步异或后输出判断结果。直接用z3解了

#脚本来源：https://ycznkvrmzo.feishu.cn/docx/E92JdQmGxoUwXexnQgpcRaIsn7g

#!/usr/bin/env python3

'''
from Crypto.Cipher import ARC4

data = open('./REEZ', 'rb').read()[0x3070: 0x3070 + 0x3F50]
data = ARC4.new(b'do_you_like_what_you_see?').decrypt(data)

open('out', 'wb').write(data)
'''

from z3 import *
s = Solver()
x = [BitVec('x%d' % i, 8) for i in range(25)]
for i in x:
    s.add(i > 0)
    s.add(i < 0x7f)

input_inv = x[::-1]

input_inv[24] = -105 * (39 * (2 * (input_inv[24] & (-105 * (39 * (2 * (input_inv[13] & (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111)) + (input_inv[13] ^ (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111))) + 23) + 111)) + (input_inv[24] ^ (-105 * (39 * (2 * (input_inv[13] & (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111)) + (input_inv[13] ^ (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111))) + 23) + 111))) + 23) + 111
input_inv[23] = -105* (39* (2 * ((input_inv[11] ^ input_inv[10]) & input_inv[23])+ (input_inv[11] ^ input_inv[10] ^ input_inv[23]))+ 23)+ 111;
input_inv[22] = -105* (39* (2* (input_inv[22] & (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111))+ (input_inv[22] ^ (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111)))+ 23)+ 111;
input_inv[21] = -105* (39 * (2 * ((input_inv[7] ^ 0x17) & input_inv[21]) + (input_inv[7] ^ 0x17 ^ input_inv[21])) + 23)+ 111;
input_inv[20] = -105* (39* (2* (input_inv[20] & (-105* (39 * (2 * (input_inv[4] & (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111)) + (input_inv[4] ^ (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111))) + 23)+ 111))+ (input_inv[20] ^ (-105* (39 * (2 * (input_inv[4] & (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111)) + (input_inv[4] ^ (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111))) + 23)+ 111)))+ 23)+ 111;
input_inv[19] = -105* (39* (2 * (input_inv[19] & (~input_inv[1] + input_inv[3] + 1))+ (input_inv[19] ^ (~input_inv[1] + input_inv[3] + 1)))+ 23)+ 111;
input_inv[18] = -105* (39* (2* (input_inv[18] & (-105* (39 * (2 * (input_inv[16] & input_inv[17]) + (input_inv[16] ^ input_inv[17])) + 23)+ 111))+ (input_inv[18] ^ (-105* (39 * (2 * (input_inv[16] & input_inv[17]) + (input_inv[16] ^ input_inv[17])) + 23)+ 111)))+ 23)+ 111;
input_inv[17] = -105* (39* (2* (input_inv[17] & (-105* (39 * (2 * ((~input_inv[4] + input_inv[1] + 1) & 0x11) + ((~input_inv[4] + input_inv[1] + 1) ^ 0x11)) + 23)+ 111))+ (input_inv[17] ^ (-105* (39 * (2 * ((~input_inv[4] + input_inv[1] + 1) & 0x11) + ((~input_inv[4] + input_inv[1] + 1) ^ 0x11)) + 23)+ 111)))+ 23)+ 111;
input_inv[16] = -105* (39* (2* (input_inv[16] & (input_inv[5] ^ (-105 * (39 * (2 * (input_inv[6] & 1) + (input_inv[6] ^ 1)) + 23)+ 111)))+ (input_inv[16] ^ input_inv[5] ^ (-105 * (39 * (2 * (input_inv[6] & 1) + (input_inv[6] ^ 1)) + 23) + 111)))+ 23)+ 111;
input_inv[15] = ~input_inv[8]+ -105 * (39 * (2 * (input_inv[7] & input_inv[15]) + (input_inv[7] ^ input_inv[15])) + 23)+ 111+ 1;
input_inv[14] = -105* (39* (2* (input_inv[14] & (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111))+ (input_inv[14] ^ (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111)))+ 23)+ 111;
input_inv[13] = -105* (39* (2* (input_inv[12] & (-105* (39 * (2 * (input_inv[11] & (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111)) + (input_inv[11] ^ (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111))) + 23)+ 111))+ (input_inv[12] ^ (-105* (39 * (2 * (input_inv[11] & (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111)) + (input_inv[11] ^ (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111))) + 23)+ 111)))+ 23)+ 111;
input_inv[12] = -105 * (39 * (2 * (input_inv[12] & input_inv[13]) + (input_inv[12] ^ input_inv[13])) + 23) + 111;
input_inv[11] = -105* (39* (2 * (input_inv[11] & (input_inv[17] ^ input_inv[16]))+ (input_inv[11] ^ input_inv[17] ^ input_inv[16]))+ 23)+ 111;
input_inv[10] = -105* (39* (2* (input_inv[19] & (-105* (39 * (2 * (input_inv[20] & (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111)) + (input_inv[20] ^ (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111))) + 23)+ 111))+ (input_inv[19] ^ (-105* (39 * (2 * (input_inv[20] & (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111)) + (input_inv[20] ^ (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111))) + 23)+ 111)))+ 23)+ 111;
input_inv[9] = -105* (39* (2 * (input_inv[21] & (-105 * (39 * (2 * (input_inv[9] & 8) + (input_inv[9] ^ 8)) + 23) + 111))+ (input_inv[21] ^ (-105 * (39 * (2 * (input_inv[9] & 8) + (input_inv[9] ^ 8)) + 23) + 111)))+ 23)+ 111;
input_inv[8] = -105* (39 * (2 * ((input_inv[22] ^ 0x4D) & input_inv[8]) + (input_inv[22] ^ 0x4D ^ input_inv[8])) + 23)+ 111;
input_inv[7] = -105* (39* (2* (input_inv[7] & (-105 * (39 * (2 * ((input_inv[23] ^ 0x17) & 0xF9) + (input_inv[23] ^ 0xEE)) + 23) + 111))+ (input_inv[7] ^ (-105 * (39 * (2 * ((input_inv[23] ^ 0x17) & 0xF9) + (input_inv[23] ^ 0xEE)) + 23) + 111)))+ 23)+ 111;
input_inv[6] = -105* (39* (2 * ((input_inv[7] ^ input_inv[9]) & input_inv[6]) + (input_inv[7] ^ input_inv[9] ^ input_inv[6]))+ 23)+ 111;
input_inv[5] = -105* (39* (2* (input_inv[12] & (-105 * (39 * (2 * (input_inv[10] & input_inv[5]) + (input_inv[10] ^ input_inv[5])) + 23) + 111))+ (input_inv[12] ^ (-105 * (39 * (2 * (input_inv[10] & input_inv[5]) + (input_inv[10] ^ input_inv[5])) + 23) + 111)))+ 23)+ 111;
input_inv[4] = -105 * (39 * (2 * (input_inv[4] & input_inv[13]) + (input_inv[4] ^ input_inv[13])) + 23) + 111;
input_inv[3] = -105* (39* (2* (input_inv[16] & (-105 * (39 * (2 * (input_inv[3] & input_inv[18]) + (input_inv[3] ^ input_inv[18])) + 23) + 111))+ (input_inv[16] ^ (-105 * (39 * (2 * (input_inv[3] & input_inv[18]) + (input_inv[3] ^ input_inv[18])) + 23) + 111)))+ 23)+ 111;
input_inv[2] = -105 * (39 * (2 * (input_inv[19] & input_inv[2]) + (input_inv[19] ^ input_inv[2])) + 23) + 111;
input_inv[1] = -105* (39* (2 * ((input_inv[24] ^ input_inv[22]) & input_inv[1]) + (input_inv[24] ^ input_inv[22] ^ input_inv[1]))+ 23)+ 111;
input_inv[0] = -105* (39* (2 * (input_inv[0] & (-105 * (39 * (2 * (input_inv[23] & 0x18) + (input_inv[23] ^ 0x18)) + 23) + 111))+ (input_inv[0] ^ (-105 * (39 * (2 * (input_inv[23] & 0x18) + (input_inv[23] ^ 0x18)) + 23) + 111)))+ 23)+ 111;

input_inv = input_inv[::-1]

dword_2010 = [0, -2, -1, 4, 1, -1, 1, 0, 0, -1, -3, -2, 0, -0xA, -1, -1, -2, 1, -0xD, -1, -6, -1, -2, 1, -2]
out = [0] * 25

for a in range(5):
    for b in range(5):
        v13 = 0
        for c in range(5):
            v3 = dword_2010[5 * a + c] * input_inv[5 * c + b]
            v13 = -105 * (39 * (2 * (v13 & v3) + (v13 ^ v3)) + 23) + 111
        out[5 * a + b] = v13

result1 = bytes.fromhex('3244AA56633D2B09CD34993C56B899DE261F7E0B42C21BEBF5')
result2 = b'D0_y0u_Like_What_You_See?'
for i in range(25):
    s.add(out[i] == result1[i] ^ result2[i])

assert s.check() == sat
model = s.model()
flag = bytes([model[i].as_long() for i in x])
print(flag)

# NKCTF{THut_1Ss_s@_eAsyhh}

唯一值得注意的就是在第一步变换完后依次存到了v45[*+1]的位置，然后v45[*+33]的位置存储的是经过第二步变换的结果（矩阵加密）

inputtttt

放到下一篇