Z3在逆向中运用

亲爱的,关注我吧

9/17

文章共计7370个词

预计阅读10分钟

来和我一起阅读吧

介绍

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 下载。https://github.com/Z3Prover/z3/releases

简单使用

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 变量可以进行异或

  solver.add(BitVec('x',8)^BitVec('y',8)==5)

• BitVec 变量值之间可进行>或=或=BitVec('b',8) BitVec('a',8)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 中不允许列表与列表之间添加==约束条件：

判断是否有解

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