Mas0n
mailto:MasonShi@88.com
翻车鱼

从CTF入门z3 solver

z3 是微软开发的的高性能约束求解工具。

https://cdn.shi1011.cn/2021/11/72181184d756844504c4ee515e7a230b.png?imageMogr2/format/webp/interlace/0/quality/90|watermark/2/text/wqlNYXMwbg/font/bXN5aGJkLnR0Zg/fontsize/14/fill/IzMzMzMzMw/dissolve/80/gravity/southeast/dx/5/dy/5

z3 也是 angr 和 triton 底层的约束求解器。其强大的数学求解能力在CTF解题中被广泛使用,

本文记录/摘录一些常用的z3 Python API,以期能较为充分的运用z3的强大能力。

数据类型

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

数学类型

函数名说明
Int定义一个整数符号x = Int('x')
Ints定义几个整数 符号 x, y = Ints('x y')
IntVector以$1为前缀定义,定义$2个Intx = IntVector('x', 12)
IntVal定义值为$1的一个Int,$1可以是string或整数a = IntVal(1); b=IntVal('123')
Real定义一个实数x = Real('x')
Reals同Intsx = Reals('x y')
RealVector同IntVectorx = RealVector('x', 12)
RealVal同IntValx = RealVal('2.718')
Q定义一个有理分数$1/$2x = Q(5, 8)
RatVal与Q一样,定义一个有理分数$1 / $2,实际Q是调用的RatValx = RatVal(5, 8)
Bool定义一个布尔类型p = Bool('p')
Bools同Intsp, q, r = Bools('p q r')
BoolVector同IntVectorP = BoolVector('p', 5)
BoolVal同IntValBoolVal(True)

有限类型

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

数学类型

Int

成员函数

函数名返回类型说明
as_longpython int把z3的Int转换成python的intIntVal(888).as_long()
as_stringpython string把z3的Int转换成python的stringIntVal(888).as_string()

运算

函数名返回类型说明
__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')
ToRealReal转换成Real类型ToReal(Int('x'))
Int2BVBitVec把1 转换成长2 bit的BitVecInt2BV(Int('x'), 32)

Real

成员函数

函数名返回类型说明
numeratorInt返回该数分数形式的分子Q(3,5).numerator()
numerator_as_longpython int返回该数分数形式的分子Q(3,5).numerator()
denominatorInt返回该数分数形式的分母RealVal(12.25).denominator()
denominator_as_longpython int返回该数分数形式的分母RealVal("1/77").denominator_as_long()
as_fractionpython Fraction得到该数的python Fraction对象RealVal("1/12").as_fraction()
as_decimalpython string得到该数的小数形式并保留$1位小数RealVal("1/33").as_decimal(3)
as_longpython int得到该数的python整数形式,如果该数不为整数则抛异常同Int
as_stringpyhton string同Int同Int

运算

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

Bool

成员函数

运算

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

有限类型

BitVec

成员函数

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

运算

函数名返回类型说明
BV2IntInt$1 转换成Int,布尔值$2输入是否有符号BV2Int(BitVec('a', 8), is_signed=True)
ConcatBitVec BitVec 类型参数拼接Concat(BitVec('a', 8),BitVec('b', 8))
ExtractBitVec取$3[$2: $1]得到新的 BitVec Extract(6, 2, BitVec('a', 8))
RotateLeftBitVec$1 循环左移 $2位RotateLeft(BitVec('a', 8),2)
RotateRightBitVec$1 循环右移 $2位RotateRight(BitVec('a', 8),2)
RepeatBitVecBitVec重复$2,$1 次RepeatBitVec(2, a)RepeatBitVec(2, BitVec('a', 8))
SignExtBitVec向$2前缀填充$1 位1SignExt(8, BitVec('a', 32))
ZeroExtBitVec向$2前缀填充$1 位0ZeroExt(8, BitVec('b', 32))

有符号与无符号运算表

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

FP

成员函数

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

运算

z3中定义了5种IEEE舍入规则:

  • RoundNearestTiesToEven
  • RoundNearestTiesToAway
  • RoundTowardPositive
  • RoundTowardNegative
  • RoundTowardZero
Function Alias Description
RoundNearestTiesToEvenRNE向偶数舍入
RoundNearestTiesToAwayRNA最近 舍入
RoundTowardPositiveRTP向+∞ 舍入
RoundTowardNegativeRTN向-∞ 舍入
RoundTowardZeroRTZ向0 舍入

C语言默认为RNE

