in0va'S Blog JustLearnM0re

犯二

0%

Z3初探

发表于 更新于 分类于

0x01 Z3简介

1
2
3
4
5
Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.
If you are not familiar with Z3, you can start here.
Pre-built binaries for releases are available from here, and nightly builds from here.
Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.
See the release notes for notes on various stable releases of Z3.

Z3是微软研究院的一个定理证明工具(SMT求解)，它是根据MIT许可证授权的，能够解决给定约束条件来求解满足值的问题。通常用来检查表达式的逻辑是否满足。

Z3在计算机领域常用于软件验证、逻辑分析等；CTF中常被用于密码学、二进制逆向、符号执行、Fuzz等领域。Angr中就内置了一个Z3约束求解器用来求解满足条件的路径约束。

0x02 安装

贴一下gayhub地址：https://github.com/Z3Prover/z3

clone下Z3源码，进入文件目录

1
2
3
4
python scripts/mk_make.py --python
cd build
make
make install

//bpython真好用，补全还有自动提示，只是循环的时候和低版本的ipython一样不能回到上一行

0x03 常用API

Solver()：创建求解器

add()：变量之间增加约束条件

check()：检查约束条件

model()：列出求解结果

Int()：声明一个整形的变量

Real()：声明一个实殊变量

BitVec()：声明一个变量数组

0x04 实例

iscc2018 Reverse My_math_is_bad

拿到题目首先扔ida看一下，找到主要逻辑

逻辑还是很简单的，输入32个字节大小的字符串，4字节一组转为整形，一共分成8组，前四组后四组满足两个方程组就行了。

大二的时候做这道题的时候用的matlab解的，orz，变量一个一个敲进去，是很烦了，还是Z3方便，一把梭。

逻辑可以说很清晰了，申明变量，建立约束，再整形格式化成字符串就是flag了

贴下脚本：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
from z3 import *
from binascii import *
import ctypes
a=Int('a')
b=Int('b')
c=Int('c')
d=Int('d')
s=Solver()
s.add(a*b-c*d==2652042832920173142)
s.add(3*d+4*c-b-2*a==397958918)
s.add(3*a*c-d*b==3345692380376715070)
s.add(27*b+a-11*c-d==40179413815)
print s.check()
print s.model()
a=1869639009
b=1801073242
c=862734414
d=829124174
flag=''
flag=a2b_hex(hex(a)[2:])[::-1]+a2b_hex(hex(b)[2:])[::-1]+a2b_hex(hex(d)[2:])[::-1]+a2b_hex(hex(c)[2:])[::-1]
#print flag
seed = a ^ b ^ c ^ d
dll = ctypes.CDLL("/lib/x86_64-linux-gnu/libc.so.6")
dll.srand(seed)
v1 = dll.rand() % 50;
v2 = dll.rand() % 50;
v7 = dll.rand() % 50;
v8 = dll.rand() % 50;
v9 = dll.rand() % 50;
v10 = dll.rand() % 50;
v11 = dll.rand() % 50;
v12 = dll.rand() % 50;

print v1,v2,v7,v8,v9,v10,v11,v12
v3 = Int('v3')
v4 = Int('v4')
v5 = Int('v5')
v6 = Int('v6')

t = Solver()
t.add(v6 * v2 + v3 * v1 - v4 - v5 == 61799700179)
t.add(v6 + v3 + v5 * v8 - v4 * v7 == 48753725643)
t.add(v3 * v9 + v4 * v10 - v5 - v6 == 59322698861)
t.add(v5 * v12 + v3 - v4 - v6 * v11 == 51664230587)
t.check()
print t.model()
v3=811816014
v4=828593230
v5=1867395930
v6=1195788129
flag+=a2b_hex(hex(v3)[2:])[::-1]+a2b_hex(hex(v4)[2:])[::-1]+a2b_hex(hex(v5)[2:])[::-1]+a2b_hex(hex(v6)[2:])[::-1]
print flag

iscc2018 Reverse obfuscation_and_encode

