Z3

学前准备

先在本地机上安装Z3求解器

win+r cmd打开终端

1
pip  install  z3-solver

然后去pycharm或者vscode去输入以下代码去看看是否可以正常运行：

1
2
3
4
5
6
7
8
9
10
11
from z3 import*
a,b,c = BitVecs('a b c',32)
d,e,f = BitVecs('d e f',32)
g,h,i = BitVecs('g h i',32)
key = [a,b,c,d,e,f,g,h]
s = Solver()
s.add()
check = s.check()
print(check)
model = s.model()
print(model)

运行正常会显示：没报错

img

定义声明变量

1
2
3
4
5
6
7
8
9
10
11
12
#整型变量
from z3 import *
a = Int('a')#声明单个整型变量
a,b = Ints('a b')#声明多个整型变量
#实型变量
from z3 import *
a = Real('a')#声明单个实型变量
a,b = Reals('a b')#声明多个实型变量
#向量变量
from z3 import *
a = BitVec('a',8) #声明单个8位的变量
a, b = BitVec('a b',8)#声明多个8位的变量

z3函数使用

简单的使用举例：

1
2
3
4
5
6
7
8
from z3 import *
#首先调用z3模块
a,b = Ints('a b')
#声明a，b两个变量是int型变量
solve(a>3,b<8,2*a+b==16)
#slove（）设置约束条件，就如括号中的条件，然后自动生成a和b，像是解数学函数一样
#程序结束自动输出a，b的值
#结果 [a = 5, b = 6]

如果是出现有多种情况的时候，会只输出最近的一种情况：

1
2
solve(a>3,b<8,a+b<16)
#结果 [a = 0, b = 4]

在解决问题是很多情况下是有多个约束条件的。这个时候可以先生成一个求解器对象(Solver())，然后就可以方便的向其中添加更多的约束条件。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
#-*- coding=utf-8 -*-
from z3 import *
a,b = Ints('a b')
solver = Solver()
#创建一个求解器对象solver（）
solver.add(a+b==10)
#用solver.add方法添加约束条件
solver.add(a-b==6)
#用solver.add方法添加约束条件
if solver.check() == sat: 
#check()方法用来判断是否有解，sat表示满足有解
    ans = solver.model()
    #solver.model()表示求到的解
    print(ans)
    #也可以用变量名作为下标得到解
    #print(solver.model())
    print(ans[a])
    #表示只输出解中的a部分
else:
    print("no ans!")

Buuctf [GWCTF 2019]pyre

下载文件，是一个pyc文件，使用uncompyle6命令反编译一下

uncompyle6 attachment.pyc > 1.py

生成了新的py文件：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
# uncompyle6 version 3.9.0
# Python bytecode version base 2.7 (62211)
# Decompiled from: Python 3.10.7 (tags/v3.10.7:6cc6b13, Sep  5 2022, 14:08:36) [MSC v.1933 64 bit (AMD64)]
# Embedded file name: encode.py
# Compiled at: 2019-08-19 21:01:57
print 'Welcome to Re World!'
print 'Your input1 is your flag~'
l = len(input1)
#将l赋值为input1的长度（这里大概率就是输入的flag）
for i in range(l):
    num = ((input1[i] + i) % 128 + 128) % 128
    code += num
#for循环，遍历input1的每一个函数，每一个元素都加上i然后模除128之后再加上128然后再破除128
#然后将得到的结果形成一个列表code，用来存储经过第一轮加密之后的数据
for i in range(l - 1):
    code[i] = code[i] ^ code[i + 1]
#第二次循环，对code列表从第一个到倒数第一个遍历，前者赋值为前者异或后者
print code
code = ['\x1f', '\x12', '\x1d', '(', '0', '4', '\x01', '\x06', '\x14', '4', ',', 
 '\x1b', 'U', '?', 'o', '6', '*', ':', '\x01', 'D', ';', '%', '\x13']
# okay decompiling attachment.pyc

分析上面的加密过程，大概是输入了一串flag，然后经过第一段加i模除的运算，然后再把得到的结果进行一个前后异或计算，最后得到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
from z3 import *
lb=[]
flag=[]
code = ['\x1f', '\x12', '\x1d', '(', '0', '4', '\x01', '\x06', '\x14', '4', ',','\x1b', 'U', '?', 'o', '6', '*', ':', '\x01', 'D', ';', '%', '\x13']
code = [ord(i) for i in code]
#将code中的所有元素都经过一个ord函数变成其ascll吗的形式方便计算
# print(code)
l=len(code)
#l存储为code的长度
#print(len(code))
for i in range(l-1):
    code[l-i-2] ^= (code[l-i-1])