FunctionReturn TypesDescriptionExample
fpNaNFP返回 一个值为NaN的FPfpNaN(FPSort(8, 24))
fpPlusInfinitFP返回 一个值为+∞的FPfpPlusInfinity(FPSort(8, 24))
fpMinusInfinityFP返回 一个值为-∞的FPfpMinusInfinity(FPSort(8, 24))
fpInfinityFP返回 一个值为+∞ 或 -∞的FPfpInfinity(FPSort(8, 24), False)
fpPlusZeroFP返回一个值为+0.0的FPfpPlusZero(FPSort(8, 24))
fpMinusZeroFP返回 一个值为-0.0的FPfpMinusZero(FPSort(8, 24))
fpZeroFP返回 一个值为+0.0 或 -0.0的FPfpZero(FPSort(8, 24), False)
fpAbsFP取绝对值fpAbs(x)
fpNegFP取相反数fpAbs(Neg)
fpAddFP按照$1舍入规则$2 + $3fpAdd(RNE(), x, y)
fpSubFP按照$1舍入规则$2 – $3fpSub(RNE(), x, y)
fpMulFP按照$1舍入规则$2 * $3fpMul(RNE(), x, y)
fpDivFP按照$1舍入规则$2 / $3fpDiv(RNE(), x, y)
fpRemFP按照$1舍入规则$2 % $3fpRem(RNE(), x, y)
fpMinFP返回$1与$2中最小的FPfpMin(x, y)
fpMaxFP 返回$1与$2最大的FPfpMax(x, y)
fpFMAFP按照$1舍入规则$2 * 3 + $4fpFMA(RNE(), x, y, z)
fpSqrtFP按照$1 舍入规则对$1开方fpSqrt(RNE(), x)
fpRoundToIntegralInt按照$1舍入规则对$2取整fpRoundToIntegral(RNE(), a)
fpIsNaNBool判断$1是否为NaNfpIsNaN(x)
fpIsInfBool判断$1是否为InffpIsInf(x)
fpIsZeroBool判断$1是否为0fpIsZero(x)
fpIsNormalBool当fpIsNaN、fpIsInf、fpIsZero都不成立时为TruefpIsNormal(x)
fpIsNegativeBool判断$1是否为负值fpIsNegative(x)
fpIsPositiveBool判断$1是否为正值fpIsPositive(x)
fpLTBool$1 < $2fpLT(a,b)
fpLEQBool$1 <= $2fpLEQ(a,b)
fpGTBool$1 > $2fpGT(a,b)
fpGEQBool$1 >= $2fpGEQ(a,b)
fpEQBool$1 == $2fpEQ(a,b)
fpNEQBool$1 != $2fpNEQ(a,b)
fpBVToFPFP按照IEEE编码把$1转换成$2类型的浮点数fpBVToFP(BitVecVal(0x41440000, 32), Float32())
fpSignedToFPFP按照$1 舍入规则把$2转换成$3 类型fpSignedToFP(RNE(), BitVecVal(-5, 32), Float32())
fpUnsignedToFPFP按照$1 舍入规则把$2转换成$3 类型fpUnsignedToFP(RNE(), BitVecVal(-5, 32), Float32())
fpFPToFPFP按照$1 舍入规则把$2转换成$3 类型fpFPToFP(RNE(), FPVal(1.0, Float32()), Float64())
fpRealToFPFP按照$1 舍入规则把$2转换成$3 类型fpRealToFP(RNE(), RealVal(1.5), Float32())
fpToIEEEBVBitVec按照IEEE编码把$1转换成BitVec类型fpToIEEEBV(FP('x', FPSort(8, 24)))
fpToSBVBitVec按照$1舍入规则把$2转换成有符号BitVec类型fpToSBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))
fpToUBVBitVec按照$1舍入规则把$2转换成无符号BitVec类型fpToUBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))
fpToRealReal把$1转换成Real类型fpToReal(x)

String

成员函数

函数名返回类型说明
atString返回第$1个位置的值StringVal('who am i').at(2)
__add__String拼接String('a') + String('b')

运算

函数名返回类型说明
SubSeqString从$2位置开始在$1中取出长度为$3的字串SubSeq(s,0,4)
PrefixOfBool判断$1是否是$2的前缀PrefixOf("ab", "abc")
SuffixOfBool判断$1是否是$2的后缀SuffixOf("bc", "abc")
ContainsBool判断$1是否包含$2Contains("abc", "bc")
ReplaceString把$1 中的第一个$2 字符替换成$3Replace("aaa", "a", "b")
IndexOfInt从$3位置开始在$1中搜索$2,$3默认为0IndexOf("abcabc", "bc", 2)
LastIndexOfInt在$1中检索最后出现$2的位置LastIndexOf("abcdc","dc")
LengthInt取长度Length(StringVal('aaa'))
StrToIntIntString转IntStrToInt("1")
IntToStrStringInt转StringIntToStr(IntVal(31))

求解

一般情况下,用Solver创建一个求解器,利用成员函数add添加约束,最后使用成员函数check进行求解,成员函数model()得到求解结果。 例如:

a, b = Reals('a b')
sol = Solver()
sol.add(a + b == 128)
sol.add(a - b == 64)
assert sol.check() == sat
rol = sol.model()
print(f"a = {rol[a]}")
print(f"b = {rol[b]}")

还有一个函数solve则是直接在参数中添加约束。

例如:

a = Int('a')
solve(a > 0, a < 2)

z3 解Base64

from z3 import *
from functools import reduce

enc = "kcGXlcG9ihRqlYy5"
maps = StringVal("3GHIJKLMNOPQRSTUb=cdefghijklmnopWXYZ/12+406789VaqrstuvwxyzABCDEF5")
sol = reduce(Concat, [Int2BV(If(i == '=', 0, IndexOf(maps, i, 0)), 6) for i in enc])
arr = reversed([chr(simplify(Extract(i + 7, i, sol)).as_long()) for i in range(0, sol.size(), 8)])
print("".join(arr))

参考

Z3: z3py Namespace Reference

Z3Py Guide

Z3求解约束器及例题 -SYJ

本文链接:https://blog.shi1011.cn/learn/1789
本文采用 CC BY-NC-SA 3.0 Unported 协议进行许可

Mas0n

文章作者

发表评论

textsms
account_circle
email

翻车鱼

从CTF入门z3 solver
z3 是微软开发的的高性能约束求解工具。 z3 也是 angr 和 triton 底层的约束求解器。其强大的数学求解能力在CTF解题中被广泛使用, 本文记录/摘录一些常用的z3 Python API,以…
扫描二维码继续阅读
2021-11-03