今天在vidar的分享会上
s神跟我们讲了一个python的库叫做z3
可以在python中用这个库解决任何方程（只要有解）
网上找不到任何中文资料=。=看来我只能自己写了
z3库的介绍
Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。
z3的安装过程
我差点就放弃这个库了，就是因为一直安装不上。。
后来询问了s神，s神跟我说要用源码安装
给个地址https://pypi.org/project/z3-solver/4.5.1.0/#files（whl文件下载地址）
只能python2，所以我装在虚拟机上了
千万千万不要使用pip install z3，不知道为什么就是不一样。。
安装好了！
z3如何使用！
惊了这个库可以解决所有的方程，如果有解
首先要给所有的设置一个变量，他有很多种变量
Int型他代表整数所有的解都只能是整数，当然也可以用Ints一次性设置多个变量
还有就是Real型的这个代表的是有理数，可以解出所有的有理数
以及BitVec（常用的）
可以设置几位主要是re选手用的吧，这里可以解决位与方程用这个！超级强，后面一个变量设置这个变量有几位，方便位与运算
-
Int型解方程
首先是给变量赋值
设置一个解方程的类Solver
然后一个一个添加（这样比较直观）
check一下看看有没有解，最后得出一个解，当然还有另外一种方法
-
Real型解方程
直接用solve函数就可以了
-
BitVec型解方程
这些都不算什么，平常都可以解出来
现在有平常解不出来的东西！！！就是向量（位与运算）
！！！！惊了这都能解出来以后我再也不用担心计组了
网友评论