#一个循环，使被异或的新数值都异或回去
#以上就是异或的脚本下面是模除部分的脚本
solve = Solver()
#定义一个解释器对象Solver（）
for i,v in enumerate(code):
#一个for的enumerate的循环，其中在循环中，i代表循环变量，v代表code[i]
    # x=z3.Int(f"V{i}")
    x = z3.Int('v%d'% i)
    #定义了一个int形式的变量x，并且赋值为v[i]（可以这么理解）
    solve.add(x > 31)
    solve.add(x < 128)
    #添加限制条件，限制只能是有输出字符的参与计算
    solve.add(((x+ i) % 128 + 128) % 128 == v)
    #题目中的要求
    lb.append(x)
    #把x的值存入lb列表中
#print(solve.check())
# print(solve.model())
if solve.check()==sat:
#判断如果有解就把解存入flag
    flag=solve.model()
    #开始计算求解，并且把解放到flag中
    # for i in range(len(flag)):
    # print((flag[i]))
#print(lb)
#print(flag)
for i in lb:
    print(chr(flag[i].as_long()),end='')
#此时lb存储的是v1，v2，v3，然后输出flag[v1]....

[GUET-CTF2019]re

首先拖入die查看，有壳，upx壳，64位

img

拖入虚拟机里面脱壳

img

然后拖到64位ida中反编译一下，没有main函数，但是有点离谱

img

但是找到了start函数

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
  int v6; // edx
  int v7; // ecx
  int v8; // r8d
  int v9; // r9d
  __int64 result; // rax
  __int64 v11; // [rsp+0h] [rbp-30h] BYREF
  unsigned __int64 v12; // [rsp+28h] [rbp-8h]

  v12 = __readfsqword(0x28u);
  sub_40F950((unsigned int)"input your flag:", a2, a3, a4, a5, a6, 0LL, 0LL, 0LL, 0LL);
  sub_40FA80((unsigned int)"%s", (unsigned int)&v11, v6, v7, v8, v9, v11);
  if ( (unsigned int)sub_4009AE(&v11) )
    sub_410350("Correct!");
  else
    sub_410350("Wrong!");
  result = 0LL;
  if ( __readfsqword(0x28u) != v12 )
    sub_443550();
  return result;
}

可以看到有一个if语句，只要if达成，就可以输出正确，所以去看看那个函数，然后找到了一堆if

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
53
54
55
56
57
58
59
60
61
62
63
{
  if ( 1629056 * *a1 != 166163712 )
    return 0LL;
  if ( 6771600 * a1[1] != 731332800 )
    return 0LL;
  if ( 3682944 * a1[2] != 357245568 )
    return 0LL;
  if ( 10431000 * a1[3] != 1074393000 )
    return 0LL;
  if ( 3977328 * a1[4] != 489211344 )
    return 0LL;
  if ( 5138336 * a1[5] != 518971936 )
    return 0LL;
  if ( 7532250 * a1[7] != 406741500 )
    return 0LL;
  if ( 5551632 * a1[8] != 294236496 )
    return 0LL;
  if ( 3409728 * a1[9] != 177305856 )
    return 0LL;
  if ( 13013670 * a1[10] != 650683500 )
    return 0LL;
  if ( 6088797 * a1[11] != 298351053 )
    return 0LL;
  if ( 7884663 * a1[12] != 386348487 )
    return 0LL;
  if ( 8944053 * a1[13] != 438258597 )
    return 0LL;
  if ( 5198490 * a1[14] != 249527520 )
    return 0LL;
  if ( 4544518 * a1[15] != 445362764 )
    return 0LL;
  if ( 3645600 * a1[17] != 174988800 )
    return 0LL;
  if ( 10115280 * a1[16] != 981182160 )
    return 0LL;
  if ( 9667504 * a1[18] != 493042704 )
    return 0LL;
  if ( 5364450 * a1[19] != 257493600 )
    return 0LL;
  if ( 13464540 * a1[20] != 767478780 )
    return 0LL;
  if ( 5488432 * a1[21] != 312840624 )
    return 0LL;
  if ( 14479500 * a1[22] != 1404511500 )
    return 0LL;
  if ( 6451830 * a1[23] != 316139670 )
    return 0LL;
  if ( 6252576 * a1[24] != 619005024 )
    return 0LL;
  if ( 7763364 * a1[25] != 372641472 )
    return 0LL;
  if ( 7327320 * a1[26] != 373693320 )
    return 0LL;
  if ( 8741520 * a1[27] != 498266640 )
    return 0LL;
  if ( 8871876 * a1[28] != 452465676 )
    return 0LL;
  if ( 4086720 * a1[29] != 208422720 )
    return 0LL;
  if ( 9374400 * a1[30] == 515592000 )
    return 5759124 * a1[31] == 719890500;
  return 0LL;
}

