z3py api guide

z3 是微软开发的的高性能约束求解工具。z3有许多发行版,C、.net、Python等。本文介绍CTF中常用的Python API。

数据类型

\$1 \$2 表示第1,2个参数。以此类推

数学类型

函数名 说明
Int 定义一个整数,这里的整数是数学意义上的整数,不是C中int x = Int('x')
Ints 定义几个整数 x, y = Ints('x y')
IntVector 以\$1为前缀定义,定义\$2个Int x = IntVector('x', 3)
IntVal 定义值为\$1的一个Int,\$1可以是string或整数 a = IntVal(1); b=IntVal('100')
Real 定义一个实数 x = Real('x')
Reals 同Ints x = Reals('x y')
RealVector 同IntVector x = RealVector('x', 3)
RealVal 同IntVal x = RealVal('3.14')
Q 定义一个有理分数\$1/\$2 x = Q(3, 5)
RatVal 与Q一样,定义一个有理分数\$1/\$2,实际Q是调用的RatVal x = RatVal(3, 5)
Bool 定义一个布尔类型 p = Bool('p')
Bools 同Ints p, q, r = Bools('p q r')
BoolVector 同IntVector P = BoolVector('p', 3)
BoolVal 同IntVal BoolVal(True)

有限类型

函数名 说明
BitVec 定义一个名为\$1长度为\$2 bit的位向量,如BitVal(‘x’,32)表示C语言中的int x = BitVec('x', 16)
BitVecs 同Ints x, y, z = BitVecs('x y z', 16)
BitVecVal 定义值为\$1,长度为\$2 bit的位向量 v = BitVecVal(10, 32)
FPSort 按照\$1 bit指数位, \$2 bit有效位定义一个浮点类型,如FPSort(8, 24)表示C语言中float,FPSort(11, 53)表示C语言中double,当然z3已经内置了这几种类型:Float16(),Float32(),Float64(),float128() Single = FPSort(8, 24); Double = Float64()
FP 定义一个名为\$1,类型为\$2 的浮点数 x = FP('x', FPSort(8, 24))
FPs 同Ints x, y, z = FPs('x y z', FPSort(8, 24))
FPVal 定义值为\$1,类型为\$2的浮点数 v = FPVal(12.25, FPSort(8, 24))
String 定义一个名为\$1 的字符串 x = String('x')
Strings 同Ints x, y, z = Strings('x y z')
StringVal 定义一个值为\$1 的字符串 x = StringVal('x')

数学类型

Int

成员函数

函数名 返回类型 说明
as_long python int 把z3的Int转换成python的int IntVal(1).as_long()
as_string python string 把z3的Int转换成python的string IntVal(1).as_string()

运算

以下int除非特殊说明,均可使用python类型

函数名 返回类型 说明
__add__ Int 两个Int相加 Int('x') + Int('y'); Int('x') + 10
__sub__ Int 两个Int相减 Int('x') - Int('y'); Int('x') - 10
__mul__ Int 两个Int相乘 Int('x') * Int('y'); Int('x') * 10
__div__ Int 两个Int相除 Int('x') / Int('y'); Int('x') / 10
__mod__ Int 取模运算 Int('x') % Int('y'); Int('x') % 10
__neg__ Int 取相反数 -Int('x')
__pow__ Int 指数运算 Int('x') ** Int('y'); Int('x') ** 10
__eq__ Bool 得到相等的约束 Int('a') == Int('b')
__ne__ Bool 得到不等的约束 Int('a') != Int('b')
__lt__ Bool 得到小于的约束 Int('a') < Int('b')
__le__ Bool 得到小于等于的约束 Int('a') <= Int('b')
__gt__ Bool 得到大于的约束 Int('a') > Int('b')
__ge__ Bool 得到大于等于的约束 Int('a') >= Int('b')
ToReal Real 转换成Real类型 ToReal(Int('x'))
Int2BV BitVec 把\$1 转换成长\$2 bit的BitVec Int2BV(Int('x'), 32)

Real

成员函数

函数名 返回类型 说明
numerator Int 返回该数分数形式的分子 Q(3,5).numerator()
numerator_as_long python int 返回该数分数形式的分子 Q(3,5).numerator()
denominator Int 返回该数分数形式的分母 RealVal(12.25).denominator()
denominator_as_long python int 返回该数分数形式的分母 RealVal("1/3").denominator_as_long()
as_fraction python Fraction 得到该数的python Fraction对象 RealVal("1/5").as_fraction()
as_decimal python string 得到该数的小数形式并保留\$1位小数 RealVal("1/3").as_decimal(3)
as_long python int 得到该数的python整数形式,如果该数不为整数则抛异常 同Int
as_string pyhton string 同Int 同Int

