type
status
date
slug
summary
tags
category
icon
password
z3约束求解器是解决多元问题的好工具
其应用广泛，比如，著名的二进制分析框架angr也内置了修改版的z3
安装下载
虽然z3具有适用于各种编程语言的绑定(由C++开发，提供了 .NET、C、C++、Java、Python 等语言调用接口)，但更多以及方便的是python接口。以python接口进行详讲：
准备好Python环境和pip，就可以使用如下命令安装：
z3_微软开发的SMT求解器
什么是SMT？
- SAT-布尔可满足性问题
- SMT-可满足性模理论
若简化理解的话：SMT = SAT + Theory Solvers(理论求解器)
特点 | SAT | SMT |
逻辑范围 | 仅限于布尔逻辑 | 支持多种理论，包括整数、实数、数组、位向量等 |
公式表示 | 通常是 CNF 或其他布尔逻辑表示 | 可以是混合的逻辑公式，包含不同理论中的变量和约束 |
求解器框架 | 基于 DPLL 或 CDCL 算法 | 基于 DPLL(T) 框架，结合了 SAT 求解器和理论求解器 |
表达能力 | 只能处理简单的布尔变量关系 | 能处理复杂的约束和多样化的数据类型 |
相比较而言，SMT 能够处理更复杂的约束和数据类型，可以说是SAT的扩展
使用z3
在确保你的python环境以及安装好z3-solver后
python脚本中使用如下导入相应的包
常用的API
API | 功能 |
Solver() | 创建一个通用求解器 |
add() | 添加约束条件 |
check() | 用来判断在添加完约束条件后，来检测解的情况 |
model() | 在存在解的时候，该函数会将每个限制条件所对应的解集取交集，进而得出正解 |
变量声明
z3中有3种类型的变量，分别是整型(Int)、实型(Real)和向量(BitVec)
只有向量类型可以进行位运算（异或，左右移位等）
如何使用z3
使用一些CTF题例来进行讲解(以注释形式)
基本的思路是：
- 初始化变量
- 创建约束求解器
- 添加约束条件
- 求解
- 将每个限制条件所对应的解集取交集
[HGAME 2023 week3]kunmusic
[NSSRound#X Basic]ez_z3
[CISCN 2021初赛]babybc
用z3搓个求解器解出满足的数独
z3还能怎么用呢？
z3不只能用作多方程求解
在Reverse中，逆向有时会碰到除法运算，这一类东西在逆向的时候不能直接单纯逆为’*’
比如：
实际上我们知道c应该为1.66666…，分数会直接舍弃掉小数部分，这个时候直接逆向
a = b * c = 3 * 1 = 3，就是不对的
这种时候就需要使用到一个知识点：乘法逆元
参考文章：乘法逆元通俗易懂的理解方法-CSDN博客
可以用扩展欧几里得算法来实现计算逆元：
但实际上，可以跳过逆向这一个步骤，直接用z3正向匹配
比如说，我要计算出
直接逆向就会面临着乘法逆元的问题
用z3即可
很多有关计算的的步骤都可以用z3来巧解，可以说z3是Reverse必不可少的好伙伴
- 作者:Sh4d0w
- 链接:https://sh4d0w.life//article/0be69118-60ad-4983-8ed9-f90f9b13fc90
- 声明:本文采用 CC BY-NC-SA 4.0 许可协议，转载请注明出处。