z3求解器
周五晚上参加了vidar的分享会，感觉收获非常多（实际上一半都没听懂
但是！也可以好好总结一下上周的学习任务，比较简单（），学习z3，说实话虽然简单但是过程似乎并不是很顺利，但是还是要好好写第一篇记录学习！
第一次写加上python还不是很熟悉，可能不是很专业，而且只记下了比较常用的用法，一些细节还在推敲中，后面学得更深入会补充！如有问题和建议欢迎留言>”<
装环境
没错这个过程真的太曲折了………本来可以不写的，但是多啰嗦一句来吸取教训，就是别在虚拟机里装………………
（我指的是我自己）
Windows的安装就简单很多啦，一句命令就可以
pip install z3-solver
注意注意注意！！！不要写成z3！！这俩库完全不一样！！！具体它是什么我也不知道
简介绍
确实是很简单的介绍，传统艺能查资料（）
z3是微软开发的一个开源约束求解器。在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。
开始用
解方程
在re中经常能看到需要解方程的题目，z3就提供了非常方便的语法，真·什么方程都能解！
可以通过Int定义整型未知数，z3里的Int型跟python的Int都是没有规定位数的，可以定义一个未知数，也可以一次性定义多个未知数，利用solve函数可以直接求解
from z3 import *
# 随意发挥想象的example
x=Int('x')
y=Int('y')
a,b=Ints('a b') # 定义多个变量
solve(x>2,y<5,x+y==5)
solve(a>0,b<2,a**2+b**2==1)
# [y = 0, x = 5]
# [b = 0, a = 1]
# 无解输出no solution
除了Int，还可以定义实数（Real，位向量（BitVec，布尔（Bool等类型的未知数，语法都是一样的
逆向的时候常能看到各种作位运算的加密算法，用z3也可以解！但要注意的就是只有位向量能作位运算！！
可以看看改简单版本的Tea加密
from z3 import *
# 这里算法可能会有一点小问题，但是算法不是关键，关键是z3的语法，只是举一个简单的例子来熟悉用法！
v0=BitVec('v0',32) # 注意位向量的定义要规定位数
v1=BitVec('v1',32)
v0 += ((v1<<4) + 0) ^ (v1 + 0x12345678) ^ ((v1>>5) + 1)
v1 += ((v0<<4) + 2) ^ (v0 + 0x12345678) ^ ((v0>>5) + 3)
x=Solver()
x.add(v0==305419852,v1==4424755894)
assert x.check()==sat
print(x.model())
# [v0 = 2, v1 = 3]
顺带来解释一下更加常用的z3求解方程的方法！创建一个求解器x，通过add()创建约束条件，用check()来检查有没有解，有的话返回sat，否则返回unsat，接着可以通过print(x.model())来输出解
创建多个变量
在单字加密flag的时候就很好用了
from z3 import *
a=[Int('a%d' % i )for i in range(50)]
print(a[1])
#a1
这样就创建好了五十个整型变量啦！
（未完待续）
参考链接