美文网首页
2019年9月2日做题笔记(TokyoWesterns CTF

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

作者: Ginkgo_Alkaid | 来源:发表于2019-09-23 11:23 被阅读0次

    一道贼简单的逆向,被我做了一天才搞出来,我好菜。题目给了大量的限制条件,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+'}'
    

    相关文章

      网友评论

          本文标题:2019年9月2日做题笔记(TokyoWesterns CTF

          本文链接:https://www.haomeiwen.com/subject/tpwqyctx.html