对此，可以用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
from z3 import *
s = Solver()
a1 = [0]*32
for i in range(32):
    a1[i] = Int('a1['+str(i)+']')

s.add( 1629056 * a1[0] == 166163712 )
s.add( 6771600 * a1[1] == 731332800 )
s.add( 3682944 * a1[2] == 357245568 )
s.add( 10431000 * a1[3] == 1074393000 )
s.add( 3977328 * a1[4] == 489211344 )
s.add( 5138336 * a1[5] == 518971936 )
s.add( 7532250 * a1[7] == 406741500 )
s.add( 5551632 * a1[8] == 294236496 )
s.add( 3409728 * a1[9] == 177305856 )
s.add( 13013670 * a1[10] == 650683500 )
s.add( 6088797 * a1[11] == 298351053 )
s.add( 7884663 * a1[12] == 386348487 )
s.add( 8944053 * a1[13] == 438258597 )
s.add( 5198490 * a1[14] == 249527520 )
s.add( 4544518 * a1[15] == 445362764 )
s.add( 3645600 * a1[17] == 174988800 )
s.add( 10115280 * a1[16] == 981182160 )
s.add( 9667504 * a1[18] == 493042704 )
s.add( 5364450 * a1[19] == 257493600 )
s.add( 13464540 * a1[20] == 767478780 )
s.add( 5488432 * a1[21] == 312840624 )
s.add( 14479500 * a1[22] == 1404511500 )
s.add( 6451830 * a1[23] == 316139670 )
s.add( 6252576 * a1[24] == 619005024 )
s.add( 7763364 * a1[25] == 372641472 )
s.add( 7327320 * a1[26] == 373693320 )
s.add( 8741520 * a1[27] == 498266640 )
s.add( 8871876 * a1[28] == 452465676 )
s.add( 4086720 * a1[29] == 208422720 )
s.add( 9374400 * a1[30] == 515592000 )
s.add(5759124 * a1[31] == 719890500)
s.check()
print(s.model())
for i in range(32):
  print(al[il)

然后发现没有a[6],爆破一下得到flag

赛题复现

愚人杯-esay_pyc

本题附件给到的是一个pyc文件，需要用uncompyle6进行反编译成py文件然后才可以查看源代码

uncompyle6 ez_re.pyc > ez_re.py

生成了ez_re.py的源代码文件

img

拖动到pycharm，查看源码

img

程序源代码以及程序分析：

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
uncompyle6 version 3.9.0
# Python bytecode version base 2.7 (62211)
# Decompiled from: Python 3.10.7 (tags/v3.10.7:6cc6b13, Sep  5 2022, 14:08:36) [MSC v.1933 64 bit (AMD64)]
# Embedded file name: enpyc.py
# Compiled at: 2023-03-29 18:30:23
print 'Welcome to CTFshow Re!'
print 'your flag is here!'
flag = ''
#定义了一个空列表，名字为flag
l = len(flag)#l赋值为flag的长度
for i in range(l):
    num = ((flag[i] + i) % 114514 + 114514) % 114514
    #在循环中，flag[i]先加上自己，然后%114514，但是114514已经很大了，所以flag[i]&114514还是本身，可以忽略
    code += chr(num)
    #定义一个code，且存储经过计算的num的字符形式

code = map(ord, code)
#一个map函数，类似于一个循环，遍历每一个code的元素然后变为ord形式
for i in range(l - 4 + 1):
    #一个for循环，把列表从0~l-4+1遍历一遍
    code[i] = code[i] ^ code[i + 1]
    #实现的功能是code的第i位和i+1位进行异或计算
print code
code = ['\x16', '\x1d', '\x1e', '\x1a', '\x18', '\t', b'\xff', b'\xd0', ',', '\x03', 
 '\x02', '\x14', '8', 'm', '\x01', 'C', 'D', b'\xbd', b'\xf7', '*', '\r', 
 b'\xda', b'\xf9', '\x1c', '&', '5', "'", b'\xda', b'\xd4', b'\xd1', '\x0b', 
 b'\xc7', b'\xc7', '\x1a', b'\x90', 'D', b'\xa1']
# okay decompiling ez_re.pyc

python解题脚本和分析：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
-*- encoding:utf-8 -*-
code = ['\x16', '\x1d', '\x1e', '\x1a', '\x18', '\t', '\xff', '\xd0', ',', '\x03', '\x02', '\x14', '8', 'm', '\x01', 'C', 'D', '\xbd', '\xf7', '*', '\r', '\xda', '\xf9', '\x1c', '&', '5', "'", '\xda', '\xd4', '\xd1', '\x0b', '\xc7', '\xc7', '\x1a', '\x90', 'D', '\xa1']
temp=list(map(ord,code))
#将code中的字符转换成ascii码值放入temp
#temp=[22, 29, 30, 26, 24, 9, 255, 208, 44, 3, 2, 20, 56, 109, 1, 67, 68, 189, 247, 42, 13, 218, 249, 28, 38, 53, 39, 218, 212, 209, 11, 199, 199, 26, 144, 68, 161]

for i in range(len(temp)-3)[::-1]:
    #从倒数第四个元素开始异或处理
    temp[i]=temp[i]^temp[i+1]

#temp=[99, 117, 104, 118, 108, 116, 125, 130, 82, 126, 125, 127, 107, 83, 62, 63, 124, 56, 133, 114, 88, 85, 143, 118, 106, 76, 121, 94, 132, 80, 129, 138, 77, 138, 144, 68, 161]

for i in range(len(temp)):
    print(chr(temp[i]-i),end='')

#ctfshow{Just_F00l's_D@y_R3_Ch3ck-in!}

有一个小问题，有时候在执行程序的时候，会出现一个报错：Non-UTF-8 code starting with…..

这个报错应该是表示没有utf-8的编码格式，在程序中加入以下代码就可以解决了：

1
# -*- encoding:utf-8 -*-

愚人杯-easy_cc

拖到die中查壳，32位无壳

img

拖入32位ida，f5查看伪代码

img

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
53
54
55
 strcpy(v19, "key123");//将key123写入v19
  sub_941010((char *)&Format, v16[0]);
  v4 = _acrt_iob_func(0);
  fgets(Buffer, 100, v4);
  v5 = strcspn(Buffer, "\n");
  if ( v5 >= 0x64 )
    goto LABEL_16;
  v15 = v3;
  Buffer[v5] = 0;
  v6 = 0;
  v7 = strlen(Buffer);
  if ( v7 )
  {
    v8 = strlen(v19);
    do
    {
      v17[v6] = Buffer[v6] ^ v19[v6 % v8];
      ++v6;
    }
    while ( v6 < v7 );
    if ( v6 >= 0xC9 )
      goto LABEL_16;
  }
  v17[v6] = 0;
  v9 = 0;
  v10 = strlen(v17);
  if ( v10 )
  {
    v11 = v16;
    do
    {
      sub_941040(v11, "%02x", v17[v9++]);
      v11 += 2;
    }
    while ( v9 < v10 );
  }
  v12 = 2 * v9;
  if ( v12 >= 0xC9 )
  {
LABEL_16:
    __report_rangecheckfailure(v15);
    __debugbreak();
  }
  v16[v12] = 0;
  sub_941010("\n", v15);
  v13 = strcmp(v16, "08111f425a5c1c1e1a526d410e3a1e5e5d573402165e561216");
  if ( v13 )
    v13 = v13 < 0 ? -1 : 1;
  if ( v13 )
    sub_941010("flag is false: ", v16[0]);
  else
    sub_941010("flag is true: ", v16[0]);
  system("pause");
  return 0;
}

