2019年9月2日做题笔记（TokyoWesterns CTF

一道贼简单的逆向，被我做了一天才搞出来，我好菜。题目给了大量的限制条件，flag必须满足所有限制条件才是正确的，首先看下题目，IDA走起：

第一个check，检查flag长度为39个字节，不满足就exit：

check1

第二个check，检查flag头和尾是否为标准flag格式：

check2

第三个check，检查中间的32个字节的字母出现次数，不满足就exit，这里我们可以知道，flag中间是由32个16进制字符组成，并且有了所有字母的个数，其中3的出现次数为0：

check3

第四个check和第五个check各校验了8组的四个字母的累加和异或的结果，这四组值为

un400F40=['15e', 'da', '12f', '131', '100', '131', 'fb', '102']
un400F60=['52', 'c', '1', 'f', '5c', '5', '53', '58']
un400FA0=['129', '103', '12b', '131', '135', '10b', 'ff', 'ff']
un400F48=['1', '57', '7', 'd', 'd', '53', '51', '51']

check4 check5

第六个check，判断flag中间32个字符的取值情况，满足0-9区间的对应字符串为ff，满足a-d区间的对应字符为80

check6

第七个check，对部分字符的和进行判断，不符合就exit

check7

第八个check，如果对应位置的字符不满足，程序exit

check8

以上就是全部的程序内容，为了快速做题，接下来使用z3约束求解的方式比较容易，添加每一个约束条件，对应上面的check，详细脚本如下所示：

from z3 import *

# flag="TWCTF{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}"
# flag=list(flag)
strlist='0123456789abcdef'
num=[3,2,2,0,3,2,1,3,3,1,1,3,1,2,2,3]

dict1={}
for i in range(len(strlist)):
    dict1[strlist[i]]=num[i]
print dict1

def check1():
    b=[]
    for i in range(8):
        a=[]
        for j in range(4):
            a.append(4*i+j)
        b.append(a)
    return b

def check2():
    b=[]
    for i in range(8):
        a=[]
        for j in range(4):
            a.append(8*j+i)
        b.append(a)
    return b

def check3():
    a=[]
    for i in range(16):
        a.append(2*(i+3)-6)
    return a

if __name__=="__main__":
    un400F40=['15e', 'da', '12f', '131', '100', '131', 'fb', '102']
    un400F60=['52', 'c', '1', 'f', '5c', '5', '53', '58']
    un400FA0=['129', '103', '12b', '131', '135', '10b', 'ff', 'ff']
    un400F48=['1', '57', '7', 'd', 'd', '53', '51', '51']
                
    solver = Solver()   
    flag = [BitVec('flag%d'%i,8) for i in range(32)]

    e=['80', '80', 'ff', '80', 'ff', 'ff', 'ff', 'ff', '80', 'ff', 'ff', '80', '80', 'ff', 'ff', '80', 'ff', 'ff', '80', 'ff', '80', '80', 'ff', 'ff', 'ff', 'ff', '80', 'ff', 'ff', 'ff', '80', 'ff']

    solver.add(flag[1]==ord('f'))
    solver.add(flag[5]==ord('8'))
    solver.add(flag[6]==ord('7'))
    solver.add(flag[17]==ord('2'))  
    solver.add(flag[25]==ord('4'))
    solver.add(flag[31]==ord('5'))
    solver.add(flag[13]==ord('9'))

    for i in range(32):
        if i != 30:
            solver.add(flag[i]!=ord('a'))

    for i in range(32):
        solver.add(flag[i]!=ord('3'))

    for i in range(32):
        if i != 17 and i!= 2:
            solver.add(flag[i]!=ord('2'))

    for i in range(32):
        if i != 6 and i != 7 and i != 9:
            solver.add(flag[i]!=ord('7'))

    solver.add(flag[11]!=ord('c'))
    solver.add(flag[23]!=ord('1'))

    for i in range(len(e)):
        if e[i] == 'ff':
            solver.add(flag[i]>=ord('0'))
            solver.add(flag[i]<=ord('9'))
        else:
            solver.add(flag[i]>=ord('a'))
            solver.add(flag[i]<=ord('f'))

    for i in range(7):
        solver.add(flag[i]>47)
        solver.add(flag[i]<103) 

    a1=check1()
    a2=check2()
    a3=check3()

    for i in range(8):
        team = a1[i]
        solver.add(flag[team[0]]+flag[team[1]]+flag[team[2]]+flag[team[3]] == int(un400F40[i],16))
        solver.add(flag[team[0]]^flag[team[1]]^flag[team[2]]^flag[team[3]] == int(un400F60[i],16))

    for i in range(8):
        team = a2[i]
        solver.add(flag[team[0]]+flag[team[1]]+flag[team[2]]+flag[team[3]] == int(un400FA0[i],16))
        solver.add(flag[team[0]]^flag[team[1]]^flag[team[2]]^flag[team[3]] == int(un400F48[i],16))

    solver.add(flag[0]+flag[2]+flag[4]+flag[6]+flag[8]+flag[10]+flag[12]+flag[14]+flag[16]+flag[18]+flag[20]+flag[22]+flag[24]+flag[26]+flag[28]+flag[30] == 1160)

    #solver.add(flag[])

    solver.check()
    s=solver.model()
    cc=''
    for i in flag:
        cc+=chr(int(str(s[i])))
    print 'TWCTF{'+cc+'}'