运算

Int有的Real都有,同时Real特有

函数名 返回类型 说明
Cbrt Real 开三次方 Cbrt(Real('x'))
Sqrt Real 开平方 Sqrt(Real('x'))
ToInt Int 转换成Int类型 ToInt(Real('x'))

Bool

成员函数

运算

函数名 返回类型 说明
Xor Bool 异或表达式 Xor(Bool('p'), Bool('q'))
Not Bool 取非表达式 Not(Bool('p'))
And Bool 取与表达式 And(Bool('p'), Bool('q'), Bool('w'))
Or Bool 取或表达式 Or(Bool('p'), Bool('q'), Bool('w'))
Implies Bool 蕴含表达式 Implies(Bool('p'), Bool('q'))

有限类型

BitVec

成员函数

函数名 返回类型 说明
size python int 得到BitVec的长度 len = BitVec('x', 12).size()

运算

Int有的BitVec都有,长度不同的BitVec不能运算,且均为有符号运算、无符号运算见下。

函数名 返回类型 说明
BV2Int Int 把\$1 转换成Int,\$2 表示这个BitVec是否有符号 BV2Int(BitVec('x', 32), is_signed=False)
Concat BitVec 把参数中的Bitvec连接到一起 Concat(BitVec('x', 16),BitVec('y', 16))
Extract BitVec 截取\$3 从\$2 到 \$1,长度为\$1 - \$2 + 1bit的BitVec Extract(6, 2, BitVec('x', 8))
RotateLeft BitVec 把\$1 循环左移 \$2位,RotateLeft(BitVec('x', 16),4)等价于Concat(Extract(11, 0, x), Extract(15, 12, x)) RotateLeft(BitVec('x', 16),4)
RotateRight BitVec 把\$1 循环右移 \$2位 RotateRight(BitVec('x', 16),4)
RepeatBitVec BitVec 重复\$2,\$1 次RepeatBitVec(2, a)等价于Concat(a, a) RepeatBitVec(4, BitVec('x', 8))
SignExt BitVec 得到一个带有\$1 位前缀并填充1的BitVec,SignExt(8, BitVec('x', 16)等价于Concat(RepeatBitVec(8, BitVecVal(1, 1)), BitVec('x', 16)) SignExt(8, BitVec('x', 16))
ZeroExt BitVec 得到一个带有\$1 位前缀并填充0的BitVec ZeroExt(8, BitVec('x', 16))

有符号与无符号对比

有符号 说明 无符号
+ 加法 +
- 减法 -
* 乘法 *
/ 除法 UDiv
% 取模 URem
<= 小于等于 ULE
< 小于 ULT
>= 大于等于 UGE
> 大于 UGT
>> 右移运算 LShR
<< 左移运算 <<

FP

成员函数

函数名 返回类型 说明
ebits python int 得到浮点数的指数位长度
sbits python int 得到浮点数的有效位长度

运算

在看运算前,先看看浮点数的舍入规则,在z3py中定义了5种IEEE舍入规则:RoundNearestTiesToEven、RoundNearestTiesToAway、RoundTowardPositive、RoundTowardNegative、RoundTowardZero。
在IEEE 754-2019 27页中,我们找到了这五种舍入规则的定义。

函数名 别名 说明
RoundNearestTiesToEven RNE 向偶数舍入
RoundNearestTiesToAway RNA 最近舍入
RoundTowardPositive RTP 向+oo舍入
RoundTowardNegative RTN 向-oo舍入
RoundTowardZero RTZ 向0舍入

在C语言中默认的是RNE

函数名 返回类型 说明
fpNaN FP 创建一个值为NaN的FP fpNaN(FPSort(8, 24))
fpPlusInfinit FP 创建一个值为+oo的FP fpPlusInfinity(FPSort(8, 24))
fpMinusInfinity FP 创建一个值为-oo的FP fpMinusInfinity(FPSort(8, 24))
fpInfinity FP 创建一个值为+oo 或 -oo的FP fpInfinity(FPSort(8, 24), False)
fpPlusZero FP 创建一个值为+0.0的FP fpPlusZero(FPSort(8, 24))
fpMinusZero FP 创建一个值为-0.0的FP fpMinusZero(FPSort(8, 24))
fpZero FP 创建一个值为+0.0 或 -0.0的FP fpZero(FPSort(8, 24), False)
fpAbs FP 取绝对值 fpAbs(x)
fpNeg FP 取相反数 fpAbs(Neg)
fpAdd FP \$2 和 \$3按照\$1舍入规则相加 fpAdd(RNE(), x, y)
fpSub FP \$2 和 \$3按照\$1舍入规则相减 fpSub(RNE(), x, y)
fpMul FP \$2 和 \$3按照\$1舍入规则相乘 fpMul(RNE(), x, y)
fpDiv FP \$2 和 \$3按照\$1舍入规则相除 fpDiv(RNE(), x, y)
fpRem FP \$2 和 \$3按照\$1舍入规则取模 fpRem(RNE(), x, y)
fpMin FP 取出\$1与\$2较小的一个 fpMin(x, y)
fpMax FP 取出\$1与\$2较大的一个 fpMax(x, y)
fpFMA FP 按照\$1舍入规则计算\$2 * \$3 + \$4,但整个过程只进行一次舍入 fpFMA(RNE(), x, y, z)
fpSqrt FP 按照\$1 舍入规则进行开方 fpSqrt(RNE(), x)
fpRoundToIntegral Int 按照\$1舍入规则,把\$2取整 fpRoundToIntegral(RNE(), a)
fpIsNaN Bool 判断\$1是否是NaN fpIsNaN(x)
fpIsInf Bool 判断\$1是否是Inf fpIsInf(x)
fpIsZero Bool 判断\$1是否是0 fpIsZero(x)
fpIsNormal Bool 但fpIsNaN、fpIsInf、fpIsZero都不成立时此表达式为True fpIsNormal(x)
fpIsNegative Bool 判断\$1是否为负 fpIsNegative(x)
fpIsPositive Bool 判断\$1是否为正 fpIsPositive(x)
fpLT Bool \$1 < \$2 fpLT(a,b)
fpLEQ Bool \$1 <= \$2 fpLEQ(a,b)
fpGT Bool \$1 > \$2 fpGT(a,b)
fpGEQ Bool \$1 >= \$2 fpGEQ(a,b)
fpEQ Bool \$1 == \$2 fpEQ(a,b)
fpNEQ Bool \$1 != \$2 fpNEQ(a,b)
fpBVToFP FP 把\$1 按照IEEE编码转换成\$2类型的浮点数 fpBVToFP(BitVecVal(0x41440000, 32), Float32())
fpSignedToFP FP \$2 按照\$1 舍入规则转换成\$3 类型 fpSignedToFP(RNE(), BitVecVal(-5, 32), Float32())
fpUnsignedToFP FP \$2 按照\$1 舍入规则转换成\$3 类型 fpUnsignedToFP(RNE(), BitVecVal(-5, 32), Float32())
fpFPToFP FP \$2 按照\$1 舍入规则转换成\$3 类型 fpFPToFP(RNE(), FPVal(1.0, Float32()), Float64())
fpRealToFP FP \$2 按照\$1 舍入规则转换成\$3 类型 fpRealToFP(RNE(), RealVal(1.5), Float32())
fpToIEEEBV BitVec 把\$1 按照IEEE编码转换成BitVec类型 fpToIEEEBV(FP('x', FPSort(8, 24)))
fpToSBV BitVec 把\$2 按照\$1舍入规则转换成有符号BitVec类型 fpToSBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))
fpToUBV BitVec 把\$2 按照\$1舍入规则转换成无符号BitVec类型 fpToUBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))
fpToReal Real 把\$1 转换成Real类型 fpToReal(x)

