2024NKCTFREEZ

0x00 分析题目

和上一道题一样大部分还是用Z3

不过这道题会动态输出一个可执行文件，有点类似于SMC了

0x01 解

ELF，无壳

直接上IDA

没有cmp，而这个byte_404070里面的内容很多

应该是类似于SMC那样会输出一个可执行文件，而这些应该就是操作码

试着运行一下

这时候会输出一个outputfile

直接拷走就行（

来到outputfile的main里面，可以发现整个程序的加密可以被分为三个操作

第一部分是一大堆加减乘除和位运算

第二部分是和内存里的某个东西（dword_55FA1FBB2010）进行乘除以及位运算

第三部分就是一个简单的异或

将byte_55FA1FBB2080与第二部分的结果异或然后与byte_55FA1FBB20A0进行比较

那么就该REVERSE了

先从最后的开始，直接异或得出第二部分的结果

key = [0x32, 0x44, 0xaa, 0x56, 0x63, 0x3d, 0x2b, 0x09, 0xcd, 0x34, 0x99, 0x3c,
       0x56, 0xb8, 0x99, 0xde, 0x26, 0x1f, 0x7e, 0x0b, 0x42, 0xc2, 0x1b, 0xeb, 0xf5]
enc = [0x44, 0x30, 0x5f, 0x79, 0x30, 0x75, 0x5f, 0x4c, 0x69, 0x6b, 0x65, 0x5f,
       0x57, 0x68, 0x61, 0x74, 0x5f, 0x59, 0x6f, 0x75, 0x5f, 0x53, 0x65, 0x65, 0x3f]
dec = []
for i in range(len(enc)):
    dec.append(key[i] ^ enc[i])
    print('0x{:02x}'.format(dec[i]), end=', ')

# dec = [0x76, 0x74, 0xf5, 0x2f, 0x53, 0x48, 0x74, 0x45, 0xa4, 0x5f, 0xfc, 0x63, 0x01, 0xd0, 0xf8, 0xaa, 0x79, 0x46, 0x11, 0x7e, 0x1d, 0x91, 0x7e, 0x8e, 0xca]

然后是第二部分，用Z3操作一下可以得出第一部分的结果

from z3 import *
enc1 = [0x76, 0x74, 0xf5, 0x2f, 0x53, 0x48, 0x74, 0x45, 0xa4, 0x5f, 0xfc, 0x63,
        0x01, 0xd0, 0xf8, 0xaa, 0x79, 0x46, 0x11, 0x7e, 0x1d, 0x91, 0x7e, 0x8e, 0xca]

key2 = [0x00, 0xfffffffe, 0xffffffff, 0x04, 0x01, 0xffffffff, 0x01, 0x00, 0x00, 0xffffffff, 0xfffffffd, 0xfffffffe,
        0x00, 0xfffffff6, 0xffffffff, 0xffffffff, 0xfffffffe, 0x01, 0xfffffff3, 0xffffffff, 0xfffffffa, 0xffffffff,
        0xfffffffe, 0x01, 0xfffffffe]


s = Solver()
dec = [BitVec(('x%s' % i), 8) for i in range(25)]
enc2 = []
out = []
v15 = 0
for i in range(5):
    v17 = 0
    for j in range(5):
        v12 = 0
        v13 = 0
        for z in range(5):
            v3 = dec[5 * v12 + v17] * key2[5 * v15 + v12]
            v9 = -105 * (39 * (2 * (v13 & v3) + (v13 ^ v3)) + 23) + 111
            v12 += 1
            v13 = v9
        enc2.append(v9)
        v17 += 1
    v15 += 1
for i in range(25):
    s.add(enc2[i] == enc1[i])
if s.check() == sat:
    result = s.model()
    print(result)
    for i in range(25):
        out.append(result[dec[i]].as_long())
        print('0x{:02x}'.format(out[i]), end=', ')

# out = [0xe1, 0x77, 0x15, 0x9c, 0x28, 0x8c, 0x11, 0x4e, 0x9c, 0x93, 0x31, 0xf0, 0x43, 0x45, 0x1f, 0x17, 0x98, 0xb8, 0x14, 0xa3, 0x63, 0x26, 0xf4, 0x5c, 0x0c]

最后对第一部分的结果进行Z3，可以得出flag

from z3 import *
s = Solver()

input = [BitVec(('x%s' % i), 8) for i in range(25)]

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

enc = [0xe1, 0x77, 0x15, 0x9c, 0x28, 0x8c, 0x11, 0x4e, 0x9c, 0x93, 0x31, 0xf0,
       0x43, 0x45, 0x1f, 0x17, 0x98, 0xb8, 0x14, 0xa3, 0x63, 0x26, 0xf4, 0x5c, 0x0c]
out = []
for i in range(25):
    s.add((input[i] & 0xff) == enc[i])
if s.check() == sat:
    result = s.model()
    print(result)

out = [78, 75, 67, 84, 70, 123, 84, 72, 117, 116, 95, 49, 83, 115, 95, 115, 64, 95, 101, 65, 115, 121, 104, 104, 125]
for i in out:
    print(chr(i), end='')
# NKCTF{THut_1Ss_s@_eAsyhh}

总的来说不难，基本都是Z3的使用，不过要注意输出的问题，在这个程序中，结果的输出要进行一个“& 0xff”的操作（取低八位）

可以参考这个：https://blog.csdn.net/i6223671/article/details/88924481

如果这点没有注意到的话会发现其他地方输出的结果与程序输出的不同（