可以看到最重要的一句就是：

1
v17[v6] = Buffer[v6] ^ v19[v6 % v8];

这是buffer和v19进行异或计算然后赋值给v16，最后一个strcmp和一些种数字串比较

08111f425a5c1c1e1a526d410e3a1e5e5d573402165e561216

刚开始看不懂和buffer[]进行模除计算的是什么，自己计算一遍之后才知道，是和v19异或完了之后然后继续从头异或的一个算法，就是key123异或完继续key123的顺序异或

然后就可以写一个异或解题脚本了：

1
2
3
4
5
6
7
8
9
list1=[0x08,0x11,0x1f,0x42,0x5a,0x5c,0x1c,0x1e,0x1a,0x52,0x6d,0x41,0x0e,0x3a,0x1e,0x5e,0x5d,0x57,0x34,0x02,0x16,0x5e,0x56,0x12,0x16]
list2=['k','e','y','1','2','3']
l=len(list2)
#定义一下list2列表的长度，方便在list1比list2长度长的时候重头异或
flag=''
for i in range(len(list1)):
    flag+=chr(list1[i]^ord(list2[(i%l)]))
print(flag)
#ctfshow{cc_re_good_good!}

这里看到有字符串就以为是base64或者密码的问题应该改改，这里其实很明显的是16进制的字符串

还有大佬关于list2列表的定义：

1
2
Buffer="key123"
buffer=list(Buffer)