z3约束求解器

一、z3约束求解器理解

  1. z3介绍

    Z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，可以用来软件/硬件验证和测试，约束求解，混合系统分析，安全性研究，生物学研究（计算机分析）以及几何问题。通俗的来讲我们可以简单理解为它是一个解方程的计算器，Z3py是使用脚本来解决一些实际问题。

  2. z3在CTF逆向中有什么用？

    我们在做CTF逆向题的时候，当我们已经逆向到最后求flag或者具体数值解的时候，例如最简单的：我们知道了未知量x,y，也知道了约束条件x+y=5，那么此时我们就可以使用Z3来求解x和y的值，因为x和y的值肯定有多个解，而我们最后的flag肯定只有一个，那么我们就可以继续添加约束条件来减少解的数量，最后得出正确的flag。

二、z3语法简介：

z3在python中的未知数变量主要有以下数据类型：

  1. Int –> 整型（注意逐个列出时使用Int()，一次全部列出使用Ints()）。

    1
    2
    3
    4
    5
    a,b,c,d=Ints('a b c d')
    # a = Int('a')
    # b = Int('b')
    # c = Int('c')
    # d = Int('d')

    • 如果参数多建议使用循环：v = [Int(f'v{i}') for i in range(0, 16)]

      • f'v{i}' 是一种格式化字符串字面量（也称为 f-string），它允许你在字符串中嵌入表达式。具体来说：

      • f 前缀：表示这是一个 f-string,将字符串格式化的方法。

      • 大括号 {}：用于包裹需要动态计算的表达式。

      • f'v{i}' 会根据循环变量 i 的值动态生成字符串。

      • 例如，当 i=0 时，f'v{i}' 会变成字符串 'v0'；当 i=1 时，会变成 'v1'，依此类推，直到 i=15 时生成 'v15'。

      • **Int()**是z3中用于将变量转换为特定类型的一个函数

  2. Bool –> 布尔型

  3. Array –> 数组

  4. BitVec(‘a’,8) –> char型（其中的数字不一定是8，例如C语言中的int型可以用BitVec(‘a’,32)表示）

三、几个常用的API

**Solver()：**创建一个通用求解器，创建后我们可以添加我们的约束条件，进行下一步的求解。

add()：添加约束条件（方程）**，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式。

**check()：**通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会回显unsat。

**model()：**在存在解的时候，该函数会将每个限制条件所对应的解集取交集，进而得出正解。

更多的使用方法大家可以参考这个说明文档[Z3 API IN PYTHON 中文文档 （官方文档翻译）](https://arabelatso.github.io/2018/06/14/Z3 API in Python/)

和z3py namespace reference。

四、一个nssctf例题脚本：

1
2
3
4
5
6
7
8
9
10
11
12
13
from z3 import *

v,w,x,y,z=Ints("v w x y z")
s=Solver()
s.add(v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322)
s.add(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724)
s.add(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529)
s.add (v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457)
s.add (v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)
if s.check() == sat:
    print(s.model())
else:
    print("无解")