[python/工具] python z3库学习 python的加减乘除位与运算 ctf一把梭

今天在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型解方程

这些都不算什么,平常都可以解出来
现在有平常解不出来的东西!!!就是向量(位与运算)

 

!!!!惊了这都能解出来以后我再也不用担心计组了

z3的学习连接

发表评论

电子邮件地址不会被公开。 必填项已用*标注