一道贼简单的逆向,被我做了一天才搞出来,我好菜。题目给了大量的限制条件,flag必须满足所有限制条件才是正确的,首先看下题目,IDA走起:
第一个check,检查flag长度为39个字节,不满足就exit:
check1第二个check,检查flag头和尾是否为标准flag格式:
check2第三个check,检查中间的32个字节的字母出现次数,不满足就exit,这里我们可以知道,flag中间是由32个16进制字符组成,并且有了所有字母的个数,其中3的出现次数为0:
check3第四个check和第五个check各校验了8组的四个字母的累加和异或的结果,这四组值为
check4 check5un400F40=['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']
第六个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+'}'
网友评论