Z3-Solver

简介

Z3 Solver是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题

Z3 Solver支持多种不同的问题领域，包括布尔逻辑、整数和实数的线性和非线性算术、位向量、数组、集合、函数等，主要应用领域包括软件验证、形式化验证、程序分析、人工智能和自动定理证明等

语法

z3中有3种类型的变量，分别是整型(Int)，实型(Real)和向量(BitVec)

对于整数类型数据，基本API：

  1. Int(name, ctx=None)，创建一个整数变量，name是名字
  2. Ints (names, ctx=None)，创建多个整数变量，names是空格分隔名字
  3. IntVal (val, ctx=None)，创建一个整数常量，有初始值，没名字

对于实数类型的API与整数类型一致，向量(BitVec)则稍有区别：

  1. Bitvec(name,bv,ctx=None)，创建一个位向量，name是他的名字，bv表示大小
  2. BitVecs(name,bv,ctx=None)，创建一个有多变量的位向量，name是名字，bv表示大小
  3. BitVecVal(val,bv,ctx=None)，创建一个位向量，有初始值，没名字

simplify(表达式)，对可以简化的表达式进行简化

应用

直接调用solve() 函数

solve() 函数会创造一个 solver，然后对括号中的约束条件进行求解，需要注意默认情况下只会找到满足条件的一组解，因此提供约束条件时尽可能详尽，一个例子：

1
2
3
4
5
from z3 import *
x = Int('x')                                         #声明变量
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)                   #添加约束条件
>>>[y = 0, x = 7]

solve()函数会自动打印解，不需要再套一层print()

创建Solver求解器

基本按照 创建约束求解器、声明变量 -> 添加约束条件 -> 验证是否有解 -> 求解 的步骤进行

1
2
3
4
5
6
7
8
9
10
from z3 import *
s = Solver()                #创建约束求解器
x = Int('x')                #声明变量
y = Int('y')
s.add(x > 2)                #添加约束条件
s.add(y < 10)
s.add(x + 2*y == 7)
if s.check() == sat:        #验证是否有解
	print(s.model())        #求解并打印
>>>[y = 0, x = 7]

例题

解数独

文章链接：Python Z3约束求解器解决数独问题

[GUET-CTF2019]re

前面脱壳逆向的过程略，找到关键函数

出现这么多线性判断语句，考虑用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
from z3 import *
s = Solver()
a1 = [Int("[a1[%d]" % i) for i in range(32)]

s.add( 1629056 * a1[0] == 166163712 )
s.add( 6771600 * a1[1] == 731332800 )
s.add( 3682944 * a1[2] == 357245568 )
s.add( 10431000 * a1[3] == 1074393000 )
s.add( 3977328 * a1[4] == 489211344 )
s.add( 5138336 * a1[5] == 518971936 )
s.add( a1[6] == 49 )
s.add( 7532250 * a1[7] == 406741500 )
s.add( 5551632 * a1[8] == 294236496 )
s.add( 3409728 * a1[9] == 177305856 )
s.add( 13013670 * a1[10] == 650683500 )
s.add( 6088797 * a1[11] == 298351053 )
s.add( 7884663 * a1[12] == 386348487 )
s.add( 8944053 * a1[13] == 438258597 )
s.add( 5198490 * a1[14] == 249527520 )
s.add( 4544518 * a1[15] == 445362764 )
s.add( 3645600 * a1[17] == 174988800 )
s.add( 10115280 * a1[16] == 981182160 )
s.add( 9667504 * a1[18] == 493042704 )
s.add( 5364450 * a1[19] == 257493600 )
s.add( 13464540 * a1[20] == 767478780 )
s.add( 5488432 * a1[21] == 312840624 )
s.add( 14479500 * a1[22] == 1404511500 )
s.add( 6451830 * a1[23] == 316139670 )
s.add( 6252576 * a1[24] == 619005024 )
s.add( 7763364 * a1[25] == 372641472 )
s.add( 7327320 * a1[26] == 373693320 )
s.add( 8741520 * a1[27] == 498266640 )
s.add( 8871876 * a1[28] == 452465676 )
s.add( 4086720 * a1[29] == 208422720 )
s.add( 9374400 * a1[30] == 515592000 )
s.add( 5759124 * a1[31] == 719890500 )

if s.check() == sat:
    m = s.model()
    #直接print(m)输出的是解，用eval和as_long处理一下
    for i in range(32):
        print(chr(m.eval(a1[i]).as_long()),end='')

这题有两个坑，一个是a1[6]不在这个判断条件中，一个是a1[16]和a1[17]位置调换了

*关于调整解的格式的补充

a1[6]要添加在约束条件中，不然最后输出会报错，有大佬指出用burp爆破可以得到本题的a1[6]

而且不能写成

1
print(" ".join([m.eval(a1[i]).as_long() for i in range(32)]))

(我不知道为什么

有时候在使用.as_long() / .as_fraction()时会报错

AttributeError: 'NoneType' object has no attribute 'as_long'

解决方法详见链接：Z3求解器结果输出（python