介绍

Z3是微软研究院的一个定理验证器。它是由麻省理工学院授权的，常用来解一些方程组，在做一些CTF逆向题目的时候很有用，下面就简单介绍一下这个工具。

下载

官网：https://github.com/Z3Prover/z3

这里讲Linux下的安装，执行下面的命令即可，还有很多教程说去官网下载源码安装，没有试过感觉麻烦了些，实在安装不了就用docker

sudo pip install z3-solver

例子

(angr) angr@9fceed56f09e:~$ python
Python 3.6.7 (default, Oct 22 2018, 11:32:17)
[GCC 8.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import*
>>> x,y,z=BitVecs('x y z',8) # 申明未知量
>>> s=Solver() # 创建约束求解器
>>> s.add(x^y&z==12) # 添加约束条件
>>> s.add(y&x>>3==3)
>>> s.add(z^y==4)
>>> s.check() # 检查是否有解
sat
>>> s.model() # 显示结果
[z = 19, y = 23, x = 31]
>>>

常用的数据类型如下:

BitVec ：至特定大小的数据类型

BitVec("x",32)对应C语言中的int => 4个byte
BitVec("x",8)对应C语言中的char => 1个byte

Int：整型，Real：有理数，Bool：布尔类型，Array：数组

CTF demo

放一个demo做记录以后可能会用到

from z3 import*
input = [BitVec('input %d'%i,8)for i in range(32)] # char input[32]s = Solver()
s.add(...)
if s.check()!=sat:print 'unset'
else:m = s.model()print mprint repr("".join([chr(m[input[i]].as_long())for i in range(32)]))

whaleCTF有一道类似的题目，下面有题目和答案的链接
https://github.com/UnnameBao/My_ctf_path/tree/master/blog/I_Hate_Math

总结

更多详细的用法当然是看官网的API定义了，CTF中一般解的方程题不会太难，所以不必太深究其原理

CTF-z3简要介绍相关推荐

Hadoop学习笔记一简要介绍
Hadoop学习笔记一简要介绍这里先大致介绍一下Hadoop. 本文大部分内容都是从官网Hadoop上来的.其中有一篇介绍HDFS的pdf文档,里面对Hadoop介绍的比较全面了.我的这一 ...
数据结构的简要介绍：图形如何工作
by Michael Olorunnisola 通过Michael Olorunnisola 数据结构的简要介绍:图形如何工作 (A Gentle Introduction to Data Struc ...
R语言效用分析 ( 效能分析、Power analysis)、除了pwr包之外还有其它包、例如、基因研究中的效能分析、MBESS包可用于各种形式的效能分析和最少样本量确定、其他效用分析包的简要介绍
R语言效用分析 ( 效能分析.Power analysis).除了pwr包之外还有其它包.例如.基因研究中的效能分析(power analysis).MBESS包可用于各种形式的效能分析(power ...
简要介绍一下贝叶斯定理（ Bayes‘ theorem）
简要介绍一下贝叶斯定理( Bayes' theorem) 在引出贝叶斯定理之前,先学习几个定义: 条件概率(又称后验概率)就是事件A在另外一个事件B已经发生条件下的发生概率.条件概率表示为P(A|B) ...
各种编程语言功能综合简要介绍（C,C++,JAVA,PHP,PYTHON,易语言）
各种编程语言功能综合简要介绍(C,C++,JAVA,PHP,PYTHON,易语言) 总结 a.一个语言或者一个东西能火是和这种语言进入某一子行业的契机有关.也就是说这个语言有没有解决社会急需的问题. ...
[翻译]敏捷软件开发一之简要介绍
敏捷软件开发一之简要介绍原则.模式与实践是重要的,但是这三个要素都要由人来使得它们协同工作.正如Alistair Cockburn所说:"一个成功的项目,过程与技术永远都是排第 ...
导向滤波python_导向滤波(Guided Filter)简要介绍
1.介绍提到导向滤波,首先想到的是"何恺明",他的确是真大神,在图像领域,是中国人的骄傲,深度学习流行的时候,也是提出各种新算法,比如ResNets,而最近两年,深度学习的发展已 ...
Android系统匿名共享内存Ashmem（Anonymous Shared Memory）简要介绍和学习计划
在Android系统中,提供了独特的匿名共享内存子系统Ashmem(Anonymous Shared Memory),它以驱动程序的形式实现在内核空间中.它有两个特点,一是能够辅助内存管理系统来有效地 ...
Android进程间通信（IPC）机制Binder简要介绍和学习计划
在Android系统中,每一个应用程序都是由一些Activity和Service组成的,这些Activity和Service有可能运行在同一个进程中,也有可能运行在不同的进程中.那么,不在同一个进程的 ...
Android应用程序组件Content Provider简要介绍和学习计划
在Android系统中,Content Provider作为应用程序四大组件之一,它起到在应用程序之间共享数据的作用,同时,它还是标准的数据访问接口.前面的一系列文章已经分析过Android应用程序的 ...

CTF-z3简要介绍

介绍

下载

例子

总结

CTF-z3简要介绍相关推荐

最新文章

热门文章