z3是一个约束求解器，可以理解为解方程的工具，每一个约束都要写在x.add的语句中。

声明变量

z3一共有三种变量

1
2
3
a,b = Int('a b')#声明多个整数型变量
a = Real('a')#声明单个实型变量
a,b = Bitvec('a b',8)#声明多个8位的向量型变量

使用例

1
2
3
a,b = Int('a b')
solve(a+b == 10,a + 3 * b ==12)#条件少时可以直接用solve不用add
#result : [b = 1,a = 9]
1
2
3
4
5
6
7
8
9
x=Int('x')
y=Int('y')
print (simplify(x + y + 2*x + 3))#simplify用于打印化简后的表达式
print (simplify(x < y + x + 2))
print (simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))

#3 + 3*x + y
#Not(y <= -2)
#And(x >= 2, 2*x**2 + y**2 >= 3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
from z3 import *
a,b = Ints('a b')

s=Solver()  #创建一个解的对象s
s.add(a + b == 10)#添加约束条件
s.add(a + 3 * b == 12)

if s.check() == sat: #check() 检查解是否存在，存在会return 'sat'
	result = s.model() #输出

print(result)

print(result[a])
print(result[b])

z3语法

对于普通的自定义逻辑（带位移，异或之类的不好逆向），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
from prism import *

cmp = [0x66, 0x4E, 0xA9, 0xFD, 0x3C, 0x55, 0x90, 0x24, 0x57, 0xF6, 0x5D, 0xB1, 0x01, 0x20, 0x81, 0xFD, 0x36, 0xA9, 0x1F, 0xA1, 0x0E, 0x0D, 0x80, 0x8F, 0xCE, 0x77, 0xE8, 0x23, 0x9E, 0x27, 0x60, 0x2F, 0xA5, 0xCF, 0x1B, 0xBD, 0x32, 0xDB, 0xFF, 0x28, 0xA4, 0x5D]
f = Solver()

flag,out = pini(42)


m = n = a = 0
for i,j in pl(7,6):
    a = 6 * i + j
    m = flag[a]
    n = flag[a]
    m = ~m
    m &= i * (j + 2)
    n = n & ~(i * (j + 2)) | m
    a = 7 * j + i
    out[a] = n
for i in range(1,42):
    if ( i % 2 == 1 ):
        out[i] *= 107
    else:
        out[i] += out[i - 1]

for i in range(42):
    f.add(cmp[i]==out[i])
isflag(f,flag)
pcheck(f,flag)

但是可能遇到要对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
int __fastcall main(int argc, const char **argv, const char **envp)
{
  size_t v3; // rax
  char flag[64]; // [rsp+0h] [rbp-C0h] BYREF
  char out2[64]; // [rsp+40h] [rbp-80h] BYREF
  __int64 check[4]; // [rsp+80h] [rbp-40h]
  __int16 v8; // [rsp+A0h] [rbp-20h]
  int len; // [rsp+B0h] [rbp-10h]
  int v10; // [rsp+B4h] [rbp-Ch]
  int v11; // [rsp+B8h] [rbp-8h]
  int i; // [rsp+BCh] [rbp-4h]

  check[0] = 0x10C0105000D07LL;
  check[1] = 0xF0509000F050D00LL;
  check[2] = 0x701030305020003LL;
  check[3] = 0xC02070201020B07LL;
  v8 = 514;
  i = 0;
  v11 = 0;
  v10 = 0;
  len = 17;
  puts("Hi, PLZ input input");
  memset(flag, 0, sizeof(flag));
  memset(out2, 0, sizeof(out2));
  __isoc99_scanf("%s", flag);
  v3 = strlen(flag);
  if ( v3 == len )
  {
    for ( i = 0; i <= 16; ++i )
    {
      if ( (unsigned __int8)flag[i] > '`' && (unsigned __int8)flag[i] <= 'z' )
        flag[i] = (flag[i] ^ 0x47) + 1;
      if ( (unsigned __int8)flag[i] > '@' && (unsigned __int8)flag[i] <= 'Z' )
        flag[i] = (flag[i] ^ 0x4B) - 1;
      out2[2 * i] = (unsigned __int8)flag[i] >> 4;
      out2[2 * i + 1] = flag[i] & 0xF;
    }
    for ( i = 0; i < len; ++i )
    {
      if ( *((_BYTE *)check + 2 * i) != out2[2 * (len - i) - 2]
        && *((_BYTE *)check + 2 * i + 1) != out2[2 * (len - i) - 2] )
      {
        printf("wrong wrong wrong");
        return 0;
      }
    }
    printf("woc,you got it,flag is your input");
    return 0;
  }
  else
  {
    printf("a Ha ? wrong1");
    return 0;
  }
}

