WhiteHat CTF 2015 Crypto400

这是一道re

这题原本是angr官方文档的题目，用来让熟悉angr使用方式，但是由于种种原因，angr脚本并不能跑起来，遂转用传统做法，

也在此中完善了对z3的认识。

思路

题目很简单

可以先使用finger恢复符号表。恢复完后程序的逻辑就会更为明显，首先是通过命令行传参，丢给sub_40166A进行初步的判断，然后再将参数当作密钥对BlowFish的P盒以及S盒变换，然后在解密qword_6C10E01,再比对结果。

所以这题的关键就在与传的参数，参数对了，这个解密才能正确

先来看看第一步判断sub_40166A

很简单明了的约束条件,首先密钥长度为8，然后每一位密钥之间应该满足如下关系

byte_6C4B20 * byte_6C4B21 == 13310
byte_6C4B22 + byte_6C4B23 == 185
byte_6C4B24 != (byte_6C4B25 == 53)
byte_6C4B26 - byte_6C4B27 == -19
byte_6C4B20 + byte_6C4B27 == 195
byte_6C4B24 != (byte_6C4B21 == 24)
byte_6C4B22 | (byte_6C4B27 == 117)
byte_6C4B20 * byte_6C4B25 == 9240

但细心一点会发现，这里虽然有8行表达式，但其中有两行是无效的，即byte_6C4B24 != (byte_6C4B25 == 53)和byte_6C4B22 | (byte_6C4B27 == 117)，这两行并不能起到约束效果。也就是说有八个未知数，但只有六个约束条件，这就决定了能通过第一步的参数不止一个。

于是乎很自然的想到可以使用z3求解器帮助我们过掉第一步的筛选，再进一步判断。

当我们过掉一步的判断后，紧接这就是BlowInit和Blowdec，这两个函数就是BlowFish的标准初始化函数和解密函数，那么我们就可以使用z3求解出来的值来进一步爆破。

note：需要把z3求解出来的值，转化为python的int型，才能去索引列表，脚本中会有详细注释

note2：脚本中Blow_BOX 存放提取出来的S盒 P盒，此题目的S盒、P盒与传统的值不相同

脚本

from z3 import *
import copy
from Blow_BOX import *

# 存储P盒以及S盒，因为每次爆破一次key P盒和S盒都会变化，下一次爆破需要复原
# 这个地方需要使用此复制 即创建两个独立的P盒 S盒 不可简单用等于号 否则会一起变化
P_temp = copy.deepcopy(p_box)
S_temp = copy.deepcopy(s_box)


def init_key_pbox(_key):
    index = 0
    key_pbox = [0 for i in range(18)]
    for i in range(18):
        for j in range(4):
            key_pbox[i] = ord((_key[index])) | (key_pbox[i] << 8)
            index += 1
            if index >= len(_key):
                index = 0

    for i in range(18):
        p_box[i] ^= key_pbox[i]


def Fn(Left):
    a = (Left & 0xff000000) >> 24
    b = (Left & 0x00ff0000) >> 16
    c = (Left & 0x0000ff00) >> 8
    d = Left & 0x000000ff

    Sa = s_box[0][a]
    Sb = s_box[1][b]
    Sc = s_box[2][c]
    Sd = s_box[3][d]

    return (((Sa + Sb) ^ Sc) + Sd) & 0xffffffff


def Blow_Main_Encrypt(Left, Right):
    # print(p_box)
    for i in range(16):
        Left ^= p_box[i]
        Right ^= Fn(Left)
        Temp = Left
        Left = Right
        Right = Temp

    Temp = Left
    Left = Right ^ p_box[17]
    Right = Temp ^ p_box[16]
    return Left, Right


def Blow_Main_Decrypt(Left, Right):
    for i in range(17, 1, -1):
        Left ^= p_box[i]
        Right ^= Fn(Left)

        Temp = Left
        Left = Right
        Right = Temp

    Temp = Left
    Left = Right ^ p_box[0]
    Right = Temp ^ p_box[1]
    return Left, Right


def Change_Box():
    Left = 0
    Right = 0
    for i in range(0, 18, 2):
        Left, Right = Blow_Main_Encrypt(Left, Right)
        p_box[i] = Left
        p_box[i + 1] = Right

    for i in range(4):
        for j in range(0, 256, 2):
            Left, Right = Blow_Main_Encrypt(Left, Right)
            s_box[i][j] = Left
            s_box[i][j + 1] = Right


