z3约束求解

发表于 分类于 本文字数： 1.3k

我不识青天高 黄地厚

z3-solver

https://ctf-wiki.org/reverse/tools/constraint/z3/

Z3 solver 是由微软开发的 可满足性模理论求解器（Satisfiability Modulo Theory solver， 即 SMT solver），用于检查逻辑表达式的可满足性，并可以找到一组约束中的其中一个可行解（无法找出所有的可行解）。

image-20260308114620657

可以使用 z3 来辅助求解一些较为复杂的约束条件

安装

1
pip3 install z3-solver

使用

总之就是声明未知数，创建solver对象（可以加一些约束条件），然后就把所有方程喂给它，让它去求解

1
2
3
4
5
6
7
8
9
10
11
12
13
14
from z3 import *
 
#创建未知数变量
v = [Int(f'v{i}')    for i in range(0, 16)]
 
#创建解释器对象
solver = Solver()#创建一个求解器对象

# 限制字符范围为可见 ASCII 码 (32-126)
for i in range(0, 16):
    s.add(v[i] >= 32, v[i] <= 126)

#添加约束方程
solver.add(v[0] * 7 == 546)

一些点

其他运算

z3中可以添加：

乘法方程。但是变量乘变量会导致复杂度大增

取模。

异或。但是只能用于位向量（BitVec）类型，不能用于整数（Int）类型

额外约束

（加快求解速度以及排除错误解）

求解flag问题可以添加可见ASCII范围约束（32-126）

根据题目内容可添加其他约束

求多解

默认只返回一解。如果需要多解或者其他解，可以通过添加约束来排除当前解来实现

题

参考：https://blog.csdn.net/liKeQing1027520/article/details/138047537

摸索着出了一题（？）还是不要作为什么严肃的参考了但是可以看看

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
#include <stdio.h>
#include <string.h>

int frame_dummy()
{
  char flag[100] = "flag is like 'flag{...}'";
  for (int i = 0; i < strlen(flag); i++)
  {
    printf("%d ", (flag[i] + 999) % 26);
  }
  return 0;
}

int main()
{
  char flag[32];
  int v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20;
  printf("Please input your flag: ");
  scanf("%s", flag);

  v20 = flag[0];
  v19 = flag[1];
  v18 = flag[2];
  v17 = flag[3];
  v16 = flag[4];
  v15 = flag[5];
  v14 = flag[6];
  v13 = flag[7];
  v12 = flag[8];
  v11 = flag[9];
  v10 = flag[10];
  v9 = flag[11];
  v8 = flag[12];
  v7 = flag[13];
  v6 = flag[14];
  v5 = flag[15];
  v4 = flag[16];
  v3 = flag[17];
  v2 = flag[18];
  v1 = flag[19];

  int f = 0;
  if (3 * v20 == 306 && v19 + v18 == 205 && v17 * 2 + v16 == 329 && v15 + v14 + v13 == 237 && v12 - v11 == 42 && v10 * 10 == 530 && v9 + v8 + v7 == 311 && v6 - v5 == 7 && v4 + v3 == 197 && v2 + v1 == 244 && v20 + v19 + v18 + v17 == 410 && v16 + v15 + v14 + v13 == 360 && v12 + v11 + v10 + v9 == 338 && v8 + v7 + v6 + v5 == 443 && v4 + v3 + v2 + v1 == 441 && v20 + v16 + v12 + v8 + v4 == 543 && v19 + v15 + v11 + v7 + v3 == 473 && v18 + v14 + v10 + v6 + v2 == 491 && v17 + v13 + v9 + v5 + v1 == 485)
  {
    f = 1;
  }

    if (f && v20 % 7 == 4 && v12 + 2 * v11 == 261 && v8 - v7 == -8 && v2 ^ v1 == 10 && (v20 + v19) % 13 == 2 && (v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20) == 1992 && v20 % 6 == 0 && v19 % 6 == 0 && v16 % 2 == 1)
      f = 1;
    else f = 0;

    if (f)
    {
      printf("Right\n");
    }
    else
    {
      printf("Wrong\n");
    }
  return 0;
}

解。要手动加一个最后一个字符是}的约束。或者暴力求多解也行

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
from z3 import *

v = [Int(f'v{i}') for i in range(21)] 

s = Solver()

# 限制字符范围为可见 ASCII 码 (32-126)
for i in range(1, 21):
    s.add(v[i] >= 32, v[i] <= 126)

# --- 基础线性约束 ---
s.add(3 * v[20] == 306)
s.add(v[19] + v[18] == 205)
s.add(v[17] * 2 + v[16] == 329)
s.add(v[15] + v[14] + v[13] == 237)
s.add(v[12] - v[11] == 42)
s.add(v[10] * 10 == 530)
s.add(v[9] + v[8] + v[7] == 311)
s.add(v[6] - v[5] == 7)
s.add(v[4] + v[3] == 197)
s.add(v[2] + v[1] == 244)

s.add(v[20] + v[19] + v[18] + v[17] == 410)
s.add(v[16] + v[15] + v[14] + v[13] == 360)
s.add(v[12] + v[11] + v[10] + v[9] == 338)
s.add(v[8] + v[7] + v[6] + v[5] == 443)
s.add(v[4] + v[3] + v[2] + v[1] == 441)

s.add(v[20] + v[16] + v[12] + v[8] + v[4] == 543)
s.add(v[19] + v[15] + v[11] + v[7] + v[3] == 473)
s.add(v[18] + v[14] + v[10] + v[6] + v[2] == 491)
s.add(v[17] + v[13] + v[9] + v[5] + v[1] == 485)

# --- 新增的高级约束 (取模、异或、求和) ---
s.add(v[20] % 7 == 4)
s.add(v[12] + 2 * v[11] == 261)
s.add(v[8] - v[7] == -8)
s.add((v[20] + v[19]) % 13 == 2)
# 全局求和约束
s.add(Sum([v[i] for i in range(1, 21)]) == 1992)
s.add(v[20] % 6 == 0)
s.add(v[19] % 6 == 0)
s.add(v[16] % 2 == 1)
s.add(v[1] == 125) # 加

# --- 求解 ---
if s.check() == sat:
    m = s.model()
    # 按照 flag[0]-flag[19] 顺序排列 (v20 down to v1)
    res = "".join([chr(m[v[i]].as_long()) for i in range(20, 0, -1)])
    print(f"解密成功！")
    print(f"Flag 字符串为: {res}")
    
else:
    print("错误：在该约束条件下无解（Unsat）。")

image-20260308200839490

约束条件转换脚本

后面再研究

https://blog.csdn.net/liKeQing1027520/article/details/141174137?spm=1001.2014.3001.5502

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
import re
 
def replace_func(match):
    shift = 2 #shift是指第一个未知数和0的差，例如：如果题目中第一个未知数是v2（如果是v3），那么shift就设置成2（就设置成3）
    index = int(match.group(1)) - shift
    return str(f'v[{index}]')  # 返回字符串'v[a后数字-1]'，用其替换匹配到的an
 
 
if __name__ == '__main__':
    s1 = ""  # 定义包含an的字符串
 
    s1 = re.sub(r'v(2[0-9]|1[0-9]|[1-9])', replace_func, s1)
    # sub函数参数, pattern、repl、string分别表示：正则表达式匹配规则、替换后结果（可以是函数也可以是常量）、要被查找替换的原始字符串
    s1 = re.sub('!', '=', s1) #有些题目给的条件的方程是用'||'关系运算符连接的不等式方程，需要用这一行代码将'!'替换成'='变成等式方程
    res = s1.split('| | ')
    print(res)