normal28 （z3 进阶学习，向量异或，数值还原，yield使用）

一道简单的py累加题目，

可以直接解出

也可以z3

分析题目

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
#!/usr/bin/env python
# visit https://tool.lu/pyc/ for more information
# Version: Python 2.7

import struct
import time

def fun(start, end, s):#相当于生成key
    a = 32310901
    b = 1729
    c = s
    m = end - start #254
    while True:
        d = int((a * c + b) % m)
        yield d
        c = d

if __name__ == '__main__':
    arr = [77, 263, 394, 442, 463, 512, 667, 641, 804, 752, 885, 815, 1075, 1059, 1166, 1082, 1429, 1583, 1696, 1380, 1987, 2263, 2128, 2277,
           2387, 2670, 2692, 3255, 3116, 3306, 3132, 3659, 3139, 3422, 3600, 3584, 3343, 3546, 3299, 3633, 3281, 3146, 2990, 2617, 2780, 2893,
           2573, 2584, 2424, 2715, 2513, 2324, 2080, 2293, 2245, 2309, 2036, 1944, 1931, 1817, 1483, 1372, 1087, 1221, 893, 785, 697, 586, 547,
           324, 177, 184]

    flag = input('plz input your flag:')
    length = len(flag)
    a = struct.unpack('<I', flag[length - 4:].encode())[0] & 255 #小端，unsigned int,取倒数第4位
    b = []
    c = fun(1, 255, a)
    for i in range(32):
        b.append(next(c))
    #print(b)相当于key
    d = [ 0 for i in range(72) ]#初始化72*0
    for i in range(length):
        for j in range(32):
            a = ord(flag[i]) ^ b[j]
            d[i + j] += a
        
    
    for i in range(len(d)):
        if d[i] != arr[i]:
            print('fail')
            time.sleep(5)
            exit(0)
            continue
    print ('success')
    time.sleep(5)
    exit(0)

Z3在逆向中运用 - 合天网安实验室 - 博客园 (cnblogs.com)

Python yield 使用浅析 | 菜鸟教程 (runoob.com)

从CTF入门z3 solver - 翻车鱼 (shi1011.cn)

脚本编写

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
from z3 import*
def fun(start, end, s):
    a = 32310901
    b = 1729
    c = s
    m = end - start
    while True:
        d = int((a * c + b) % m)
        yield d
        c = d

def counter(b):
    s=Solver()
    flag=[BitVec(('%d'%i),8)for i in range(41)]
    arr = [77, 263, 394, 442, 463, 512, 667, 641, 804, 752, 885, 815, 1075, 1059, 1166, 1082, 1429, 1583, 1696, 1380,
           1987, 2263, 2128, 2277,
           2387, 2670, 2692, 3255, 3116, 3306, 3132, 3659, 3139, 3422, 3600, 3584, 3343, 3546, 3299, 3633, 3281, 3146,
           2990, 2617, 2780, 2893,
           2573, 2584, 2424, 2715, 2513, 2324, 2080, 2293, 2245, 2309, 2036, 1944, 1931, 1817, 1483, 1372, 1087, 1221,
           893, 785, 697, 586, 547,
           324, 177, 184]

    d = [0]*72
    for i in range(41):
        for j in range(32):
            a = flag[i] ^ b[j]
            d[i + j] += a
    for i in range(0,72):
     s.add(d[i]==arr[i])
    ans=[]
    if s.check() == sat:
        result = s.model()
        for a in flag:
            ans.append(result[a].as_long())
        print(''.join(chr(x)for x in ans))
    else:
        print("fxxk")

for a in range(32,127):
  b=[]
  r=fun(1,255,a)
  for i in range(32):
      b.append(next(r))
  counter(b)

Syc{Y0u_S3e_Z3_1s_soooo00000_Interest1ng}