def BlowFish_Encrypt(data):
    while len(data) % 8:
        data += '0'
    cipher = ''
    for i in range(0, len(data), 8):
        Left = (ord(data[i]) << 24) | (ord(data[i + 1]) << 16) | (ord(data[i + 2]) << 8) | (ord(data[i + 3]))
        Right = (ord(data[i + 4]) << 24) | (ord(data[i + 5]) << 16) | (ord(data[i + 6]) << 8) | (ord(data[i + 7]))
        Left, Right = Blow_Main_Encrypt(Left, Right)
        cipher += hex(Left)[2:]
        cipher += hex(Right)[2:]

    print(cipher)


def BlowFish_Decrypt(cipher):
    plain = ''
    for i in range(0, len(cipher), 16):
        Left = cipher[i:i + 8]
        Right = cipher[i + 8:i + 16]
        # print(Left)
        Left = int(Left, base=16)
        Right = int(Right, base=16)
        
        Left, Right = Blow_Main_Decrypt(Left, Right)
        plain += hex(Left)[2:]
        plain += hex(Right)[2:]

    plain = int(plain, base=16)

    print("[*] Now ans: ", hex(plain)[2:])
    return plain

# 创建8个8bits的位向量
# 存放在flagp[]列表中，每一个位向量符号是flag[i]
flag = [BitVec("flag[%d]" % i, 8) for i in range(8)]
S = Solver()

# 添加约束条件
S.add(flag[0] * flag[1] == 13310)
S.add(flag[2] + flag[3] == 185)
S.add(flag[6] - flag[7] == -19)
S.add(flag[0] + flag[7] == 195)
S.add(flag[0] * flag[5] == 9240)

# 进一步添加约束条件，略去非常见flag字符，比如'|'  ','  '<'等
for i in range(8):
    S.add(flag[i] >= 33)
    S.add(flag[i] <= 125)
    S.add(flag[i] != 39)
    S.add(flag[i] != 58)
    S.add(flag[i] != 59)
    S.add(flag[i] != 60)
    S.add(flag[i] != 61)
    S.add(flag[i] != 62)
    S.add(flag[i] != 96)
    S.add(flag[i] != 124)
    S.add(flag[i] != 91)
    S.add(flag[i] != 92)
    S.add(flag[i] != 93)
    S.add(flag[i] != 94)
# C即待解数据 即qword_6C10E01
C = '69142BA8383E7938'
# ans即待比对数据
ans = 0x6f8cb46b5138c655

while 1:
    S.check()
    T = S.model() # 得到一组解
    Try = ''
    condition = [] # 用于把这一组解添加进约束变量，用于排除此组解
    for i in range(8):
        a = T.eval(flag[i]).as_long() # 把flag[i]从z3的类型转为python的Int类型
        condition.append(flag[i] != a)# 添加约束条件，把这一整组解都作为约束条件

        Try += chr(a) # 当前解
    S.add(Or(condition))# 把当前这组解添加进去，这样以后的解就不会再有此组解了
    # note: 注意不可以简单使用S.add(flag[i]!=xxx)，因为这样排除其他解，即在flag[i]==xx的前提下，也有很多解
    print("[*] Trying:", Try, end=' ')
	# 使用刚刚得到的值去尝试解密
    init_key_pbox(Try)
    Change_Box()
    an = BlowFish_Decrypt(C)

    if an == ans:
        print("[+] answer:", Try)
        break
    # 恢复P盒 S盒 
    p_box = copy.deepcopy(P_temp)
    s_box = copy.deepcopy(S_temp)

关于S盒的提取可以说道说道，由于BlowFish的S盒是4*256的二维数组，就是有1024个值，那么在IDA就体现为这个形式

以往我都是一行行复制，但无疑这样的效率是极低的，而且也很繁琐。因为我的BlowFish脚本中S盒是以4*256二维数组形式存储的，难不成我还要每次数256个来复制，然后复制4次？

显然是不科学的，所以可以借助于IDApython来帮我们提取这个S盒

ea = 0x6c00e0
S_Box=[[],[],[],[]]
for i in range(1024):
    S_Box[i//256].append((idc.get_wide_dword(ea)))
    ea += 4
print(S_Box)

看，简简单单几行代码就可以帮我们把这个4*256的数组按照我们所想的方式存放，多轻松（这就是技多不压身吧hhh

总结

这题思路很简单，就是爆破。但这题最大的收获在于学习了BlowFish加密算法，而且最重要的是学会了如何遍历z3的所有解，如何把z3类型转为python类型，以便进一步爆破求解。因为z3类型是不可以作为数组索引的，只有python的Int型才可以。

angr解此题也是一样的，也是符号执行把密钥空间缩小，然后再一个一个爆破密钥，与上面的思路完全一样