pythonz3学习

本文最后更新于：2023年10月8日上午

一件梭哈✌️工具学习

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

System Diagram

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

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

数据类型

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

数学类型

函数名	说明	例
Int	定义一个整数符号	`x = Int('x')`
Ints	定义几个整数符号	`x, y = Ints('x y')`
IntVector	以$1为前缀定义，定义$2个Int	`x = IntVector('x', 12)`
IntVal	定义值为$1的一个Int，$1可以是string或整数	`a = IntVal(1); b=IntVal('123')`
Real	定义一个实数	`x = Real('x')`
Reals	同Ints	`x = Reals('x y')`
RealVector	同IntVector	`x = RealVector('x', 12)`
RealVal	同IntVal	`x = RealVal('2.718')`
Q	定义一个有理分数$1/$2	`x = Q(5, 8)`
RatVal	与Q一样，定义一个有理分数$1 / $2，实际Q是调用的RatVal	`x = RatVal(5, 8)`
Bool	定义一个布尔类型	`p = Bool('p')`
Bools	同Ints	`p, q, r = Bools('p q r')`
BoolVector	同IntVector	`P = BoolVector('p', 5)`
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(122, 8)`
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的浮点数	`f = FPVal(11.11, FPSort(8, 24))`
String	定义一个名为$1 的字符串	`a = String('a')`
Strings	同`Ints`	`a, b, c = Strings('a b c')`
StringVal	定义一个值为$1 的字符串	`a = StringVal('a')`

类

数学类型

Int

成员函数

函数名	返回类型	说明	例
as_long	python int	把z3的Int转换成python的int	`IntVal(888).as_long()`
as_string	python string	把z3的Int转换成python的string	`IntVal(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')`
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/77").denominator_as_long()`
as_fraction	python Fraction	得到该数的python Fraction对象	`RealVal("1/12").as_fraction()`
as_decimal	python string	得到该数的小数形式并保留$1位小数	`RealVal("1/33").as_decimal(3)`
as_long	python int	得到该数的python整数形式，如果该数不为整数则抛异常	同Int
as_string	pyhton string	同Int	同Int

运算

函数名	返回类型	说明	例
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()`

运算

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

有符号与无符号运算表

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

FP

成员函数

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

运算

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

RoundNearestTiesToEven
RoundNearestTiesToAway
RoundTowardPositive
RoundTowardNegative
RoundTowardZero

Function	Alias	Description
RoundNearestTiesToEven	RNE	向偶数舍入
RoundNearestTiesToAway	RNA	最近舍入
RoundTowardPositive	RTP	向+∞ 舍入
RoundTowardNegative	RTN	向-∞ 舍入
RoundTowardZero	RTZ	向0 舍入

C语言默认为RNE

Function	Return Types	Description	Example
fpNaN	FP	返回一个值为NaN的FP	`fpNaN(FPSort(8, 24))`
fpPlusInfinit	FP	返回一个值为+∞的FP	`fpPlusInfinity(FPSort(8, 24))`
fpMinusInfinity	FP	返回一个值为-∞的FP	`fpMinusInfinity(FPSort(8, 24))`
fpInfinity	FP	返回一个值为+∞ 或 -∞的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	按照$1舍入规则$2 + $3	`fpAdd(RNE(), x, y)`
fpSub	FP	按照$1舍入规则$2 – $3	`fpSub(RNE(), x, y)`
fpMul	FP	按照$1舍入规则$2 * $3	`fpMul(RNE(), x, y)`
fpDiv	FP	按照$1舍入规则$2 / $3	`fpDiv(RNE(), x, y)`
fpRem	FP	按照$1舍入规则$2 % $3	`fpRem(RNE(), x, y)`
fpMin	FP	返回$1与$2中最小的FP	`fpMin(x, y)`
fpMax	FP	返回$1与$2最大的FP	`fpMax(x, y)`
fpFMA	FP	按照$1舍入规则$2 * 3 + $4	`fpFMA(RNE(), x, y, z)`
fpSqrt	FP	按照$1 舍入规则对$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	按照IEEE编码把$1转换成$2类型的浮点数	`fpBVToFP(BitVecVal(0x41440000, 32), Float32())`
fpSignedToFP	FP	按照$1 舍入规则把$2转换成$3 类型	`fpSignedToFP(RNE(), BitVecVal(-5, 32), Float32())`
fpUnsignedToFP	FP	按照$1 舍入规则把$2转换成$3 类型	`fpUnsignedToFP(RNE(), BitVecVal(-5, 32), Float32())`
fpFPToFP	FP	按照$1 舍入规则把$2转换成$3 类型	`fpFPToFP(RNE(), FPVal(1.0, Float32()), Float64())`
fpRealToFP	FP	按照$1 舍入规则把$2转换成$3 类型	`fpRealToFP(RNE(), RealVal(1.5), Float32())`
fpToIEEEBV	BitVec	按照IEEE编码把$1转换成BitVec类型	`fpToIEEEBV(FP('x', FPSort(8, 24)))`
fpToSBV	BitVec	按照$1舍入规则把$2转换成有符号BitVec类型	`fpToSBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))`
fpToUBV	BitVec	按照$1舍入规则把$2转换成无符号BitVec类型	`fpToUBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))`
fpToReal	Real	把$1转换成Real类型	`fpToReal(x)`

String

成员函数

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

运算

函数名	返回类型	说明	例
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"， 2)`
LastIndexOf	Int	在$1中检索最后出现$2的位置	`LastIndexOf("abcdc","dc")`
Length	Int	取长度	`Length(StringVal('aaa'))`
StrToInt	Int	String转Int	`StrToInt("1")`
IntToStr	String	Int转String	`IntToStr(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则是直接在参数中添加约束。

例如：

1 2	`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))

