23R3F's Blog

初探Z3约束求解器

字数统计: 1k阅读时长: 4 min
2019/04/02 Share

Z3 是一个微软出品的开源约束求解器,功能十分强大,尤其是运用于逆向的时候,进行约束求解十分快速,这里写写学z3的一些操作

安装

首先讲讲安装,说实话这玩意玄学问题还是蛮多的,在安装的时候会出现各种各样的坑,最后我在win10下和Ubuntu16.04下都安装成功了

win 10

首先下载github上的文件,解压,进入z3目录

在菜单栏中输入vs,搜索出这个工具,再选择打开文件位置(这个东西你得在电脑上安装了vs才有的)

1554180376853

选择这个,以管理员权限运行

1554180691077

接着就是输入命令了:

1
2
3
python scripts/mk_make.py -x
cd build
nmake

安装好了以后需要配置两个环境变量

新建PYTHONPATH变量,变量内容是:C:\z3\build\python\

在path变量中添加:C:\z3\build\

如图

1554181707077

1554181728624

然后进入python交互环境,输入 import z3,无报错说明就安装成功了

1554181835921

Ubuntu

Ubuntu也是一样的,下载好zip后解压进入z3目录

然后执行命令

1
2
3
python scripts/mk_make.py
cd build
make

同样的设置环境变量

sudo gedit /etc/environment

修改文件,在最后一行加上:

PYTHONPATH=”/z3/build/python”
LD_LIBRARY_PATH=”/z3/build/“

重启Ubuntu,在python输入 import z3,无报错说明就安装成功了

ps:如果想要用python虚拟环境安装z3的话可以参考1mpossible师傅的教程

使用

先来看个最简单的模版实例

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

x = Int('x') #定义一个整数型x变量
y = Int('y') #定义一个整数型y变量
s = Solver() #生成一个约束求解器
s.add(x > 2) #添加约束条件 x > 2
s.add(y < 10) #添加约束条件 y < 10
s.add(x + 2*y == 7) ##添加约束条件 x + 2*y == 7


if s.check()==sat:#检查是否有解,如果有,返回sat; 如果不满足,返回unsat
print(s.model())#输出结果

'''
输出:
[y = 0, x = 7]
'''

可以创建实数用于解次方的问题

1
2
3
x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)

函数set_option用于配置Z3环境。它用于设置全局配置选项,比如设置结果如何显示。set_option(precision = 30)设置显示结果时使用的小数位数为30。而?标记在1.2599210498?中表示输出被截断。

1
2
3
4
5
6
7
8
set_option(precision=30)
print "Solving, and displaying result with 30 decimal places"
solve(x**2 + y**2 == 3, x**3 == 2)
'''
输出
[x = 1.259921049894873164767210607278?,
y = -1.188528059421316533710369365015?]
'''

函数Q(num,den)创建一个Z3有理数,其中num是分子,den是分母。
RealVal(1)创建了表示为1的Z3实数

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
print 1/3
print RealVal(1)/3
print Q(1,3)

x = Real('x')
print x + 1/3
print x + Q(1,3)
print x + "1/3"
print x + 0.25

'''
0
1/3
1/3
x + 0
x + 1/3
x + 1/3
x + 1/4
'''

有理数也可以用十进制表示法显示。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
x = Real('x')
solve(3*x == 1)

set_option(rational_to_decimal=True)
solve(3*x == 1)

set_option(precision=30)
solve(3*x == 1)

'''
[x = 1/3]
[x = 0.3333333333?]
[x = 0.333333333333333333333333333333?]
'''

布尔运算符:And, Or, Not, Implies (implication), If (if-then-else)

双蕴含符号用==表示。

以下示例显示如何解决一组简单的布尔约束。

输入:

1
2
3
4
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))

输出:

1
[q = False, p = False, r = True]

pop / push 保护现场

从这两个名称可以推测是跟栈结构,保护现场有关的操作

来看个例子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
#coding:utf-8
from z3 import *

x = Int('x')
y = Int('y')
s = Solver()

s.add(x > 100, y == 2*x + 2)
print s.check()
print s
print "------------------"
s.push()#保存上面的约束条件,并且追加下面的条件
s.add(y <200)
print s
print s.check()

print "------------------"
s.pop()
print s#恢复加入“y <200”前的约束结果
print s.check()

输出:

1
2
3
4
5
6
7
8
sat
[x > 100, y == 2*x + 2]
------------------
[x > 100, y == 2*x + 2, y < 200]
unsat
------------------
[x > 100, y == 2*x + 2]
sat

可以看到,保存现场的操作就是这样实现的

例题

  1. 2019看雪CTF-Q1:RePwn

参考

官方:

https://github.com/Z3Prover/z3

http://z3prover.github.io/api/html/namespacez3py.html

大佬:

https://arabelatso.github.io/2018/06/14/Z3%20API%20in%20Python/

http://myhackerworld.top/2018/09/25/%E5%88%9D%E8%AF%86z3/

http://xj.poke8.com/?p=149

CATALOG
  1. 1. 安装
    1. 1.1. win 10
    2. 1.2. Ubuntu
  2. 2. 使用
  3. 3. 例题
  4. 4. 参考