主函数是这样的，这里它不止对flag进行分类讨论，还在讨论后进行计算：z3型可以直接进行计算，包括加和乘，对于位向量还可以左右移以及异或，但是都不能进行判断大小，如果要进行判断必须要在add中做判断，比如判断两个值是否相等：

1
f.add(check[2 * i]==out3[2*(len-i-1)])

那么如果我们根据这道题写，还需要If函数（Z3自带）

1
If(condition,a,b)

意思是：如果条件成立，语句视为a，否则视为b

那么和add结合起来看就是：

1
2
f.add(If(And(out[i] > 0x60, out[i] <= 0x7a), out2[i] == (out[i] ^ 0x47) + 1, True))
f.add(If(And(out[i] > 0x40, out[i] <= 0x5a), out2[i] == (out[i] ^ 0x4b) - 1, True))

如果条件成立，添加a约束，否则添加b约束，这里的b约束恒为真，表示如果条件不成立就跳过这个约束。可是问题来了，我们知道out[i]是由flag初始化的，也就是说out是z3位向量型，但是out2呢？如果把这里的out2视作一个普通列表，让out[i]计算后的值返回给out2，好像也没问题。但是！！这里的语句并不是赋值语句，而是判断语句，是一个约束，如果这里out2=34*[0],那么就是让out[i]运算后的值恒等于0的条件成立，显然这是无解的，也就是说，这里的两个变量都必须是位向量才可以，同时，不应该忘了如果两个条件均不成立，就要让out=out2

1
f.add(out2[i] == If(And(out[i] > 0x40, out[i] <= 0x5a), (out[i] ^ 0x4b) - 1,If(And(out[i] > 0x60, out[i] <= 0x7a), (out[i] ^ 0x47) + 1, out[i])))

进行if的嵌套完成这个效果

之后还要对flag继续做变换变成最后的数组，且数组大小翻倍，如果后面的检查比较简单，可以直接在check==的时候写，但是由于这里的比较不是很直观，不如写出来变成单独的列表再比较，这时又要涉及到out2变成out3的问题了，由于这个是直接赋值，没有判断，所以方便起见，直接写赋值语句。

1
2
out3[2*i] = LShR(out2[i], 4)
out3[2*i+1] = out2[i] & 0xf

通过这两个例子可以发现，当想要赋值时，如果要对z3型变量进行判断/比较，就必须用add表达式，在其中，为了达成赋值效果，必须新建一个z3量才可以成功，但是如果是直接赋值，则直接对列表赋值即可。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
from prism import *
check = [0x07, 0x0D, 0x00, 0x05, 0x01, 0x0C, 0x01, 0x00, 0x00, 0x0D, 0x05, 0x0F, 0x00, 0x09, 0x05, 0x0F, 0x03, 0x00, 0x02, 0x05, 0x03, 0x03, 0x01, 0x07, 0x07, 0x0B, 0x02, 0x01, 0x02, 0x07, 0x02, 0x0C, 0x02, 0x02]
flag,out = pini(17)
out2 = [BitVec('out2[%2d]' % i , 8) for i in range (34)]
out3 = [0]*34
len = 17
f = Solver()

for i in range(17):

    f.add(out2[i] == If(And(out[i] > 0x40, out[i] <= 0x5a), (out[i] ^ 0x4b) - 1,
                     If(And(out[i] > 0x60, out[i] <= 0x7a), (out[i] ^ 0x47) + 1, out[i])))

    out3[2*i] = LShR(out2[i], 4)
    out3[2*i+1] = out2[i] & 0xf
isflag(f,flag)

for i in range(17):
    f.add(check[2 * i]==out3[2*(len-i-1)])
    f.add(check[2 * i + 1]==out3[2*(len-i-1)+1])
