L1E6N0A2

监督自己不断学习

0%

每日一题3-15

发表于 更新于
本文字数： 4.8k 阅读时长 ≈ 4 分钟

Z3求解器在CTF中的应用

Postion——Reversing.kr

首先题目描述如下：

Find the Name when the Serial is 76876-77776
This problem has several answers.

Password is ***p

有一个Postion.exe，需要输入正确的用户名和对应的序列号，我们需要序列号76876-77776对应的用户名，根据题目用户名为4位，且最后一位是“p“。使用IDA打开程序。

函数有点多，甚至找不到主要函数。

ida

用ollydbg打开看一下。找到字符串”Wrong“和”Correct“，上面有一个调用（call Postion.00401740）

猜测1740这个位置应该是判断逻辑的核心代码。

string

返回IDA，确定关键函数就是sub_CA1740了，只需要对这个函数进行分析就好了。F5查看伪代码。

函数的大体思路就是经过一系列的if条件判断，判断成功之后会返回1（成功的标志）

  1. 首先创建了三个变量，分别是name、serial和中间变量。

1

  1. 判断name的长度为4，取值范围从a-z，4个字母都满足条件后进入下面的if

判断

  1. GetWindowText获得输入的字符串，第一个是name（v50），第二个是serial（v51）

    要求name的四个输入为小写字母且各不相同。当name通过检查后，才会进行serial的获取。要求serial是一个长为11的字符串，且serial[5] ==’-‘

2

  1. serial格式验证通过后就是通过name计算出结果，将结果与serial比对的过程。

    GetAt(a, pos) = a[pos]

    (a » count )&1表示取a的第count+1位， ((name » 4) & 1) 是取name从右向左第5个比特

    首先获得name[0]和name[1], 分别进行处理得到几个变量。

3

​ 之后比较serial[0]和v40+v8是否相同。

4

​ 这个过程可以转化为一个等式约束：

