z3 solver学习
3 minute read
0x00 About
z3是个解题神器,可用于ctf中的加解密和逆向和pwn类型的题目.安装方法为:
pip3 install z3-solver
0x01 解题
0x0a 加减乘除
解法:
from z3 import *
s=[Int('serial%d' % i) for i in range(20)]
solver = Solver()
solver.add(s[15] + s[4] == 10)
solver.add(s[1] * s[18] == 2 )
solver.add(s[15] / s[9] == 1)
solver.add(s[17] - s[0] == 4)
solver.add(s[5] - s[17] == -1)
solver.add(s[15] - s[1] == 5)
solver.add(s[1] * s[10] == 18)
solver.add(s[8] + s[13] == 14)
solver.add(s[18] * s[8] == 5)
solver.add(s[4] * s[11] == 0)
solver.add(s[8] + s[9] == 12)
solver.add(s[12] - s[19] == 1)
solver.add(s[9] % s[17] == 7)
solver.add(s[14] * s[16] == 40)
solver.add(s[7] - s[4] == 1)
solver.add(s[6] + s[0] == 6)
solver.add(s[2] - s[16] == 0)
solver.add(s[4] - s[6] == 1)
solver.add(s[0] % s[5] == 4)
solver.add(s[5] * s[11] == 0)
solver.add(s[10] % s[15] == 2)
solver.add(s[11] / s[3] == 0)
solver.add(s[14] - s[13] == -4)
solver.add(s[18] + s[19] == 3)
print(solver.check())
answer=solver.model()
print(answer)
tidy_answer="".join([str(answer[each]) for each in s])
print(tidy_answer)
0x0b 未涉及BitVec类型
解法:
#!/usr/bin/env python2
from z3 import *
s = Solver()
ciphertext = "7c153a474b6a2d3f7d3f7328703e6c2d243a083e2e773c45547748667c1511333f4f745e"
cipher = ciphertext.decode("hex")
# print(cipher)
key = [Int('k%d' % i) for i in range(13)]
for each in key:
s.add(0 < each)
s.add(each < 128)
flag = [Int('flag%d' % i) for i in range(len(cipher) - 15)]
prefix = [ord(each) for each in "TWCTF{"]
for i in range(len(prefix)):
s.add(flag[i] == prefix[i])
for each in flag:
s.add(0 < each)
s.add(each < 128)
message = flag + [ord('|')] + key
encrypted = Int('R')
s.add(0 <= encrypted)
s.add(encrypted <= 128)
encrypted = [encrypted] + [Int('encrypted%d' % i)
for i in range(len(cipher) - 1)]
for i in range(1, len(message) + 1):
encrypted[i] = (message[i - 1] + key[(i - 1) %
len(key)] + encrypted[i - 1]) % 128
for i in range(len(cipher)):
s.add(ord(cipher[i]) == encrypted[i])
s.check()
answer = s.model()
flag = "".join([chr(answer[each].as_long()) for each in flag])
print(flag)
0x0c BitVec类型
当实际问题中需要进行与二进制数据有关的操作(如异或操作),则需要用到BitVec类型变量,在z3中:
1.只有BitVec变量可以进行异或
solver.add(Int('x')^Int('y')==5)不被允许
只能solver.add(BitVec('x',8)^BitVec('y',8)==5)
2.BitVecVal值之间不能进行>或<比较,只能转换成python认识的类型才可以比较
不允许:if BitVecVal(98,8)>BitVecVal(97,8)
允许:if BitVecVal(98,8)==98:
允许:if BitVecVal(98,8).as_long()>97
允许:if BitVecVal(98,8).as_long()>BitVecVal(97,8).as_long()
z3重载了==符号,但是没有重载>和<号,在int类型与bit-vector类型进行"=="比较时会将int常量当作bit-vector类型来比较
3.BitVec变量值之间可进行>或<或=或>=或<=的比较
允许:BitVec('a',8)>=BitVec('b',8)
允许:BitVec('a',8)<=BitVec('b',8)
允许:BitVec('a',8)<=9
允许:BitVec('a',8)==9
不允许:BitVec('a',8).as_long(),而允许BitVecVal(98,8).as_long()
4.z3中不允许列表与列表之间添加==约束条件
允许对列表中的每个元素分开进行==的条件限定约束:
from z3 import *
prefix=[ord(each) for each in "flag{"]
plain_line=[Int('x%d' % i) for i in range(5)]
s=Solver()
z=0
#s.add(plain_line[z:z+5]==prefix)
s.add(plain_line[z]==prefix[0])
s.add(plain_line[z+1]==prefix[1])
s.add(plain_line[z+2]==prefix[2])
s.add(plain_line[z+3]==prefix[3])
s.add(plain_line[z+4]==prefix[4])
s.check()
print(s.model())
不允许直接对列表进行==的条件限定约束,下面的用法是不允许的,会无解:
from z3 import *
prefix=[ord(each) for each in "flag{"]
plain_line=[Int('x%d' % i) for i in range(5)]
s=Solver()
z=0
s.add(plain_line[z:z+5]==prefix)
#s.add(plain_line[z]==prefix[0])
#s.add(plain_line[z+1]==prefix[1])
#s.add(plain_line[z+2]==prefix[2])
#s.add(plain_line[z+3]==prefix[3])
#s.add(plain_line[z+4]==prefix[4])
s.check()
print(s.model())
解法:
from z3 import *
import base64
def encrypt(plaintext, key):
plaintext += '|'
plaintext += key
key = key*(len(plaintext)//len(key))
key += key[:len(plaintext)-len(key)]
cipher = ''.join(chr(ord(i)^ord(j)) for i,j in zip(plaintext, key))
cipher = base64.b64encode(cipher.encode('ascii'))
return cipher.decode('ascii')
#z=11,y=17
ceshi_encrypted=encrypt("lalalanihaoflag{8989082399}","11122233344455566")
timu_encrypted="BCU8EGwlJzAdBjAcGCgaFxgsNyEKIy9iOBxDLwFePVtEIj1kOxBsJisnCg1jHFd4HQ0GaSYnF2wuLDIKT2MJVjxVDA5pKScQOGEuOBkGYwFMeAYLSyg3chcjYSQ0Cg9jBld4AQsZPTEgCiImYiMKBDENTCtVAgQ7ZCUCPzUnNU8aJglKK1lEBSwyNxFsKiw+GEM3AF14FxEZJy08BGwyKjACBmMHXngURAYsJTxDLS8mcR8GNxxBeAUFGD1/chAjYS44GQZjHFA5AUhLLT07DSttYjkKQy4BXzABRBgoPWhDLS0ucQIaYwRRPhBISygoPkMhOGIiGxEmBl8sHUQcLDY3QysoNDQBQzcHGCwdAUsvLTwGPzViMg4WMA0YMRtECiUochckJGImABEvDBR4AQwOaSI7BCQ1YjcAEWMcUD1VKAIrISACOCgtP08MJUh1ORsPAicgfEMEJDA0TwowSEwwEEQbOy0oBmwnLSNPFysBS3gZAR0sKGhDKi0jNhQ3Kw1nNRQDAiobJQw+JR04HDw7B0olCS0vGyceIg4QLTIsC3swTTwe"
#encrypted=ceshi_encrypted
encrypted=timu_encrypted
cipher=base64.b64decode(encrypted.encode("ascii")).decode('ascii')
length=len(cipher)
cipher=[BitVecVal(ord(each),8) for each in cipher]
plain_line=[BitVec('p%d' % i,8) for i in range(length)]
key_line=[BitVec('k%d' % i,8) for i in range(length)]
prefix=[BitVecVal(ord(each),8) for each in "flag{"]
for y in range(1,length-7+1):
for z in range(0,length-y-7+1):
s=Solver()
#s.add(plain_line[z:z+5]==prefix)
s.add(plain_line[z]==prefix[0])
s.add(plain_line[z+1]==prefix[1])
s.add(plain_line[z+2]==prefix[2])
s.add(plain_line[z+3]==prefix[3])
s.add(plain_line[z+4]==prefix[4])
for i in range(length):
32<=plain_line[i]
plain_line[i]<=126
32<=key_line[i]
key_line[i]<=126
plain_line[-y-1]==ord('|')
key=plain_line[-y:]
for i in range(length):
s.add(key_line[i]==key[i%y])
s.add(plain_line[i]^key_line[i]==cipher[i])
if s.check()==sat:
answer=s.model()
print(answer)
key_line="".join([chr(answer[each].as_long()) for each in key_line])
plain_line="".join([chr(answer[each].as_long()) for each in plain_line])
print("key_line:")
print(key_line)
print("plain_line:")
print(plain_line)
input("Congratulations!")
else:
print("try key len:%d,'flag{' index:%d" % (y,z))
continue