例子1（原2023iscc线下re）

from z3 import *

arr3 = [x ^ 18 for x in [123, 148, 62, 53, 24, 116, 244, 126, 63, 90]]

s = Solver()
flag_value = [BitVec(("%d" % i), 8) for i in range(10)]  # 创建长度为10的BitVec列表，每个元素都是8位
for i in range(10):
    s.add((((flag_value[i] & 7) << 5) | ((flag_value[i] >> 3) & 255)) == arr3[i])

flag = ""
if s.check() == sat:  # 判断约束是否可满足
    model = s.model()  # 获取可满足模型
    sorted_keys = sorted(model, key=lambda x: int(x.name()))  # 按变量名称进行排序
    for key in sorted_keys:
        value = model[key].as_long()  # 将变量的值转换为长整型
        flag += chr(value)  # 将长整型转换为字符并添加到标志字符串中
        char = chr(value)
        print(f"{key} = {char}")  # 打印变量名及对应的字符值
else:
    print("No solution")  # 若无解，则打印无解提示

print("\n[+]-->\t\t" + flag, end="")

例子2（第十三届全国大学生网络安全预选赛的一道逆向题)

**re附件**（提取码：v02b）

转十进制，解五组方程组（仅举一个例子

from z3 import *
s = Solver()

v5,v6,v7,v8,v9,v10,v11,v12,v13      = Ints("5 6 7 8 9 10 11 12 13")
v14,v15,v16,v17,v18,v19,v20,v21,v22 = Ints("14 15 16 17 18 19 20 21 22")
v23,v24,v25,v26,v27,v28,v29,v30,v31 = Ints("23 24 25 26 27 28 29 30 31")
v32,v33,v34,v35,v36,v37,v38,v39,v40 = Ints("32 33 34 35 36 37 38 39 40")
v41,v42,v43,v44,v45,v46             = Ints("41 42 43 44 45 46")

