【RE】z3#
z3#
z3是python中的一个模块，它的主要作用是约束求解，也就是给定一些条件，就可以求出一组符合条件的解，同通过z3可以不用计算，就像解方程一样，但是要注意的是，z3只能求出符合条件的一组解，如果题目存在多解的情况，z3也只能求出一组解，现在可以来看一个题目，flag长度为33，并且要求了长度为33
程序主要的加密就是用我们输入值进行加减运算，得到a2
直接用z3来求解
from z3 import *
P=[12864,5522,10710,6924,788,10715,10008,13022,15893,9754,7946,7490,5636,13477,
2198,5861,5799,5259,6464,6171,2269,9251,8315,2989,-199,2680]
a = [z3.BitVec("p%d" % i, 8)for i in range(33)]
f="flag{"
s=Solver()
s.add(a[0]==ord(f[0]))
s.add(a[1]==ord(f[1]))
s.add(a[2]==ord(f[2]))
s.add(a[3]==ord(f[3]))
s.add(a[4]==ord(f[4]))
s.add(P[0]==12*a[5]+44*a[7]+17*a[6]+100*a[8]+20*a[9]+75*a[10])
s.add(P[1]==63*a[10]+58*a[9]+46*a[5]+25*a[8]-89*a[7]+12*a[6]+2)
s.add(P[2]==23*a[8]+45*a[9]+26*a[5]+77*a[6]+11*a[10]+41*a[7]+6)
s.add(P[3]==34*a[7]+12*a[8]+15*a[10]+19*a[9]+20*a[6]+44*a[5]+12)
s.add(P[4]==4*a[9]+2*a[10]+5*a[7]-4*a[8]+8*a[6]+a[5]+20)
s.add(P[5]==12*a[6]+10*a[7]+9*a[9]+8*a[8]+99*a[10]+85*a[5]+11)
s.add(P[6]==11*a[11]+12*a[12]+33*a[13]+55*a[14]+77*a[15]+20*a[16]+24)
s.add(P[7]==66*a[11]+45*a[13]+78*a[15]+21*a[14]+56*a[12]+3*a[16]+110)
s.add(P[8]==65*a[12]+25*a[15]+78*a[16]+54*a[14]+96*a[11]+a[13]*13+5)
s.add(P[9]==88*a[13]+20*a[14]+a[15]*7+a[16]*36+a[11]*11+a[12]*41+10)
s.add(P[10]==a[14]*14+a[15]*55+a[16]*62+a[11]*17+a[12]*8+a[13]+410)
s.add(P[11]==a[15]*52+a[16]+a[11]+a[12]*2+a[14]*5+a[13]*6+a[14]*88+50)
s.add(P[12]==a[17]+a[18]+8*a[19]+9*a[20]+11*a[21]+85*a[22]+11)
s.add(P[13]==a[18]*56+a[19]*65+a[20]*78+a[21]*22+a[22]*55+a[17]+26)
s.add(P[14]==a[19]*19+a[20]*3-a[21]-a[22]+a[17]*6+a[18]*20-11)
s.add(P[15]==a[20]*8+a[21]*77+a[22]*46+a[17]*4-a[18]*10-a[19]*5-30)
s.add(P[16]==a[21]*21+a[22]*22+a[17]*17+a[18]*18+a[19]*19+a[20]*20+120)
s.add(P[17]==a[22]*9+a[21]*85+a[20]*5+a[19]*9+a[18]*8+a[17]*4-600)
s.add(P[18]==a[23]*5+a[24]*6+a[25]*7+a[26]*8+a[27]*88+a[28]*22-200)
s.add(P[19]==a[24]*50+a[25]*80+a[26]*10+a[27]*7+a[28]*12-a[23]*20-640)
s.add(P[20]==a[25]*14+a[26]*8+a[27]*4+a[28]*25+a[23]*3+a[24]*7-720)
s.add(P[21]==a[26]*8+a[27]*80+a[28]*40+a[23]*6+a[24]*5+a[25]*60-500)
s.add(P[22]==a[27]*10+a[28]*85+a[23]*40+a[24]*41+a[25]*25-a[26]*26-260)
s.add(P[23]==a[28]*9+a[23]*9+a[24]*55-a[25]*10-a[26]-a[27])
s.add(P[24]==a[29]+a[30]+a[20]-a[19]-a[18]*2+a[16]-250)
s.add(P[25]==a[30]-a[29]+3*a[16]+4*a[5]+55*a[27]+a[25]-400)
print(s.check())
answer=s.model()
print(answer)
得到程序的解为
flag{000000000000000111111111111}
直接输入，得到flag
flag{L1sten_t0_the_s1lence_Of_extinct10n!}
z3的主要优势是直接正向模仿运算的过程，对于一些不好进行逆运算的加密算法来说是比较好的工具
大纲