String

成员函数

函数名 返回类型 说明
at String 取出第\$1个位置的值 StringVal('what is').at(2)
__add__ String Concat(\$1, \$2) String('x') + String('y')

运算

函数名 返回类型 说明
SubSeq String 从\$2 偏移处在\$1 中取出长度\$3的子串 SubSeq(s,0,4)
PrefixOf Bool 判断\$1 是否是\$2 的前缀 PrefixOf("ab", "abc")
SuffixOf Bool 判断\$1 是否是\$2 的后缀 SuffixOf("bc", "abc")
Contains Bool 判断\$1 是否包含\$2 Contains("abc", "bc")
Replace String 把\$1 中的第一个\$2 字符替换成\$3 Replace("aaa", "a", "b")
IndexOf Int 从\$3 偏移开始在\\1 中检索子串\$2,\$3默认为0 IndexOf("abcabc", "bc")
LastIndexOf Int 在\$1 中检索子串\$2 最后一个位置 LastIndexOf("abcbc","bc")
Length Int 取长度 Length(StringVal('abc'))
StrToInt Int String转Int StrToInt("1")
IntToStr String Int转String IntToStr(IntVal(123))

求解(不定时更新)

在z3py中,用Solver()创建一个求解器,利用成员函数add()添加约束,最后使用成员函数check()进行求解,成员函数model()得到求解结果。
而函数solve()则是直接在参数中添加约束,输出model()结果。
例如:

