z3
简介
Z3 solver 是由微软开发的 可满足性模理论求解器（Satisfiability Modulo Theory solver， 即 SMT solver），用于检查逻辑表达式的可满足性，并可以找到一组约束中的其中一个可行解（无法找出所有的可行解）。
在 CTF 逆向题中，我们有的时候会遇到一些较为复杂的约束条件，此时可以使用 z3 来辅助求解。
安装
Z3 提供了多种语言的接口，方便起见我们使用 Python 版本，我们可以直接通过 pip 进行安装（注意这里应当为 z3-solver 而非 z3）：
基本用法
本节仅介绍 z3 最基本的用法，更多高级用法参见官方文档
变量表示
一阶命题逻辑公式由项（变量或常量）与扩展布尔结构组成，在 z3 当中我们可以通过如下方式创建变量实例：
整型（integer，长度不限）
实数类型（real number，长度不限）
位向量（bit vector，长度需在创建时指定）
布尔类型（bool）
整型与实数类型变量之间可以互相进行转换：
常量表示
除了 Python 原有的常量数据类型外，我们也可以使用 z3 自带的常量类型参与运算：
求解器
在使用 z3 进行约束求解之前我们首先需要获得一个 求解器 类实例，本质上其实就是一组约束的集合：
添加约束
我们可以通过求解器的 add() 方法为指定求解器添加约束条件，约束条件可以直接通过 z3 变量组成的式子进行表示：
对于布尔类型的式子而言，我们可以使用 z3 内置的 And()、Or()、Not()、Implies() 等方法进行布尔逻辑运算：
约束求解
当我们向求解器中添加约束条件之后，我们可以使用 check() 方法检查约束是否是可满足的（satisfiable，即 z3 是否能够帮我们找到一组解）：
z3.sat：约束可以被满足z3.unsat：约束无法被满足
若约束可以被满足，则我们可以通过 model() 方法获取到一组解：
对于约束条件比较少的情况，我们也可以无需创建求解器，直接通过 solve() 方法进行求解：
例题：GWCTF 2019 - xxor
逆向分析
首先惯例拖入 IDA 中，main() 函数整体逻辑比较简单，首先会读入 6 个整型到栈上，接下来对前三个整型调用三次 sub_400686() 函数进行处理并将结果存到 v7 中，最后调用 sub_400770() 进行检查：
sub_400686() 有点类似于魔改的 TEA 加密：
这里的参数 a1 为我们的输入，而 a2 则为四个 int32：
而 sub_400770() 会对处理过后的输入进行检查：
求解
我们首先使用 z3 来求解 sub_400686() 运算后的结果：
结果如下：
接下来我们逆着 sub_400686() 的逻辑写出解密程序即可：
结果如下：
接下来就是快乐的拿 flag 时间了：
Last updated