title: Python-Z3-曹尼马 date: 2021-12-16 13:48:19 tags: 008-Z3
2021-Geek
1
from z3 import *
key= []
s = Solver() #创建约束求解器
s.add(S = chr((key[1] * key[2] - key[5] * 72 - key[4] * 3 - key[3] ^ key[1] + (key[3] << 2) + key[2] * 6 - key[7] & key[6] - 1000) - 14))
s.add(y = chr((key[5] * 7 + key[3] * 3 + key[2] + key[6] - (key[2] >> 2) - key[1] ^ key[0] + key[7] + (key[4] ^ key[1]) + (key[4] | key[7])) - 801))
s.add(c = chr((key[6] * 5 + key[2] * 6 - key[3] * 7 + key[4] | key[5] + key[4] * 10 + key[0] ^ key[1] * 3 - key[7] + key[0] + key[1]) - 924))
s.add(l = chr(key[1] * 3 + key[5] * 9 + key[0] + key[2] * 2 + key[3] * 5 - key[4] * (key[6] ^ key[7]) + 321 - 16))
s.add(o = chr((key[5] * 12 - key[0] ^ key[6] - key[3] * 23 + key[4] * 3 + key[2] * 8 + key[1] - key[7] * 2 + key[6] * 4 + 1324) + 1))
s.add(v = chr(key[3] * 54 - key[1] * 3 + key[2] * 3 + key[4] * 11 - key[5] * 2 + key[0] + key[7] * 3 - key[6] - 6298 + 40))
s.add(e = chr(key[7] - key[6] * key[3] + key[2] * key[2] - key[4] * 32 + key[5] * (key[0] >> 2) - key[1] * key[1] - 6689 + 41))
s.add(r = chr((key[5] - key[3] * 41 + key[6] * 41 + key[5] ^ (key[4] & key[6] | key[0]) - (key[7] * 24 | key[2]) +key[1] - 589) - 36))
key = 'Syclover'
flag = []
strflag = ''
if s.check() == sat: # 检测是否有解
result = s.model()
print (result)
else:
print('无解')
result = [113, 74, 71, 35, 29, 91, 29, 12, 114, 73, 60, 52, 69, 5, 113, 35, 95, 38, 20, 112, 95, 7, 74, 12, 102, 23, 7, 31, 87, 5, 113, 98, 85, 38, 16, 112, 29, 6, 30, 12, 65, 73, 83, 36, 12, 23]
for i in range(46):
result[i] ^ key[((i + 1) % 8)] = ord(strflag[i])
print(strflag)
2.
from z3 import*
f = Solver()
s= [BitVec('%d'%i,16) for i in range(8)]
f.add( 83== (s[1] * s[2] - s[5] * 72 - s[4] * 3 - s[3] ^ s[1] + (s[3] << 2) + s[2] * 6 - s[7] & s[6] - 1000) - 14)
f.add( 121== (s[5] * 7 + s[3] * 3 + s[2] + s[6] - (s[2] >> 2) - s[1] ^ s[0] + s[7] + (s[4] ^ s[1]) + (s[4] | s[7])) - 801)
f.add( 99== (s[6] * 5 + s[2] * 6 - s[3] * 7 + s[4] | s[5] + s[4] * 10 + s[0] ^ s[1] * 3 - s[7] + s[0] + s[1]) - 924)
f.add( 108== s[1] * 3 + s[5] * 9 + s[0] + s[2] * 2 + s[3] * 5 - s[4] * (s[6] ^ s[7]) + 321 - 16)
f.add( 111== (s[5] * 12 - s[0] ^ s[6] - s[3] * 23 + s[4] * 3 + s[2] * 8 + s[1] - s[7] * 2 + s[6] * 4 + 1324) + 1)
f.add( 118== s[3] * 54 - s[1] * 3 + s[2] * 3 + s[4] * 11 - s[5] * 2 + s[0] + s[7] * 3 - s[6] - 6298 + 40)
f.add( 101==s[7] - s[6] * s[3] + s[2] * s[2] - s[4] * 32 + s[5] * (s[0] >> 2) - s[1] * s[1] - 6689 + 41)
f.add( 114== (s[5] - s[3] * 41 + s[6] * 41 + s[5] ^ (s[4] & s[6] | s[0]) - (s[7] * 24 | s[2]) + s[1] - 589) - 36)
flag=[]
if f.check() == sat:
ans = f.model()
for i in s:
flag.append(ans[i])
print(flag)
else:
print("no ans!")
3.
#引入头文件
from z3 import*
s= [BitVec('%d'%i,8) for i in range(18)]
#引入方程组
arr=[]
x= Solver()
arr=[160,
230,
122,
286,
230,
144,
290,
208,
240,
144,
300,
216,
290,
244,
240,
100,
256,
310]
v3=0
v4=0
c=0
b=0
a=0
flag=[]
for i in range(18):
v3 =(((s[i] >> 7)&0xff) >> 4)&0xff
a = ((((v3 + (s[i] >> 4)) & 0xF) - v3))&0xff
v4 = ((((16 * s[i]) >> 31)&0xffffffff) >> 28)
b = ((((v4&0xff) +((16 * s[i]) >> 4)&0xff) & 0xF) - v4)
c = 22 * a + 12 * b
x.add(arr[i]==c&0xffff)
x.add(s[i]>=20)
x.add(s[i]<=127)
str=''
if x.check() == sat: #check()方法用来判断是否有解，sat(satisify)表示满足有解
ans = x.model()
for i in s: #因为最后得出的是等式，先遍历temp，把temp的每个依次赋给i
flag.append(ans[i])
print(flag) #model()方法得到解
else:
print("no ans!")
4.
from z3 import * #若导入了模块但没有使用则是这种灰色
arr1 = [0x7A,0xCF,0x8C,0x95,0x8E,0xA8,0x5F,0xC9,0x7A,0x91,0x88,0xA7,0x70,0xC0,0x7F,0x89,0x86,0x93,0x5F,0xCF,0x6E,0x86,
0x85,0xAD,0x88,0xD4,0xA0,0xA2,0x98,0xB3,0x79,0xC1,0x7E,0x7E,0x77,0x93]
arr2 = [0x10,0x08,0x08,0x0E,0x06,0x0B,0X5,0x17,0x05,0x0A,0x0C,0x17,0x0E,0x17,0x13,0x07,0x08,0x0A,0x04,0x0D,0x16,0x11,0x0B,
0x16,0x06,0x0E,0x02,0x0B,0x12,0x09,0x05,0x08,0x08,0x0A,0x10,0x0D]
arr3 = [8,1,7,1,1,0,4,8,1,2,3,9,3,8,6,6,4,8,3,5,7,8,8,7,0,9,0,2,3,4,2,3,2,5,4,0]
temp = [BitVec('%d' % i, 8) for i in range(36)] #初始化序列
s = Solver()
for i in range(36):
s.add(temp[i] <127)
s.add(temp[i] >=32)
#接下来还原代码
ptr = [0]*36
v7 = [0]*36 #最开始的两个变换之后的数组
one = [0]*36
two = [0]*36 #这两个用来存放对应的两个函数的结果
for i in range(36):
ptr[i] = temp[i] >> 4
v7[i] = temp[i] & 15
for i in range(6):
for j in range(6):
for k in range(6):
one[6*i+j] += ptr[6*i + k] * arr3[6*k+j]
for i in range(6):
for j in range(6):
two[6*i+j] = v7[6*i+j] + arr3[6*i+j]
#代码还原结束
for i in range(36): #添加约束条件②
s.add(one[i] == arr1[i])
s.add(two[i] == arr2[i])
flag = []
strflag = ''
if s.check() == sat: #检测是否有解
result = s.model()
for i in temp: #因为最后得出的是等式，先遍历temp，把temp的每个依次赋给i
flag.append(result[i]) #然后找到每个temp对应的解,附加到空列表的后面
print(flag) #这里先打印出来，然后后面重新赋一个序列
else:
print('无解')
from z3 import*
ss = Solver()
#s= [BitVec('s[%d]'%i,16) for i in range(33)
s = [BitVec('x%d'%i,16)for i in range(33)]
j=0
i=0
table=[0x6D, 0x53, 0x77, 0x60, 0x5A, 0x6A, 0xE6, 0x98, 0xCF, 0xE7, 0x65, 0x4B, 0x2F,
0xC9, 0xF6, 0xAD, 0xA0, 0x1F, 0xE5, 0x2A, 0xC6, 0x9E, 0xBE, 0x85, 0xDF, 0xDD, 0x10, 0x15, 0xEF,
0xE0, 0x36, 0x2B, 0xC3, 0x57, 0x23, 0x99, 0x46, 0x5F, 0x31, 0x6E, 0x9A, 0xB7, 0xE2, 0xB2, 0x03,
0x48, 0x69, 0x3A, 0xA1, 0xDE, 0xD8, 0x1D, 0x7C, 0x3C, 0xD0, 0xBD, 0xF1, 0xB3, 0xF0, 0x44, 0xA9,
0x95, 0x18, 0x33
]
cmp=[0xC3, 0x53, 0x1F, 0xBD, 0xE2, 0x60, 0xE0, 0x2A, 0x6E, 0xD8, 0xC9, 0x2F, 0xE2, 0xD8, 0x9E,
0xBE, 0x31, 0x1D, 0x95, 0x95, 0xC3, 0x1D, 0xE0, 0x5F, 0xC3, 0x6D, 0x9E, 0x85, 0x48, 0x60, 0xDE,
0x85, 0xB7, 0x60, 0x3C, 0x2B, 0x5F, 0x99, 0x57, 0xA1, 0x23, 0x57, 0x48, 0xE7
]
while(j<42):
ss.add(cmp[j]==table[(s[i]>>2)^0x34])
ss.add(cmp[j+1]==table[((s[i]&0x3)<<4 | (s[i+1]>>4))^0x34])
ss.add(cmp[j+2]==table[((s[i+1]&0xf)<<2 | (s[i+2]>>6))^0x34])
ss.add(cmp[j+3]==table[(s[i+2]&0x3f^0x34)])
i+=3
j+=4
if ss.check() == sat:
ans = ss.model()
else:
print("no ans!")
#引入头文件
from z3 import*
s= [BitVec('%d'%i,8) for i in range(18)]
#引入方程组
arr=[]
x= Solver()
arr=[160,
230,
122,
286,
230,
144,
290,
208,
240,
144,
300,
216,
290,
244,
240,
100,
256,
310]
v3=0
v4=0
c=0
b=0
a=0
flag=[]
for i in range(18):
v3 =(((s[i] >> 7)&0xff) >> 4)&0xff
a = ((((v3 + (s[i] >> 4)) & 0xF) - v3))&0xff
v4 = ((((16 * s[i]) >> 31)&0xffffffff) >> 28)
b = ((((v4&0xff) +((16 * s[i]) >> 4)&0xff) & 0xF) - v4)
c = 22 * a + 12 * b
x.add(arr[i]==c&0xffff)
x.add(s[i]>=20)
x.add(s[i]<=127)
str=''
if x.check() == sat: #check()方法用来判断是否有解，sat(satisify)表示满足有解
ans = x.model()
for i in s: #因为最后得出的是等式，先遍历temp，把temp的每个依次赋给i
flag.append(ans[i])
print(flag) #model()方法得到解
else:
print("no ans!")
from z3 import*
ss = Solver()
#s= [BitVec('s[%d]'%i,16) for i in range(33)
s = [BitVec('x%d'%i,16)for i in range(33)]
j=0
i=0
table=[0x6D, 0x53, 0x77, 0x60, 0x5A, 0x6A, 0xE6, 0x98, 0xCF, 0xE7, 0x65, 0x4B, 0x2F,
0xC9, 0xF6, 0xAD, 0xA0, 0x1F, 0xE5, 0x2A, 0xC6, 0x9E, 0xBE, 0x85, 0xDF, 0xDD, 0x10, 0x15, 0xEF,
0xE0, 0x36, 0x2B, 0xC3, 0x57, 0x23, 0x99, 0x46, 0x5F, 0x31, 0x6E, 0x9A, 0xB7, 0xE2, 0xB2, 0x03,
0x48, 0x69, 0x3A, 0xA1, 0xDE, 0xD8, 0x1D, 0x7C, 0x3C, 0xD0, 0xBD, 0xF1, 0xB3, 0xF0, 0x44, 0xA9,
0x95, 0x18, 0x33
]
cmp=[0xC3, 0x53, 0x1F, 0xBD, 0xE2, 0x60, 0xE0, 0x2A, 0x6E, 0xD8, 0xC9, 0x2F, 0xE2, 0xD8, 0x9E,
0xBE, 0x31, 0x1D, 0x95, 0x95, 0xC3, 0x1D, 0xE0, 0x5F, 0xC3, 0x6D, 0x9E, 0x85, 0x48, 0x60, 0xDE,
0x85, 0xB7, 0x60, 0x3C, 0x2B, 0x5F, 0x99, 0x57, 0xA1, 0x23, 0x57, 0x48, 0xE7
]
while(j<42):
ss.add(cmp[j]==table[(s[i]>>2)^0x34])
ss.add(cmp[j+1]==table[((s[i]&0x3)<<4 | (s[i+1]>>4))^0x34])
ss.add(cmp[j+2]==table[((s[i+1]&0xf)<<2 | (s[i+2]>>6))^0x34])
ss.add(cmp[j+3]==table[(s[i+2]&0x3f^0x34)])
i+=3
j+=4
if ss.check() == sat:
ans = ss.model()
else:
print("no ans!")
from z3 import*
s=Solver()
index = [BitVec('arr[%d]' % i, 8) for i in range(36)]
cmp = [117, 62, 240, 152, 195, 117, 103, 74, 240, 151, 173, 162, 17, 75, 141, 165, 136, 117, 113, 33, 98, 151, 174, 4, 48, 25, 254, 101, 185, 127, 131, 87]
for i in range(32):
index[i] ^= index[((i + 1) % 32)]
for j in range(1, 32):
index[j] ^= index[(j - 1)]
for k in range(32):
s.add(cmp[k]==index[k])
flag=[0]
if s.check() == sat: #检测是否有解
result = s.model()
for i in index: #因为最后得出的是等式，先遍历temp，把temp的每个依次赋给i
flag.append(result[i]) #然后找到每个temp对应的解,附加到空列表的后面
print(flag)
else:
print("bye")
''''''