1
2
3
4
5
6
7
8
x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print(s.check())
m = s.model()
print("x = %s" % m[x])
print("y = %s" % m[y])
print("z = %s" % m[z])

数独

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
X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(9)]for i in range(9)] # 初始化棋盘
cells_c = [And(1 <= X[i][j], X[i][j] <= 9) for i in range(9) for j in range(9)] # 每个格子都是1-9
rows_c = [Distinct(X[i]) for i in range(9)] # 每行内的数字都不同
cols_c = [Distinct([X[i][j] for i in range(9)])for j in range(9)] # 每列内的数字都不同
sq_c = [ Distinct([X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3)] # 每个3x3的小9宫格的数字都不同
sudoku_c = cells_c + rows_c + cols_c + sq_c
instance = ((0,4,6,9,0,3,0,0,0),
(0,0,3,0,5,0,0,6,0),
(9,0,0,0,0,2,0,0,3),
(0,0,5,0,0,6,0,0,0),
(8,0,0,0,0,0,0,1,0),
(0,1,0,7,8,0,2,0,0),
(0,0,0,0,0,0,0,5,0),
(0,8,1,3,0,0,0,0,7),
(0,0,0,8,0,0,1,0,4)) # 待填入的数独,0为空
instance_c = [If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9)]
s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [[m[X[i][j]] for j in range(9) ]
for i in range(9)]
else:
print("failed to solve")

八皇后

1
2
3
4
5
6
7
8
Q = [Int('Q_%i' % (i + 1)) for i in range(8)] # 每个皇后所在的位置
val_c = [And(1 <= Q[i], Q[i] <= 8) for i in range(8)]
col_c = [Distinct(Q)]
diag_c = [If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i)]
solve(val_c + col_c + diag_c)

替换table表的base64解码

由于z3的BitVec直接操作比特位,故同样可以用来做base64解码

