安装

Z3由微软开发的一套约束求解器，你可以简单的理解它是解方程的神器。 在CTF中有的题目可能会遇到给你一堆条件，但是写不出逆向脚本，或者是使用爆破手段获取flag的时间过长，此时z3的作用便发挥了出来。

由于在上一篇 angr学习笔记中已经了解了虚拟环境 virtualenvwrapper 的用法，我们直接mkvirtualenv --python=$(which python3) z3 && pip install z3-solver即可隔离出一个z3环境，避免与angr冲突。

或者通过如下命令：

1
2
3
4
5
6
7
8
9
10
11
12
13
# 在当前目录下创建名为 angr-venv的新目录，包含干净的python环境
python3 -m venv z3-venv

Windows：
angr-venv\Scripts\activate

Linux/Mac：
source z3-venv/bin/activate

pip install z3-solver

退出虚拟环境：
deactivate

示例

最简单的例子

假如我有一个方程

用z3求解的脚本

1
2
3
4
from z3 import *
x = Int('x')
y = Int('y')
solve(x + y == 4)

上例中，x是脚本中的变量，Int(‘x’)是在输出时对应变量x的名称。如果运行以上脚本，得到的答案为[x = 0, y = 1]，如果我们这么写

1
2
3
4
from z3 import *
x = Int('flag[0]')
y = Int('flag[1]')
solve(x + y == 4)

那么输出就是[ flag[0] = 0, flag[1] = 4]

当然这是一个不定方程，如果要得到x = 3的解，我们就要增加约束，比如

1
2
3
4
5
from z3 import *
x = Int('x')
y = Int('y')
solve(x + y == 4)
solve(x == 3)

这样输出就是[x = 3, y = 1]

变量声明与约束器solver的建立

可以使用Int,Real,BitVec等声明一个整数或实数变量，也可以申明一个变量数组，如

1
2
3
4
5
knownarr = [IntVal(i) for i in encrypted]
message = [Int('flag%d' % i) for i in range(len(encrypted)-1)]
first = IntVector(‘a’, 4)

后面都可以通过arrayname[id]进行访问

一道例题

做hgame遇到一道矩阵乘法的题，刚好看到一篇博客有类似的题，就拿来做例题吧，等比赛结束了把赛题补上。

反编译后得到的源代码：

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
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int v4; // [esp+14h] [ebp-Ch]
  int k; // [esp+18h] [ebp-8h]
  int i; // [esp+1Ch] [ebp-4h]
  int j; // [esp+1Ch] [ebp-4h]

  __main();
  v4 = 0;
  gets(flag);
  for ( i = 0; i <= 35; ++i )
  {
    if ( !flag[i] )
    {
      flag[i] = 1;//flag长度并没有36位，为了凑够36位在flag后面补了数字1
      ++v4;
    }
  }
  if ( v4 != 9 )//可以看出补了9个数字1
    exit(0);
  convert(a);//把flag赋值给a，a是一个6*6的矩阵
  Transposition(a);//把a的转置矩阵赋值给b
  Multi(a, b);//把a * b的结果赋值给c
  for ( j = 0; j <= 5; ++j )
  {
    for ( k = 0; k <= 5; ++k )
    {
      if ( c[j][k] != d[j][k] )//比较c和d
        exit(0);
    }
  }
  printf("congratulations!you have gottern the flag!");
  return 0;
}

如果爆破的话，复杂度极高，可能要跑很长时间，那么我们采用z3求解器该怎么做呢？

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 *
import time
t1 = time.time()
#创建一个解决方案实例
solver = Solver()
#flag长度先设置为36，包括尾部的9个1
flag = [Int('flag%d'%i) for i in range(36)]
#保存flag的矩阵
a = [i for i in flag]
#保存flag的转置矩阵
b = [i for i in range(36)]
#保存a*b的矩阵
c = [0 for i in range(36)]
#堆中正确flag的运算结果
d = [0x12027,0x0F296,0x0BF0E,0x0D84C,0x91D8,0x297,
	0x0F296,0x0D830,0x0A326,0x0B010,0x7627,0x230,
	0x0BF0E,0x0A326,0x8FEB,0x879D,0x70C3,0x1BD,
	0x0D84C,0x0B010,0x879D,0x0B00D,0x6E4F,0x1F7,
	0x91D8,0x7627,0x70C3,0x6E4F,0x9BDC,0x15C,
	0x297,0x230,0x1BD,0x1F7,0x15C,0x6]
#获得a的转置矩阵
for i in range(6):
	for j in range(6):
		b[i+6*j] = a[6*i+j]
#运算a*b
for i in range(6):
	for j in range(6):
		for k in range(6):
			c[j+6*i] = c[j+6*i] + a[6*i+k]*b[6*k+j]
		#添加约束，正确flag的运算结果
		solver.add(simplify(c[j+6*i]) == d[j+6*i])
#添加约束，除了尾部，flag的字符一定在可见字符范围内
for i in range(6,36-10):
	solver.add(flag[i]>=32)
	solver.add(flag[i]<=127)
#添加约束，由于flag有格式，前6位一定为whctf{
for i in range(6):
	solver.add(flag[i] == ord('whctf{'[i]))
#添加约束，flag的尾部为9个1
for i in range(36-9,36):
	solver.add(flag[i] == 0x1)
#添加约束，flag的最后一个肯定是}
solver.add(flag[-10] == ord('}'))
#这里一定要有，不check的话会报错
if solver.check() == sat:
	m = solver.model()
	s = []
	#获得结果
	for i in range(36):
		s.append(m[flag[i]].as_long())
	#输出flag
	print(bytes(s))
else:
	print('error')

这个脚本还有点问题，但是结构是对的，赛后和hagme题解交叉引用一下（doge）