s.add(0x4F17 == 34 * v8 + 12 * v5 + 53 * v6 + 6 * v7 + 58 * v9 + 36 * v10 + v11)
s.add(0x9CF6 == 27 * v9 + 73 * v8 + 12 * v7 + 83 * v5 + 85 * v6 + 96 * v10 + 52 * v11)
s.add(0x8DDB == 24 * v7 + 78 * v5 + 53 * v6 + 36 * v8 + 86 * v9 + 25 * v10 + 46 * v11)
s.add(0x8EA6 == 78 * v6 + 39 * v5 + 52 * v7 + 9 * v8 + 62 * v9 + 37 * v10 + 84 * v11)
s.add(0x6929 == 48 * v9 + 14 * v7 + 23 * v5 + 6 * v6 + 74 * v8 + 12 * v10 + 83 * v11)
s.add(0x9911 == 15 * v10 + 48 * v9 + 92 * v7 + 85 * v6 + 27 * v5 + 42 * v8 + 72 * v11)
s.add(0x40A2 == 26 * v10 + 67 * v8 + 6 * v6 + 4 * v5 + 3 * v7 + 68 * v11)
s.add(0x2F3E == 34 * v15 + 12 * v12 + 53 * v13 + 6 * v14 + 58 * v16 + 36 * v17 + v18)
s.add(0x62B6 == 27 * v16 + 73 * v15 + 12 * v14 + 83 * v12 + 85 * v13 + 96 * v17 + 52 * v18)
s.add(0x4B82 == 24 * v14 + 78 * v12 + 53 * v13 + 36 * v15 + 86 * v16 + 25 * v17 + 46 * v18)
s.add(0x486C == 78 * v13 + 39 * v12 + 52 * v14 + 9 * v15 + 62 * v16 + 37 * v17 + 84 * v18)
s.add(0x4002 == 48 * v16 + 14 * v14 + 23 * v12 + 6 * v13 + 74 * v15 + 12 * v17 + 83 * v18)
s.add(0x52D7 == 15 * v17 + 48 * v16 + 92 * v14 + 85 * v13 + 27 * v12 + 42 * v15 + 72 * v18)
s.add(0x2DEF == 26 * v17 + 67 * v15 + 6 * v13 + 4 * v12 + 3 * v14 + 68 * v18)
s.add(0x28DC == 34 * v22 + 12 * v19 + 53 * v20 + 6 * v21 + 58 * v23 + 36 * v24 + v25)
s.add(0x640D == 27 * v23 + 73 * v22 + 12 * v21 + 83 * v19 + 85 * v20 + 96 * v24 + 52 * v25)
s.add(0x528F == 24 * v21 + 78 * v19 + 53 * v20 + 36 * v22 + 86 * v23 + 25 * v24 + 46 * v25)
s.add(0x613B == 78 * v20 + 39 * v19 + 52 * v21 + 9 * v22 + 62 * v23 + 37 * v24 + 84 * v25)
s.add(0x4781 == 48 * v23 + 14 * v21 + 23 * v19 + 6 * v20 + 74 * v22 + 12 * v24 + 83 * v25)
s.add(0x6B17 == 15 * v24 + 48 * v23 + 92 * v21 + 85 * v20 + 27 * v19 + 42 * v22 + 72 * v25)
s.add(0x3237 == 26 * v24 + 67 * v22 + 6 * v20 + 4 * v19 + 3 * v21 + 68 * v25)
s.add(0x2A93 == 34 * v29 + 12 * v26 + 53 * v27 + 6 * v28 + 58 * v30 + 36 * v31 + v32)
s.add(0x615F == 27 * v30 + 73 * v29 + 12 * v28 + 83 * v26 + 85 * v27 + 96 * v31 + 52 * v32)
s.add(0x50BE == 24 * v28 + 78 * v26 + 53 * v27 + 36 * v29 + 86 * v30 + 25 * v31 + 46 * v32)
s.add(0x598E == 78 * v27 + 39 * v26 + 52 * v28 + 9 * v29 + 62 * v30 + 37 * v31 + 84 * v32)
s.add(0x4656 == 48 * v30 + 14 * v28 + 23 * v26 + 6 * v27 + 74 * v29 + 12 * v31 + 83 * v32)
s.add(0x5B31 == 15 * v31 + 48 * v30 + 92 * v28 + 85 * v27 + 27 * v26 + 42 * v29 + 72 * v32)
s.add(0x313A == 26 * v31 + 67 * v29 + 6 * v27 + 4 * v26 + 3 * v28 + 68 * v32)
s.add(0x3010 == 34 * v36 + 12 * v33 + 53 * v34 + 6 * v35 + 58 * v37 + 36 * v38 + v39)
s.add(0x67FE == 27 * v37 + 73 * v36 + 12 * v35 + 83 * v33 + 85 * v34 + 96 * v38 + 52 * v39)
s.add(0x4D5F == 24 * v35 + 78 * v33 + 53 * v34 + 36 * v36 + 86 * v37 + 25 * v38 + 46 * v39)
s.add(0x58DB == 78 * v34 + 39 * v33 + 52 * v35 + 9 * v36 + 62 * v37 + 37 * v38 + 84 * v39)
s.add(0x3799 == 48 * v37 + 14 * v35 + 23 * v33 + 6 * v34 + 74 * v36 + 12 * v38 + 83 * v39)
s.add(0x60A0 == 15 * v38 + 48 * v37 + 92 * v35 + 85 * v34 + 27 * v33 + 42 * v36 + 72 * v39)
s.add(0x2750 == 26 * v38 + 67 * v36 + 6 * v34 + 4 * v33 + 3 * v35 + 68 * v39)
s.add(0x3759 == 34 * v43 + 12 * v40 + 53 * v41 + 6 * v42 + 58 * v44 + 36 * v45 + v46)
s.add(0x8953 == 27 * v44 + 73 * v43 + 12 * v42 + 83 * v40 + 85 * v41 + 96 * v45 + 52 * v46)
s.add(0x7122 == 24 * v42 + 78 * v40 + 53 * v41 + 36 * v43 + 86 * v44 + 25 * v45 + 46 * v46)
s.add(0x81F9 == 78 * v41 + 39 * v40 + 52 * v42 + 9 * v43 + 62 * v44 + 37 * v45 + 84 * v46)
s.add(0x5524 == 48 * v44 + 14 * v42 + 23 * v40 + 6 * v41 + 74 * v43 + 12 * v45 + 83 * v46)
s.add(0x8971 == 15 * v45 + 48 * v44 + 92 * v42 + 85 * v41 + 27 * v40 + 42 * v43 + 72 * v46)
s.add(0x3A1D == 26 * v45 + 67 * v43 + 6 * v41 + 4 * v40 + 3 * v42 + 68 * v46)


