Z3 求解
s=solver()，创建一个解的对象。
s.add(条件)，为解增加一个限制条件
s.check()，检查解是否存在，如果存在，会返回"sat"
modul()，输出解得结果
solver.assertions()查看求解器已经添加的约束和约束的个数：
添加未知数
>>> x = [z3.Int(f'x{i}') for i in range(10)]
>>> 也就是 x1 x2 x3 这个样子
添加约束 ¶
我们可以通过求解器的 add() 方法为指定求解器添加约束条件，约束条件可以直接通过 z3 变量组成的式子进行表示：
>>> s.add(x * 5 == 10)
>>> s.add(y * 1/2 == x)
对于布尔类型的式子而言，我们可以使用 z3 内置的 And()、Or()、Not()、Implies() 等方法进行布尔逻辑运算：
>>> s.add(z3.Implies(p, q))
>>> s.add(r == z3.Not(q))
>>> s.add(z3.Or(z3.Not(p), r)
其分为整型(Int)，实型(Real)和向量(BitVec)
Int(name, ctx=None)，创建一个整数变量，name是名字
Ints (names, ctx=None)，创建多个整数变量，names是空格分隔名字
IntVal (val, ctx=None)，创建一个整数常量，有初始值，没名字。
实形(real)
real(name, ctx=None)，创建一个实变量，name是名字
reals (names, ctx=None)，创建多个实变量，names是空格分隔名字
realVal (val, ctx=None)，创建一个实常量，有初始值，没名字。
向量(BitVec)
Bitvec(name,bv,ctx=None)，创建一个位向量，name是他的名字，bv表示大小
BitVecs(name,bv,ctx=None)，创建一个有多变量的位向量，name是名字，bv表示大小
BitVecVal(val,bv,ctx=None)，创建一个位向量，有初始值，没名字。
实例
xorr[0] = MainGame.money
xorr[1] = MainGame.shaoguan
xorr[2] = MainGame.score
xorr[3] = MainGame.remnant_score
if xorr[0] * 256 - xorr[1] / 2 + xorr[2] * 23 + xorr[3] / 2 == 47118166:
if xorr[0] * 252 - xorr[1] * 366 + xorr[2] * 23 + xorr[3] / 2 - 1987 == 46309775:
if xorr[0] * 6 - xorr[1] * 88 + xorr[2] / 2 + xorr[3] / 2 - 11444 == 1069997:
if (xorr[0] - 652) * 2 - xorr[1] * 366 + xorr[2] * 233 + xorr[3] / 2 - 13333 == 13509025:
for i in range(len(flag)):
ans[i] = flag[i] ^ xorr[i % 4]
else:
with open("flag.txt", "w") as f:
f.write("".join([chr(a) for a in ans]))
exp
from z3 import *
flag = [178868, 188, 56953, 2413, 178874, 131, 56957, 2313, 178867, 156,
56933, 2377, 178832, 202, 56899, 2314, 178830, 167, 56924,
2313, 178830, 167, 56938, 2383, 178822, 217, 56859, 2372]
a = [178940,248,56890,2361]
a0 = BitVec('a0',64)
a1 = BitVec('a1',64)
a2 = BitVec('a2',64)
a3 = BitVec('a3',64)
s = Solver()
s.add(a0 * 256 - a1 / 2 + a2 * 23 + a3 / 2 == 47118166)
s.add(a0 * 252 - a1 * 366 + a2 * 23 + a3 / 2 - 1987 == 46309775)
s.add(a0 * 6 - a1 * 88 + a2 / 2 + a3 / 2 - 11444 == 1069997)
s.add((a0 - 652) * 2 - a1 * 366 + a2 * 233 + a3 / 2 - 13333 == 13509025)
print(s.check())
print(s.model())
for i in range(len(flag)):
print(chr(flag[i] ^ a[i % 4]),end='')
这里很多人可能会遇到一个点就是，在进行z3解密时，很多人解出来的不是2361，而是2360,
这是因为z3在Int类型中，会对数据进行一些截断的位操作，这就导致最后的结果有差异，
所以这里的话，最好还是使用z3中可以使用位运算的类型，即BitVec
实例2
# Source Generated with Decompyle++
# File: baby_core.pyc (Python 3.7)
import hashlib
def md5(s = None): #ma5 加密
m = hashlib.md5()
m.update(s)
return m.hexdigest().lower()
def main(): # 读取输入也就是我们后面所需要的 x1 x2 这个未知数 也就是值
secret = input('secret: ')
if len(secret) != 48:
return None
if not None.isnumeric():
return None
values = None
for i in range(0, 48, 3):
values.append(int(secret[i:i + 3]))
co=[
[158,195,205,229,213,238,211,198,190,226,135,119,145,205,113,122],
[234,256,185,253,244,134,102,117,190,106,131,205,198,234,162,218],
[164,164,209,200,168,226,189,151,253,241,232,151,193,119,226,193],
[213,117,151,103,249,148,103,213,218,222,104,228,100,206,218,177],
[217,202,126,214,195,125,144,105,152,118,167,137,171,173,206,240],
[160,134,131,135,186,213,146,129,125,139,174,205,177,240,194,181],
[183,213,127,136,136,209,199,191,150,218,160,111,191,226,154,191],
[247,188,210,219,179,204,155,220,215,127,225,214,195,162,214,239],
[108,112,104,133,178,138,110,176,232,124,193,239,131,138,161,218],
[140,213,142,181,179,173,203,208,184,129,129,119,122,152,186,124],
[105,205,124,142,175,184,234,119,195,218,141,122,202,202,190,178],
[183,178,256,124,241,132,163,209,204,104,175,211,196,136,158,210],
[224,144,189,106,177,251,206,163,167,144,208,254,117,253,100,106],
[251,251,136,170,145,177,175,124,193,188,193,198,208,171,151,230],
[143,200,143,150,243,148,136,213,161,224,170,208,185,117,189,242],
[234,188,226,194,248,168,250,244,166,106,113,218,209,220,158,228]
]
r=[472214,480121,506256,449505,433390,435414,453899,536361,423332,427624,440268,488759,469049,484574,480266,522818]
for i in range(16):
v = 0
for j in range(16):
v += co[i][j] * values[j] #创造一个总和 来存储值 我们想要得出来的就是values 所以我们要存储 一个方程式 158*x0 195*x1 205*x2 229*x3 213*x4 238*x5 这样的方程 添加到求解器实例中也就是add 这样
#我们并不能求解出来他所需要的值 所以我们要添加一个下面有一个判断 v != r[i] 所以我们要求解的话 就是要 v == r[i] 也就是 158*x0+195*x1+205*x2+229*x3+213*x4+...== r[i]
#这样就能判断是否能求解出合适的x0-x15的值 sat 就是有解
if v != r[i]:
return None
print('flag{ISEC-%s}' % md5(secret.encode()))
exp
from z3 import *
import hashlib
s = Solver()
x = [Int(f'x{i}') for i in range(16)]
co=[
[158,195,205,229,213,238,211,198,190,226,135,119,145,205,113,122],
[234,256,185,253,244,134,102,117,190,106,131,205,198,234,162,218],
[164,164,209,200,168,226,189,151,253,241,232,151,193,119,226,193],
[213,117,151,103,249,148,103,213,218,222,104,228,100,206,218,177],
[217,202,126,214,195,125,144,105,152,118,167,137,171,173,206,240],
[160,134,131,135,186,213,146,129,125,139,174,205,177,240,194,181],
[183,213,127,136,136,209,199,191,150,218,160,111,191,226,154,191],
[247,188,210,219,179,204,155,220,215,127,225,214,195,162,214,239],
[108,112,104,133,178,138,110,176,232,124,193,239,131,138,161,218],
[140,213,142,181,179,173,203,208,184,129,129,119,122,152,186,124],
[105,205,124,142,175,184,234,119,195,218,141,122,202,202,190,178],
[183,178,256,124,241,132,163,209,204,104,175,211,196,136,158,210],
[224,144,189,106,177,251,206,163,167,144,208,254,117,253,100,106],
[251,251,136,170,145,177,175,124,193,188,193,198,208,171,151,230],
[143,200,143,150,243,148,136,213,161,224,170,208,185,117,189,242],
[234,188,226,194,248,168,250,244,166,106,113,218,209,220,158,228]
]
r=[472214,480121,506256,449505,433390,435414,453899,536361,423332,427624,440268,488759,469049,484574,480266,522818]
for i in range(16):
v = 0
for j in range(16):
v += co[i][j] * x[j]
s.add(v == r[i])
if s.check() == sat:
m = s.model()
secret = ''.join([str(m[x[i]]) for i in range(16)])
print('flag{ISEC-%s}' % md5(secret.encode()))
'''
创造一个总和 来存储值 我们想要得出来的就是values 所以我们要存储 一个方程式 158*x0 195*x1 205*x2 229*x3 213*x4 238*x5 这样的方程 添加到求解器实例中也就是add 这样
我们并不能求解出来他所需要的值 所以我们要添加一个下面有一个判断 v != r[i] 所以我们要求解的话 就是要 v == r[i] 也就是 158*x0+195*x1+205*x2+229*x3+213*x4+...== r[i]
这样就能判断是否能求解出合适的x0-x15的值 sat 就是有解
'''
评论