z3

基本知识

Z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，可以用来软件/硬件验证和测试，约束求解，混合系统分析，安全性研究，生物学研究（计算机分析）以及几何问题。通俗的来讲我们可以简单理解为它是一个解方程的计算器。

z3py的安装
- 应该可以直接使用pip安装，有两个包：z3和z3-solver
- linux下是使用GitHub官方仓库build
语法学习
- 注意变量使用给定的函数创建
- 几个常用API
  
  Solver()：创建一个通用求解器，创建后我们可以添加我们的约束条件，进行下一步的求解。
  add()：添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式。
  check()：通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会回显unsat。
  model()：在存在解的时候，该函数会将每个限制条件所对应的解集取交集，进而得出正解。

一个演示例子

# 创建基本变量
from z3 import *
x=Int('x')
y=Int('y')

# 创建求解器并给定约束条件
s=Solver()
s.add(x+y==5)
s.add(2*x+3*y==14)

# 约束求解
if s.check()==sat:
    result=s.model()

另一个缺憾：python struct: 解决bytes和其他二进制数据类型的转换

struct.pack(str,bytes)将任意数据打包成bytes
- str的可用参数：
  1. str[0]:> / < 来指定字节序
  2. 之后用一些字母标示对应的字节大小：常用的有h、i、q分别对应2、4、8个字节，一般来说标示一次可以对应一个/所有字节，前面加上数字即可指定个数
- bytes：可以是一个或很多个待打包值，
struct.unpack(str,bytes)将bytes按指定格式解包，具体参数同上；返回一个元组

题解

ida打开即明显提示为z3题，脚本如下：

from z3 import *
import struct

varList = ['v' + str(i) for i in range(46, 100)]# 命名v46~v99

solver = Solver()

for var in varList:
    globals()[var] = Int(var) # 创建z3变量
    solver.add(globals()[var] >= 0, globals()[var] <= 255) # 基本条件：大小1字节

resList = [0x174F0000, 0xF69C0000, 0xDB8D0000, 0xA68E0000, 0x29690000, 0x11990000, 0xA2400000, 0x3E2F0000, 0xB6620000, 0x824B0000, 0x6C480000, 0x02400000, 0xD7520000, 0xEF2D0000, 0xDC280000, 0x0D640000, 0x8F520000, 0x3B610000, 0x81470000, 0x176B0000, 0x37320000, 0x932A0000, 0x5F610000, 0xBE500000, 0x8E590000, 0x56460000, 0x315B0000, 0x3A310000, 0x10300000, 0xFE670000, 0x5F4D0000, 0xDB580000, 0x99370000, 0xA0600000, 0x50270000, 0x59370000, 0x53890000, 0x22710000, 0xF9810000, 0x24550000, 0x71890000, 0x1D3A0000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x003F4000, 0x00000000, 0x00000000, 0x00000000]

for i in range(4, 46):
    globals()['v' + str(i)] = struct.unpack('<i', bytes.fromhex(f"{resList[i - 4]:x}".rjust(8, '0')))[0]

print(v5)

# ida打开后显示的条件👇

solver.add(v4 == 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52, v5 == 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52, v6 == 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52, v7 == 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52, v8 == 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52, v9 == 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52, v10 == 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52, v11 == 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59, v12 == 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59, v13 == 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59, v14 == 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59, v15 == 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59, v16 == 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59, v17 == 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59, v18 == 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66, v19 == 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66, v20 == 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66, v21 == 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66, v22 == 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66, v23 == 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66, v24 == 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66, v25 == 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73, v26 == 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73, v27 == 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73, v28 == 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73, v29 == 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73, v30 == 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73, v31 == 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73, v32 == 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80, v33 == 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80, v34 == 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80, v35 == 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80, v36 == 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80, v37 == 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80, v38 == 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80, v39 == 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87, v40 == 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87, v41 == 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87, v42 == 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87, v43 == 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87, v44 == 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87, v45 == 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87)

# solve

if solver.check() != sat:
    print("failed")
    exit(0)

m = solver.model()

res = ''

print(m[v46].as_long())
for i in range(46, 46 + 42):
    res += chr(m[globals()['v' + str(i)]].as_long())

print(res)

hyperthreading

基本知识

注意线性加密=-=
反汇编的要求是不能有未定义语句，注意把这些语句全部patch掉再创建函数
题解

IDA打开，可以直接反汇编，由字符串please input your flag定位到关键代码
线程锁相关？进入到第一个加密函数，去除花指令
这里的一个关键是注意到这个加密函数一次只调用了输入字符串中的一个字符，进行移位加密
再去下一个加密函数确认：同样对输入字符串进行了常数级加密
由以上两步即可以看出，程序对输入字符串进行了线性加密，爆破密码表
- 这里的一个点是利用我爱破解特供版OD自动绕过了反动调。。。。
解密得flag

CTF-re-信安国赛初赛

heacsing 发布于 2020-08-23

z3

基本知识

题解

hyperthreading

基本知识

题解