本文首发于“合天智汇”公众号 作者：Skye
介绍
Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。
官方使用文档：https://rise4fun.com/z3/tutorialcontent/guide z3py 功能手册：https://z3prover.github.io/api/html/namespacez3py.html z3py 使用文档：https://ericpony.github.io/z3py-tutorial/guide-examples.htm z3 所使用的语法标准：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
安装
这里安装的是 python 库版本，编译好的二进制版本在 Github 下载。
pip install z3-solver
简单使用
from z3 import * x = Int('x') #设置整型变量x y = Int('y') #设置整型变量y solve(x > 2, y < 10, x + 2*y == 7) #写入方程 # [y = 0, x = 7]
进阶使用
设置变量
批量设置变量见补充
Int - 整数型
# 声明单个变量 x = Int('x') # 声明多个变量 y,z = Ints('y z')
- | 运算需要初始化为Int变量
Real - 实数型
# 声明单个变量 x = Real('x') # 声明多个变量 y,z = Reals('y z')
BitVec - 向量（位运算）
# 声明单个 16 位的变量 x = BitVec('x',16) # 声明多个 16 位的变量 y,z = BitVecs('y z',16)
- 只有 BitVec 变量可以进行异或
python solver.add(BitVec('x',8)^BitVec('y',8)==5)
- BitVec 变量值之间可进行>或<或=或>=或<=的比较
BitVec('a',8)>=BitVec('b',8) BitVec('a',8)<=BitVec('b',8) BitVec('a',8)<=9 BitVec('a',8)==9
- BitVecVal 值之间不能进行>或<比较,只能转换成 python 认识的类型才可以比较
if BitVecVal(98,8)>BitVecVal(97,8)#错误，不是python类型 if BitVecVal(98,8)==98: if BitVecVal(98,8).as_long()>97 if BitVecVal(98,8).as_long()>BitVecVal(97,8).as_long()
变量设置的类型可能会影响到最后求解的结果。可以先 check 一下看看有没有解，然后再判断是否需要切换变量的类型。
Solver 对象
实际做题时，约束条件肯定不会想上面例子这么少，所以需要实例化一个 Solver() 对象，方便我们添加更多的约束条件。
创建约束求解器：
solver = Solver()
添加约束条件
一行一个约束条件，这里的约束条件就是方程等式：
solver.add(x**2+y**2==74) solver.add(x**5-y==z) # [y = -7, x = 5, z = 3132]
z3 中不允许列表与列表之间添加==约束条件：
from z3 import * prefix=[ord(each) for each in "flag{"] plain_line=[Int('x%d' % i) for i in range(5)] s=Solver() z=0 #s.add(plain_line[z:z+5]==prefix) 列表==列表-->错误 s.add(plain_line[z]==prefix[0]) s.add(plain_line[z+1]==prefix[1]) s.add(plain_line[z+2]==prefix[2]) s.add(plain_line[z+3]==prefix[3]) s.add(plain_line[z+4]==prefix[4]) s.check() print(s.model())
判断是否有解
if solver.check() == sat: print("solver") else: print("no solver")
求解并输出
ans = solver.model()
print(ans)
补充
限制结果为可见字符
通常如果是做题的话，解密出来很可能是 flag ，也就是 ascii 码，所以为了进一步约束范围可以给每一个变量都加上额外的一条约束，约束其结果只能在可见 ascii 码范围以内：
solver.add(x < 127) solver.add(x >= 32)
快速添加变量
添加 50 个 Int 变量 s ：
s=[Int('s%d' % i) for i in range(50)]
添加 50 个 Real 变量 s ：
s=[Real('s%d' % i) for i in range(50)]
添加 50 个 16 位 BitVec 变量 s ：
s=[BitVec ('s%d' % i,16) for i in range(50)]
在约束条件中用下标索引使用：
solver.add(s[18] * s[8] == 5) solver.add(s[4] * s[11] == 0)
将结果按顺序打印出来：
这是使用列表管理变量的好处，如果不使用列表 print(answer) 输出的结果是无序的。
answer=solver.model() #print(answer) result="".join([str(answer[each]) for each in s]) print(result)
练习例题
2020 羊城杯 login
题目前面还有一步逆向 pyinstaller 打包的 exe 文件，这里不赘述直接给出源码：
import sys input1 = input('input something:') if len(input1) != 14: print('Wrong length!') sys.exit() code = [] for i in range(13): code.append(ord(input1[i]) ^ ord(input1[i + 1])) code.append(ord(input1[13])) a1 = code[2] a2 = code[1] a3 = code[0] a4 = code[3] a5 = code[4] a6 = code[5] a7 = code[6] a8 = code[7] a9 = code[9] a10 = code[8] a11 = code[10] a12 = code[11] a13 = code[12] a14 = code[13] if ((((a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5) + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36) + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60) + a14 * 29 == 22748) & ((((a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25) + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66) + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39) + a14 * 17 == 7258) & ((((a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65) + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33) + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34) + a14 * 23 == 26190) & ((((a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59) + a5 * 49 + a6 * 81 + a7 * 25 + (a8 << 7) - a9 * 32) + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60) + a14 * 29 == 37136) & (((a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52) + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36) + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915) & ((((a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45) + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26) + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61) + a14 * 28 == 17298) & ((((a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42) + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47) + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44) + a14 * 65 == 19875) & (((a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85) + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30) + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784) & ((((a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85) + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36) + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64) + a14 * 27 == 9710) & (((((a1 * 67 - a2 * 68) + a3 * 68 - a4 * 51 - a5 * 43) + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38) + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52) + a14 * 31 == 13376) & ((((a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51) + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6) + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67) + a14 * 78 == 24065) & ((((a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5) + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35) + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61) + a14 * 20 == 27687) & (((a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25) + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92) + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250) & (((a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43) + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36) + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317): print('flag is GWHT{md5(your_input)}') print('Congratulations and have fun!') else: print('Sorry,plz try again...') import sys input1 = input('input something:') if len(input1) != 14: print('Wrong length!') sys.exit() code = [] for i in range(13): code.append(ord(input1[i]) ^ ord(input1[i + 1])) code.append(ord(input1[13])) a1 = code[2] a2 = code[1] a3 = code[0] a4 = code[3] a5 = code[4] a6 = code[5] a7 = code[6] a8 = code[7] a9 = code[9] a10 = code[8] a11 = code[10] a12 = code[11] a13 = code[12] a14 = code[13] if ((((a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5) + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36) + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60) + a14 * 29 == 22748) & ((((a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25) + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66) + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39) + a14 * 17 == 7258) & ((((a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65) + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33) + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34) + a14 * 23 == 26190) & ((((a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59) + a5 * 49 + a6 * 81 + a7 * 25 + (a8 << 7) - a9 * 32) + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60) + a14 * 29 == 37136) & (((a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52) + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36) + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915) & ((((a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45) + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26) + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61) + a14 * 28 == 17298) & ((((a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42) + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47) + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44) + a14 * 65 == 19875) & (((a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85) + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30) + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784) & ((((a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85) + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36) + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64) + a14 * 27 == 9710) & (((((a1 * 67 - a2 * 68) + a3 * 68 - a4 * 51 - a5 * 43) + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38) + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52) + a14 * 31 == 13376) & ((((a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51) + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6) + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67) + a14 * 78 == 24065) & ((((a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5) + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35) + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61) + a14 * 20 == 27687) & (((a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25) + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92) + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250) & (((a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43) + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36) + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317): print('flag is GWHT{md5(your_input)}') print('Congratulations and have fun!') else: print('Sorry,plz try again...')
分析之后确定需要先求解出 a1~a14 的值，然后再经过一次异或获得 flag 。
这里我们手动添加多个变量，因为源码中的方式形式为 ax 。如果我们用列表管理变量，方程需要手动修改，消耗更多时间得不偿失。z3 脚本：
from z3 import * a1 = Int('a1') a2 = Int('a2') a3 = Int('a3') a4 = Int('a4') a5 = Int('a5') a6 = Int('a6') a7 = Int('a7') a8 = Int('a8') a9 = Int('a9') a10 = Int('a10') a11 = Int('a11') a12 = Int('a12') a13 = Int('a13') a14 = Int('a14') solver = Solver() solver.add((((a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5) + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36) + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60) + a14 * 29 == 22748) solver.add((((a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25) + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66) + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39) + a14 * 17 == 7258) solver.add((((a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65) + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33) + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34) + a14 * 23 == 26190) # solver.add((((a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59) + a5 * 49 + a6 * 81 + a7 * 25 + (a8 << 7) - a9 * 32) + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60) + a14 * 29 == 37136) solver.add(((a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52) + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36) + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915) solver.add((((a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45) + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26) + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61) + a14 * 28 == 17298) solver.add((((a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42) + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47) + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44) + a14 * 65 == 19875) solver.add(((a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85) + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30) + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784) solver.add((((a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85) + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36) + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64) + a14 * 27 == 9710) solver.add(((((a1 * 67 - a2 * 68) + a3 * 68 - a4 * 51 - a5 * 43) + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38) + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52) + a14 * 31 == 13376) solver.add((((a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51) + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6) + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67) + a14 * 78 == 24065) solver.add((((a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5) + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35) + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61) + a14 * 20 == 27687) solver.add(((a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25) + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92) + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250) solver.add(((a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43) + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36) + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317) solver.add(a1 >= 0) solver.add(a2 >= 0) solver.add(a3 >= 0) solver.add(a4 >= 0) solver.add(a5 >= 0) solver.add(a6 >= 0) solver.add(a7 >= 0) solver.add(a8 >= 0) solver.add(a9 >= 0) solver.add(a10 >= 0) solver.add(a11 >= 0) solver.add(a12 >= 0) solver.add(a13 >= 0) solver.add(a14 >= 0) if solver.check() == sat: print("solver") ans = solver.model() print(ans) else: print("no")
这里我们需要将有移位运算的那一条方程注释掉，因为 Int 没有这种运算方法。然后我们知道 a1~a14 是两两整数异或而来，所以加上约束大于等于 0 ，否则由于缺少一条方程解出来的值含有负数。
如果不想注释那条方程，完全使用全部方程，那么就将变量定义为：BitVec('an', 16) ，那么就能够使用移位运算。
然后就是还原异或加密：
a1 = 119 a2 = 24 a3 = 10 a4 = 7 a5 = 104 a6 = 43 a7 = 28 a8 = 91 a9 = 52 a10 = 108 a11 = 88 a12 = 74 a13 = 88#121 a14 = 33 code = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13] code[0] = a3 code[1] = a2 code[2] = a1 code[3] = a4 code[4] = a5 code[5] = a6 code[6] = a7 code[7] = a8 code[9] = a9 code[8] = a10 code[10] = a11 code[11] = a12 code[12] = a13 code[13] = a14 flag = [] flag.append(chr(code[13])) for i in list(range(13))[::-1]: code[i] = (code[i] ^ code[i + 1]) for i in code: print(chr(i),end='') #flag:U_G07_th3_k3y!
2020 CISCN z3
用 IDA 分析题目得知，程序将输入值经过运算后与 Dst 的密文对比，也就是知道解，求出未知数。
Dst 定义是 int 型（8 字节），将密文提取出来：
de = [0x4F17,0x9CF6,0x8DDB,0x8EA6,0x6929,0x9911,0x40A2,0x2F3E,0x62B6,0x4B82,0x486C,0x4002,0x52D7,0x2DEF,0x28DC,0x640D,0x528F,0x613B,0x4781,0x6B17,0x3237,0x2A93,0x615F,0x50BE,0x598E,0x4656,0x5B31,0x313A,0x3010,0x67FE,0x4D5F,0x58DB,0x3799,0x60A0,0x2750,0x3759,0x8953,0x7122,0x81F9,0x5524,0x8971,0x3A1D]
这里还是用手动申请变量，因为避免修改方程表达式。这道例题可以用 Int 也可以用 BitVec ，这里就用 BitVec
from z3 import * de = [0x4F17,0x9CF6,0x8DDB,0x8EA6,0x6929,0x9911,0x40A2,0x2F3E,0x62B6,0x4B82,0x486C,0x4002,0x52D7,0x2DEF,0x28DC,0x640D,0x528F,0x613B,0x4781,0x6B17,0x3237,0x2A93,0x615F,0x50BE,0x598E,0x4656,0x5B31,0x313A,0x3010,0x67FE,0x4D5F,0x58DB,0x3799,0x60A0,0x2750,0x3759,0x8953,0x7122,0x81F9,0x5524,0x8971,0x3A1D] v46=BitVec('v46',8) v47=BitVec('v47',8) v48=BitVec('v48',8) v49=BitVec('v49',8) v50=BitVec('v50',8) v51=BitVec('v51',8) v52=BitVec('v52',8) v53=BitVec('v53',8) v54=BitVec('v54',8) v55=BitVec('v55',8) v56=BitVec('v56',8) v57=BitVec('v57',8) v58=BitVec('v58',8) v59=BitVec('v59',8) v60=BitVec('v60',8) v61=BitVec('v61',8) v62=BitVec('v62',8) v63=BitVec('v63',8) v64=BitVec('v64',8) v65=BitVec('v65',8) v66=BitVec('v66',8) v67=BitVec('v67',8) v68=BitVec('v68',8) v69=BitVec('v69',8) v70=BitVec('v70',8) v71=BitVec('v71',8) v72=BitVec('v72',8) v73=BitVec('v73',8) v74=BitVec('v74',8) v75=BitVec('v75',8) v76=BitVec('v76',8) v77=BitVec('v77',8) v78=BitVec('v78',8) v79=BitVec('v79',8) v80=BitVec('v80',8) v81=BitVec('v81',8) v82=BitVec('v82',8) v83=BitVec('v83',8) v84=BitVec('v84',8) v85=BitVec('v85',8) v86=BitVec('v86',8) v87=BitVec('v87',8) v4=de[0] v5=de[1] v6=de[2] v7=de[3] v8=de[4] v9=de[5] v10=de[6] v11=de[7] v12=de[8] v13=de[9] v14=de[10] v15=de[11] v16=de[12] v17=de[13] v18=de[14] v19=de[15] v20=de[16] v21=de[17] v22=de[18] v23=de[19] v24=de[20] v25=de[21] v26=de[22] v27=de[23] v28=de[24] v29=de[25] v30=de[26] v31=de[27] v32=de[28] v33=de[29] v34=de[30] v35=de[31] v36=de[32] v37=de[33] v38=de[34] v39=de[35] v40=de[36] v41=de[37] v42=de[38] v43=de[39] v44=de[40] v45=de[41] s=Solver() s.add(v4 == 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52) s.add(v5 == 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52) s.add(v6 == 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52) s.add(v7 == 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52) s.add(v8 == 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52) s.add(v9 == 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52) s.add(v10 == 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52) s.add(v11 == 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59) s.add(v12 == 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59) s.add(v13 == 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59) s.add(v14 == 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59) s.add(v15 == 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59) s.add(v16 == 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59) s.add(v17 == 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59) s.add(v18 == 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66) s.add(v19 == 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66) s.add(v20 == 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66) s.add(v21 == 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66) s.add(v22 == 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66) s.add(v23 == 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66) s.add(v24 == 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66) s.add(v25 == 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73) s.add(v26 == 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73) s.add(v27 == 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73) s.add(v28 == 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73) s.add(v29 == 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73) s.add(v30 == 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73) s.add(v31 == 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73) s.add(v32 == 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80) s.add(v33 == 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80) s.add(v34 == 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80) s.add(v35 == 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80) s.add(v36 == 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80) s.add(v37 == 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80) s.add(v38 == 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80) s.add(v39 == 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87) s.add(v40 == 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87) s.add(v41 == 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87) s.add(v42 == 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87) s.add(v43 == 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87) s.add(v44 == 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87) s.add(v45 == 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87) print(s.check()) flag="" if s.check() == sat: m = s.model() print(m) else: print("no answer") flag = "" for d in m.decls(): print("%s = %s" % (d.name(), m[d]))
极客大挑战 REConvolution
这条题目演示用批量申请堆方法
题目关键函数：
int __cdecl main(int argc, const char **argv, const char **envp) { unsigned int ii; // esi unsigned int v4; // kr00_4 char flag_i; // bl unsigned int jj; // eax char *v7; // edx char v8; // cl int v9; // eax char xor_result[80]; // [esp+8h] [ebp-A4h] char flag[80]; // [esp+58h] [ebp-54h] sub_DC1020("Please input your flag: "); sub_DC1050("%40s", flag); memset(xor_result, 0, 0x50u); ii = 0; v4 = strlen(flag); if ( v4 ) { do { flag_i = flag[ii]; jj = 0; do { v7 = &xor_result[jj + ii]; v8 = flag_i ^ data1[jj++]; *v7 += v8; } while ( jj < 0x20 ); ++ii; } while ( ii < v4 ); } v9 = strcmp(xor_result, (const char *)&data2); if ( v9 ) v9 = -(v9 < 0) | 1; if ( v9 ) puts("No, it isn't."); else puts("Yes, it is."); return 0; }
加密过程并不是前两题的方程了，而是循环异或，没有修改方程变量名的问题，所以我们可以用 for 循环申请变量。
from z3 import * s = Solver() X = [BitVec(('x%s' % i),8) for i in range(0x22) ] data1 = [0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A, 0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E] data2 = [0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10, 0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2, 0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E, 0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3] xor_result = [0]*0x41 for m in range(0,0x22): for n in range(0,0x20): xor_result[n+m] += X[m] ^ data1[n] for o in range(0,0x41): s.add(xor_result[o] == data2[o]) if s.check() == sat: m = s.model() for i in range(0,0x22): print(chr(int("%s" % (m[X[i]]))),end='') else: print("failed to solve")
数独
z3 还能处理数独问题，下面是官方 demo ：
#!/usr/bin/env python # -*- coding: utf-8 -*- # @Author : MrSkYe # @Email : skye231@foxmail.com from z3 import * # 9x9整数变量矩阵 X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ] for i in range(9) ] # 每个单元格包含{1，…，9}中的值 cells_c = [ And(1 <= X[i][j], X[i][j] <= 9) for i in range(9) for j in range(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) ] # 每个3x3正方形最多包含一个数字 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) ] sudoku_c = cells_c + rows_c + cols_c + sq_c # 数独实例，我们用'0'表示空单元格 instance = ((0,0,0,0,9,4,0,3,0), (0,0,0,5,1,0,0,0,7), (0,8,9,0,0,0,0,4,0), (0,0,0,0,0,0,2,0,8), (0,6,0,2,0,1,0,5,0), (1,0,2,0,0,0,0,0,0), (0,7,0,0,0,0,5,2,0), (9,0,0,0,6,5,0,0,0), (0,4,0,9,7,0,0,0,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.evaluate(X[i][j]) for j in range(9) ] for i in range(9) ] print_matrix(r) else: print("failed to solve")
参考文章
实验推荐
CTF-REVERSE练习之逆向初探
（本实验将通过具体的实例介绍Ollydbg/IDA Pro/PEiD等工具在逆向分析中的基本使用方法，并通过动态调试和静态分析两种方法来找到程序密码。）