1
((username[0]&1)+5+((((username[1]&4)!=0) +1))== 7

​ 类似的，比较serial[1]和v46+v36是否相等。

5

1
(((username[0]&8)!=0)+5+((((username[1]&8)!=0) +1))== 6

以此类推，可以得到10个不等式作为约束条件。

1
2
3
4
5
6
7
8
9
10
((username[0]&1)+5+((((username[1]&4)!=0) +1))== 7
(((username[0]&8)!=0)+5+((((username[1]&8)!=0) +1))== 6
(((username[0]&2)!=0)+5+((((username[1]&0x10)!=0) +1))== 8
(((username[0]&4)!=0)+5+((((username[1]&1)!=0) +1))== 7
(((username[0]&0x10)!=0)+5+((((username[1]&2)!=0) +1))== 6
((username[2]&1)+5+((((username[3]&4)!=0) +1))== 7
(((username[2]&8)!=0)+5+((((username[3]&8)!=0) +1))== 7
(((username[2]&2)!=0)+5+((((username[3]&0x10)!=0) +1))== 7
(((username[2]&4)!=0)+5+((((username[3]&1)!=0) +1))== 7
(((username[2]&0x10)!=0)+5+((((username[3]&2)!=0) +1))== 6

程序分析完毕，根据下面的约束，编写程序利用Z3求解器求解得到name：

（1）上面的10个约束方式

（2）题目中给出的name[3]=’p’

（3）name有4位，每位取值范围a-z

Z3安装很简单：pip install z3-solver

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
from z3 import *
#创建四个符号变量
username = [BitVec('u%d'%i,8) for i in range(0,4)]
solver = Solver() 
#设置约束条件
solver.add(((username[0]&1)+5+((((username[1]&4)!=0) +1))== 7)
solver.add((((username[0]&8)!=0)+5+((((username[1]&8)!=0) +1))== 6)
solver.add((((username[0]&2)!=0)+5+((((username[1]&0x10)!=0) +1))== 8)
solver.add((((username[0]&4)!=0)+5+((((username[1]&1)!=0) +1))== 7)
solver.add((((username[0]&0x10)!=0)+5+((((username[1]&2)!=0) +1))== 6)
solver.add(((username[2]&1)+5+((((username[3]&4)!=0) +1))== 7)
solver.add((((username[2]&8)!=0)+5+((((username[3]&8)!=0) +1))== 7)
solver.add((((username[2]&2)!=0)+5+((((username[3]&0x10)!=0) +1))== 7)
solver.add((((username[2]&4)!=0)+5+((((username[3]&1)!=0) +1))== 7)
solver.add((((username[2]&0x10)!=0)+5+((((username[3]&2)!=0) +1))== 6)
solver.add(username[3] == ord('p'))
for i in range(0,4):
    solver.add(username[i] >= ord('a'))
    solver.add(username[i] <= ord('z'))

solver.check()
result = solver.model()

flag = ''
for i in range(0,4):
    flag += chr(result[username[i]].as_long().real)
print flag

这样的程序，!=0运算得到的是BoolRef类型的，和int型无法做加法，类型转化无法实现

阅读汇编代码，shr右移指令，可以把约束进行等价修改。

右移

1
2
3
4
5
6
7
8
9
10
((username[0]&1)+5+(((username[1]>>2) & 1 )+1))==7
((((username[0]>>3) & 1)+5)+(((username[1]>>3)&1)+1))==6
(((username[0]>>1) & 1)+5+(((username[1]>>4) & 1 )+1))==8
(((username[0]>>2) & 1)+5+(((username[1]) & 1 )+1))==7
(((username[0]>>4) & 1)+5+(((username[1]>>1) & 1 )+1))==6
(((username[2]) & 1)+5+(((username[3]>>2) & 1 )+1))==7
(((username[2]>>3) & 1)+5+(((username[3]>>3) & 1 )+1))==7
(((username[2]>>1) & 1)+5+(((username[3]>>4) & 1 )+1))==7
(((username[2]>>2) & 1)+5+(((username[3]) & 1 )+1))==7
(((username[2]>>4) & 1)+5+(((username[3]>>1) & 1 )+1))==6

运行之后得到输出 bump，只是其中一个解

bump

验证一下正确。

correct

如果想把所有的解都输出，可以对代码进行下面的修改。

1
2
3
4
5
6
7
8
9
10
11
while(solver.check()==sat):
    condition = []
    m = solver.model()
    p=""
    for i in range(4):
      p+=chr(m[username[i]].as_long())
      condition.append(username[i] != int("%s" % (m[username[i]])))
    print(p)
    # Or:condition中有很多约束，为了去掉新的解和已有的解每一位都一样的那种重复情况
    # https://blog.csdn.net/qq_37400312/article/details/108962459
    solver.add(Or(condition))

输出结果如下，这四个都可以，但是gpmp不符合要求，因为程序中规定了不允许有重复的字符出现，其他三个都是正确的username。

out

问题：

  1. as_long函数是什么？ 类型转化
  2. ！=0 boolref的类型转化可以解决吗？不能解决

Re

首先拉入IDA，反编译查看源码

1-1

程序输入两个参数，第二个参数的长度不能超过0xF（15位）且第二个参数的前7位的asc码的和要等于801，如果等于801，就输出flag。

所以我们的目标是构造第二个输入，使之满足要求。代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
from z3 import *
solver = Solver()
# 创建7个符号变量
pwd = [Int('a%d' % i) for i in range(7)]

# 设置7个字符的取值范围在32-126之间(可见字符)
for i in pwd:
    solver.add(i >= 32) #48
    solver.add(i < 127) #123

# 相加为801
solver.add(pwd[0] + pwd[1] + pwd[2] + pwd[3] + pwd[4] + pwd[5] + pwd[6] == 801)

if solver.check() == sat:
    password = ''
    result = solver.model()
    for i in range(7):
        password += (chr(result[pwd[i]].as_long()))
    print (password)

输出一组答案，看上去很奇怪，可以修改pwd的取值范围，改为48-122（数字+字母），得到新的答案，经过验证都正确，得到flag：SAYCURE{L3ts_g3t_in2_R3}

3-1

4-1

2-1

（需要注意的是，re2文件需要在linux环境下执行）