pcheck(f,flag)
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
"la!{S3ch_A_EZVM}
flag{Su%0_A_EZVM}
fl'g{Su%0_A_EZVM}
fl'g{Su%h_A_EZVM}
"l'g{Su%h_A_EZVM}
"l'!{Su%h_A_EZVM}
"l'!{Such_A_EZVM}
",'!{Su%h_A_EZVM}
",'!{S3%h_A_EZVM}
",'!{S3ch_A_EZVM}
f,'!{S3%h_A_EZVM}
fl'!{S3%h_A_EZVM}
fla!{S3%h_A_EZVM}
"la!{S3%h_A_EZVM}
fla!{S3ch_A_EZVM}
f,a!{S3ch_A_EZVM}
f,a!{Such_A_EZVM}
f,a!{Su%h_A_EZVM}
",a!{Su%h_A_EZVM}
"la!{Su%h_A_EZVM}
fl'!{Su%h_A_EZVM}
f,'!{Su%h_A_EZVM}
",'g{Su%h_A_EZVM}
f,'g{Su%h_A_EZVM}
",'g{S3%h_A_EZVM}
f,'g{S3%h_A_EZVM}
fl'g{S3%h_A_EZVM}
"l'g{S3%h_A_EZVM}
"l'!{S3%h_A_EZVM}
flag{S3%h_A_EZVM}
f,ag{S3%h_A_EZVM}
flag{Su%h_A_EZVM}
f,ag{Su%h_A_EZVM}
fla!{Su%h_A_EZVM}
f,a!{S3%h_A_EZVM}
"lag{Su%h_A_EZVM}
"lag{S3%h_A_EZVM}
",ag{Su%h_A_EZVM}
",a!{S3%h_A_EZVM}
",ag{S3%h_A_EZVM}
"l'!{S3ch_A_EZVM}
fl'!{S3ch_A_EZVM}
f,'!{S3ch_A_EZVM}
",a!{S3ch_A_EZVM}
fl'!{Such_A_EZVM}
f,'!{Such_A_EZVM}
",'!{Such_A_EZVM}
",a!{Such_A_EZVM}
fla!{Such_A_EZVM}
"la!{Such_A_EZVM}
fl'g{Such_A_EZVM}
fl'g{S3ch_A_EZVM}
flag{Such_A_EZVM}
f,ag{Such_A_EZVM}
f,'g{Such_A_EZVM}
f,ag{S3ch_A_EZVM}
flag{S3ch_A_EZVM}
f,'g{S3ch_A_EZVM}
"lag{S3ch_A_EZVM}
"l'g{S3ch_A_EZVM}
"lag{Such_A_EZVM}
"l'g{Such_A_EZVM}
",ag{Such_A_EZVM}
",ag{S3ch_A_EZVM}
",'g{Such_A_EZVM}
",'g{S3ch_A_EZVM}
",'!{Su%0_A_EZVM}
",'g{Su%0_A_EZVM}
f,'!{Su%0_A_EZVM}
",'!{Suc0_A_EZVM}
",'g{Suc0_A_EZVM}
f,'!{Suc0_A_EZVM}
f,'g{Su%0_A_EZVM}
f,'g{Suc0_A_EZVM}
"l'g{Su%0_A_EZVM}
"l'g{Suc0_A_EZVM}
"l'!{Su%0_A_EZVM}
"l'!{Suc0_A_EZVM}
fl'!{Su%0_A_EZVM}
fl'!{Suc0_A_EZVM}
fl'g{Suc0_A_EZVM}
f,ag{Su%0_A_EZVM}
",ag{Su%0_A_EZVM}
"lag{Su%0_A_EZVM}
",ag{Suc0_A_EZVM}
"lag{Suc0_A_EZVM}
f,ag{Suc0_A_EZVM}
flag{Suc0_A_EZVM}
f,a!{Su%0_A_EZVM}
f,a!{Suc0_A_EZVM}
",a!{Su%0_A_EZVM}
",a!{Suc0_A_EZVM}
"la!{Su%0_A_EZVM}
fla!{Su%0_A_EZVM}
"la!{Suc0_A_EZVM}
fla!{Suc0_A_EZVM}
"l'!{S3c0_A_EZVM}
"la!{S3c0_A_EZVM}
"l'g{S3c0_A_EZVM}
"lag{S3c0_A_EZVM}
",'g{S3c0_A_EZVM}
",ag{S3c0_A_EZVM}
",'!{S3c0_A_EZVM}
",a!{S3c0_A_EZVM}
",'!{S3%0_A_EZVM}
",'g{S3%0_A_EZVM}
"l'!{S3%0_A_EZVM}
"la!{S3%0_A_EZVM}
",a!{S3%0_A_EZVM}
",ag{S3%0_A_EZVM}
"lag{S3%0_A_EZVM}
"l'g{S3%0_A_EZVM}
f,'g{S3c0_A_EZVM}
f,'g{S3%0_A_EZVM}
fl'g{S3c0_A_EZVM}
fl'g{S3%0_A_EZVM}
flag{S3c0_A_EZVM}
f,ag{S3c0_A_EZVM}
f,ag{S3%0_A_EZVM}
flag{S3%0_A_EZVM}
fla!{S3c0_A_EZVM}
fla!{S3%0_A_EZVM}
fl'!{S3c0_A_EZVM}
f,'!{S3c0_A_EZVM}
f,a!{S3c0_A_EZVM}
f,a!{S3%0_A_EZVM}
f,'!{S3%0_A_EZVM}
fl'!{S3%0_A_EZVM}

以上均是解

补充说明：

如果想约束某个值只能出现一次，比如{,}，可以用Sum：

Sum用于计算一系列表达式的和类似于加

1
2
s.add(Sum([If(i == BitVecVal(ord('{'), 8), 1, 0) for i in flag]) <= 1)
s.add(Sum([If(i == BitVecVal(ord('}'), 8), 1, 0) for i in flag]) <= 1)

计算flag中等于括号的值的表达式个数，然后让其小于等于1