main函数里面函数还是非常清晰的：

发现主要是fencode和encode两个函数，对输入进行加密，之后与固定字符串lUFBuT7hADvItXEGn7KgTEjqw8U5VQUq进行对比，先分析一下fencode函数，分析参数大概能猜出它做的操作。

看cfg发现是控制流平坦化，程序应该是用ollvm混淆过的，一般逻辑贼复杂的那种都是用pin或者angr跑的，但是这题好像混淆后的逻辑并不复杂，给关键代码下断动态调一下：

大致能分析出逻辑：输入24个字节大小的字符串，4个字节分一组，分成6组，每一组与[{2,2,4,-5},{1,1,3,-3},{-1,-2,-3,4},{-1,0,-2,2}]中对应idx的数组进行乘法操作，结果相加。一共生成6组*4数组个大小的字节，也就是24个字节，存入buffer数组中。

之后encode函数，看参数和之后要对比的字符串其实就能猜出来，再看一下逻辑：

根据汇编代码看出是个3转4的操作，确定是base64，看ALPHA_BASE发现已经被替换了。很常见的base64表替换加密，encode的加密就清楚了。

还原出伪代码：

1
2
3
4
5
6
for(v12=0;v12<6;v12++)
    for(v11=0;v11<4;v11++)
        a2[i] = v10%127
        v10 = 0
        for(v9=0;v9<4;v9++)
            v10 += input[4*v12+v9]*m[4*v11+v9]

这边贴下代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
from z3 import *

trans = [37, 192, 59, 166, 31, 175, 76, 165, 203, 139, 164, 155, 59, 225, 40, 133, 38, 38, 22, 231, 17, 9, 7, 38]
m = [2,2,4,-5,1,1,3,-3, -1, -2, -3, 4, -1, 0, -2,2]
a = Real('a')
b = Real('b')
c = Real('c')
d = Real('d')

for i in range(6):
    	s = Solver()
    	s.add((2 * a + 2 * b + 4 * c - 5 * d) == trans[4 * i])
	s.add((a + b + 3 * c - 3 * d)== trans[4*i+1])
	s.add((-1 * a - 2 * b -3 * c + 4 * d) == trans[4 * i + 2])
	s.add(( -1 * a  - 2 * c + 2 * d) == trans[4 * i + 3])
	#print s
	if s.check() == sat:
	    print s.model()
	else :
	    print s.check()


'''
[b = 620, a = 358, d = 871, c = 609]
[b = 612, a = 379, d = 863, c = 591]
[b = 816, a = 889, d = 1119, c = 597]
[b = 590, a = 331, d = 855, c = 623]
[b = 560, a = 351, d = 620, c = 329]
[b = 109, a = 86, d = 125, c = 63]
'''

'''
#[b = 108, a = 102, c = 97, d = 103]
#[b = 100, a = 123, c = 79, d = 95]
#[b = 48, a = 121, c = 85, d = 95]
#[b = 78, a = 75, c = 111, d = 87]
#[b = 48, a = 95, c = 73, d = 108]
#[b = 109, a = 86, c = 63, d = 125]
'''



f = [102,108,97,103,123,100,79,95,121,48,85,95,75,78,111,87,95,48,73,108,86,109,63,125]
print map(chr,f)
flag = ''
for i in f:
    flag += chr(i)
print flag

0x05 总结

Z3的接口还是很多的，这边只用了几个常用的，这边贴一下文档：
https://z3prover.github.io/api/html/namespacez3py.html

https://ericpony.github.io/z3py-tutorial/guide-examples.htm

https://rise4fun.com/Z3/tutorial/guide

这个视频讲的自动化分析挺不错的，贴一下：

https://www.bugbank.cn/live/view.html?id=111348

之前打算去分析Z3源码的，后来一想其实没必要，毕竟这种专门处理数理计算的工具内部实现肯定设计到一些数学定理？？？23333333，猜测类似的有对浮点指令集等操作的函数实现，肯定是很复杂的。Z3牛逼~