1
2
3
4
5
str1 = "x2dtJEOmyjacxDemx2eczT5cVS9fVUGvWTuZWjuexjRqy24rV29q"
table = StringVal("ZYXABCDEFGHIJKLMNOPQRSTUVWzyxabcdefghijklmnopqrstuvw0123456789+/")
s = reduce(Concat, [Int2BV(If(i == '=', 0, IndexOf(table, i, 0)), 6) for i in str1])
st = reversed([chr(simplify(Extract(8 * (i + 1) - 1, 8 * i, s)).as_long()) for i in range(s.size() // 8)])
print(''.join(st))

攻防世界IgniteMe

1
2
3
4
5
6
7
8
9
10
11
12
13
from z3 import *
flag = [BitVec('flag_%d' % i,8) for i in range(24)]
v8 = [If(And(i>=ord('a'),i<=ord('z')),i-32,If(And(i>=ord('A'),i<=ord('Z')),i+32,i)) for i in flag]
v8 = [(i ^ 0x55) + 72 for i in v8]
byte = [0x0D,0x13,0x17,0x11,0x02,0x01,0x20,0x1D,0x0C,0x02,0x19,0x2F,0x17,0x2B,0x24,0x1F,0x1E,0x16,0x09,0x0F,0x15,0x27,0x13,0x26]
result = 'GONDPHyGjPEKruv{{pj]X@rF'
s = Solver()
for i in range(24):
s.add(v8[i] ^ byte[i] == ord(result[i]))
assert s.check() == sat
m = s.model()
for i in flag:
print(chr(m[i].as_long()),end='')

攻防世界babymips

1
2
3
4
5
6
7
8
9
10
11
12
13
14
from z3 import *
flag = [BitVec('flag_%d' % i,8) for i in range(0x20)]
flag2 = [v ^ (0x20 - i) for i,v in enumerate(flag)]
s = Solver()
for i in zip(flag2[:5],[0x51,0x7c,0x6a,0x7b,0x67]):
s.add(i[0] == i[1])
cmpare = [0x52,0xFD,0x16,0xA4,0x89,0xBD,0x92,0x80,0x13,0x41,0x54,0xA0,0x8D,0x45,0x18,0x81,0xDE,0xFC,0x95,0xF0,0x16,0x79,0x1A,0x15,0x5B,0x75,0x1F]
flag2 = [If((i&1)==0,RotateRight(v,6),RotateRight(v,2)) for i,v in enumerate(flag2)]
for i in zip(flag2[5:],cmpare):
s.add(i[0] == i[1])
assert s.check() == sat
m = s.model()
for i in flag:
print(chr(m[i].as_long()),end='')

WMCTF2020 Wmware

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
import z3
import numpy as np
from functools import reduce

s = '1234567890_+qwertyuiop{}asdfghjklzxcvbnmQWERTYUIOPASDFGHJKLZXCVBNM'
sign = '02030405060708090a0b0c0d101112131415161718191a1b1e1f202122232425262c2d2e2f303132404142434445464748494e4f505152535455565c5d5e5f606162'
s2 = ['0x' + sign[2 * i:2 * i + 2] for i in range(len(s))]

table = {}
for i in zip(s, s2):
table[i[0]] = int(i[1], 16)


def process(s):
return '0x' + ''.join(reversed([s[2 * i: 2 * i + 2] for i in range(4)]))


result = 'd87455ecb5041a42116dba025f050581286ca0ed9904e06ae755a9189135d67164a83745'
results = [process(result[8 * i: 8 * i + 8]) for i in range(9)]

flag = [z3.BitVec('flag_%d' % i, 8) for i in range(36)]
flag2 = np.array([i + 0x55 for i in flag]).reshape(6, 6)
flag2 = flag2.T
flag2 = flag2.reshape(-1)
flag2 = [i for i in flag2]

flag3 = [reduce(z3.Concat, reversed(flag2[i * 4:i * 4 + 4])) for i in range(9)]
i = 0
v39 = 0
while True:
if i == 9:
i = 0
v39 += 1
if v39 == 129:
break
v41 = (i + 1) % 9
v44 = v39 % 3
if v44 == 0:
flag3[i] = ~((~ flag3[v41] | ~ flag3[i]) & (flag3[v41] | flag3[i]) & 0x24114514) & ~(
~((~ flag3[v41] | ~ flag3[i]) & (flag3[v41] | flag3[i])) & 0xDBEEBAEB)
elif v44 == 1:
flag3[i] = ~(~(flag3[v41] & flag3[i]) & ~(~ flag3[v41] & ~ flag3[i])) & 0x1919810 | ~(
flag3[v41] & flag3[i]) & ~(~ flag3[v41] & ~ flag3[i]) & 0xFE6E67EF
else:
flag3[i] = (~(flag3[v41] & ~ flag3[i] | ~ flag3[v41] & flag3[i]) | 0xE6D9F7E8) & (
flag3[v41] & ~ flag3[i] | ~ flag3[v41] & flag3[i] | 0x19260817)
i = i + 1
s = z3.Solver()
for i in zip(flag3, results):
s.add(i[0] == int(i[1], 16))
print(s.check())
m = s.model()
for i in flag:
t = m[i].as_long()
for item in table:
if t == table[item]:
print(item, end='')
文章目录
  1. 1. 数据类型
    1. 1.1. 数学类型
    2. 1.2. 有限类型
  2. 2.
    1. 2.1. 数学类型
      1. 2.1.1. Int
        1. 2.1.1.1. 成员函数
        2. 2.1.1.2. 运算
      2. 2.1.2. Real
        1. 2.1.2.1. 成员函数
        2. 2.1.2.2. 运算
      3. 2.1.3. Bool
        1. 2.1.3.1. 成员函数
        2. 2.1.3.2. 运算
    2. 2.2. 有限类型
      1. 2.2.1. BitVec
        1. 2.2.1.1. 成员函数
        2. 2.2.1.2. 运算
      2. 2.2.2. FP
        1. 2.2.2.1. 成员函数
        2. 2.2.2.2. 运算
      3. 2.2.3. String
        1. 2.2.3.1. 成员函数
        2. 2.2.3.2. 运算
  3. 3. 求解(不定时更新)
    1. 3.1. 数独
    2. 3.2. 八皇后
    3. 3.3. 替换table表的base64解码
    4. 3.4. 攻防世界IgniteMe
    5. 3.5. 攻防世界babymips
    6. 3.6. WMCTF2020 Wmware