flag = ""
if s.check() == sat:  # 判断约束是否可满足
    model = s.model()  # 获取可满足模型
    sorted_keys = sorted(model, key=lambda x: int(x.name()))  # 按变量名称进行排序
    for key in sorted_keys:
        value = model[key].as_long()  # 将变量的值转换为长整型
        flag += chr(value)  # 将长整型转换为字符并添加到标志字符串中
        char = chr(value)
        print(f"{key} = {char}")  # 打印变量名及对应的字符值
    print("\n[+]-->\t\t" + flag, end="")
else:
    print("No solution")  # 若无解，则打印无解提示

#flag{7e171d43-63b9-4e18-990e-6e14c2afe648}

例题3（[GUET-CTF2019]re）

题目链接：[GUET-CTF2019]re
题目下载：点击下载

from z3 import *
s = Solver()
a1 = [BitVec(("%d" % i), 32) for i in range(32)]  
# 创建长度为10的BitVec列表，每个元素都是8位
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( 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)
    flag = ""
    if s.check() == sat:  # 判断约束是否可满足
        model = s.model()  # 获取可满足模型
        sorted_keys = sorted(model, key=lambda x: int(x.name()))  # 按变量名称进行排序
        for key in sorted_keys:
            value = model[key].as_long()  # 将变量的值转换为长整型
            flag += chr(value)  # 将长整型转换为字符并添加到标志字符串中
            char = chr(value)
            print(f"{key} = {char}")  # 打印变量名及对应的字符值
    else:
        print("No solution")  # 若无解，则打印无解提示

    print("\n[+]-->\t\t" + flag, end="")

参考从CTF入门z3 solver - 翻车鱼 (shi1011.cn)
拿2020 CISCN - Mssn Harvey - CTFer && DreamRedteam附件
参考https://blog.csdn.net/Palmer9/article/details/104210881

#re #逆向 #python-z3-solver #z3 #一件梭哈✌️工具

pythonz3学习

https://huajien.gitee.io/2023/30bc1fee/

作者

HUAJI

发布于

2023年10月8日

许可协议

记录adb和jeb动态调试实体机设备上一篇

python_angr_模板下一篇