使用 z3 进行逆向解密字符串

在逆向过程中,我们知道了一个结果值，和一段计算代码。这个时候我们需要知道计算前的值是什么；需要用到 z3 模块来进行解题

z3项目地址

Java代码如下:



 private String b(String str) {

        char[] charArray = str.toCharArray();

        for (int i = 0; i < charArray.length; i++) {

            charArray[i] = (char) ((charArray[i] >> (i % 8)) ^ charArray[i]);

        }

        for (int i2 = 0; i2 < charArray.length / 2; i2++) {

            char c = charArray[i2];

            charArray[i2] = charArray[(charArray.length - i2) - 1];

            charArray[(charArray.length - i2) - 1] = c;

        }

        return new String(charArray);

    }

该函数运行结果是： 0064736c707d6f510020646b73247c4d0068202b4159516700502a214d24675100

(可以看出java代码明明是字符串类型的，因为java和python之间的问题，我给转换成了16进制，方便复制)

下面使用 z3 进行解题

from binascii import a2b_hex, b2a_hex

import z3

# a2b_hex  ascii编码的十六进制 转  二进制

# b2a_hex  二进制 转  ascii编码的十六进制

def main():

    r = '0064736c707d6f510020646b73247c4d0068202b4159516700502a214d24675100'

    # 需要先将16进制转换成二进制

    r_result = bytearray(a2b_hex(r))

    print(r_result)

    for i in range(len(r_result) // 2):

        c = r_result[i]

        r_result[i] = r_result[len(r_result) - i - 1]

        r_result[len(r_result) - i - 1] = c

    print(b2a_hex(r_result))

    # 这是一个求解器

    s = z3.Solver()

    # 创造多个求解单位

    x = [z3.BitVec(f'x{i}', 32) for i in range(len(r_result))]

    for i in range(len(r_result)):

        # c = r_result[i]

        # 根据原有算法, 这个就相当于求方程嘛。

        s.add(((x[i] >> (i % 8)) ^ x[i]) == r_result[i])

    # 求解成功

    if s.check() == z3.sat:

        model = s.model()

        # print(model)

        flag = ''

        for i in range(len(r_result)):

            # print(model[x[i]])

            # if model[x[i]]:

            try:

                flag += chr(model[x[i]].as_long().real)

            except Exception as err:

                flag += ' '

        print([flag])

    else:

        print('???')

    # [' ay I *P EASE* h ve the  assword ']

    #    ay I *P EASE* h ve the  assword

if __name__ == '__main__':

    main()

解密结果为: ay I *P EASE* h ve the assword

巴特西

使用 z3 进行逆向解密字符串

最新文章

热门文章

巴特西

使用 z3 进行逆向 解密字符串

最新文章

热门文章

使用 z3 进行逆向解密字符串