SCTF2023 Rewp

发表于2023-07-09更新于2023-07-09

SCTF2023 Rewp

Syclang

硬啃IR，手动反汇编

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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
#include <stdio.h>

struct exp {
    int key[24];
    int L[8];
    int R[8];
    int X[8];
};


int main(int argc,char** argv)
{
    char var11;
    exp myInput, var23, var24, var25;
    //arg var11
    char* temp1 = read();
    int temp4 = 24;
    for (int i = 0; i < 24; i++) {
        myInput.key[i] = temp1[23-i];
    }
    
    for (int i = 23; i > 0; i--) {
        myInput.key[i] = myInput.key[i] - myInput.key[i - 1];
    }


    int L[] = {0, 15, 2, 10, 6, 9, 1, 4};
    int R[] = {8, 23, 11, 20, 13, 21, 19, 17};
    int X[] = {11, -13, 17, -19, 23, -29, 31, -37};
    
    for(int i = 0; i < 8; i++) {
        myInput.L[i] = L[i];
        myInput.R[i] = R[i];
        myInput.X[i] = X[i];
    }

    for (int i = 0; i < 8; i++) {
        myInput.key[myInput.L[i]] += myInput.X[i];
        myInput.key[myInput.R[i]] -= myInput.X[i];
    }
    
    for (int i = 1; i < 24; i++) {
		myInput.key[i] += myInput.key[i - 1];
    }

	for (int i = 0; i < 23; i++) {
		int var12 = myInput.key[i];
		int var13 = myInput.key[i + 1];
        
		myInput[i] = myInput.key[i] ^ myInput.key[i + 1];
 	}

    int L1[] = {0, 9, 9, 8, 10, 9, 1, 0};
    int R1[] = {12, 10, 12, 19, 12, 13, 22, 23};
    int X1[] = {-19, -10, 3, -11, -9, 3, -19, 7};
    for (int i = 0; i < 8; i++) {
		var24.L[i] = L1[i];
		var24.R[i] = R1[i];
		var24.X[i] = X1[i];
    }

    int key1[] = {
        12, 31, 31, 31, 31, 31, 31, 31, 
        42, 45, 45, 20, 23, 23, 23, 23, 
        23, 23, 12, 12, 12, -7, 0, 23
    };

	for (int i = 0; i < 24; i++) {
		var24.key[i] = key1[i];
    }

    for (int i = 23; i > 0; i--) {
		var24.key[i] = var24.key[i] - var24.key[i - 1];
    }

    for (int i = 0 ; i < 8; i++) {
        var24.key[var24.L[i]] += var24.X[i];
        var24.key[var24.R[i]] -= var24.X[i];
    }
    
	for (int i = 1; i < 24; i++) {
		var24.key[i] += var24.key[i - 1];
    }

    int key2[] = {
        252, 352, 484, 470, 496, 487, 539, 585,
        447, 474, 577, 454, 466, 345, 344, 486,
        501, 423, 490, 375, 257, 203, 265, 125
    };

	for (int i = 0; i < 24; i++) {
		var23.key[i] = key2[i];
    }
    
    for (int i = 0; i < 24; i++) {
        var23.key[i] ^= var24.key[i];
    }

    for (int i = 0; i < 8; i++) {
        var23.X[i] = myInput.key[3 * i];
    }
    
    for (int i = 23; i > 0; i--) {
		var23.key[i] = var23.key[i] - var23.key[i - 1];
    }
    
    for (int i = 0; i < 8; i++) {
		var23.key[myInput.L[i]] -= var23.X[i];
		var23.key[myInput.R[i]] += var23.X[i];
    }
    
	for (int i = 1; i < 24; i++) {
		var23.key[i] = var23.key[i] + var23.key[i - 1];
    }
    
 //   for (int i = 0; i < 7; i++) {
 //       int var17 = myInput.L[i];
 //       int var19 = myInput.L[i + 1];
 //       int tmp = var17 ^ var19;
 //       if (tmp > 23) {
 //           tmp = 23;
 //       }      
 //       var25.L[i] = tmp;
 //   }
 //   var25.L[7] = 0;
 //   
	//for (int i = 0; i < 7; i++) {
	//	int var18 = myInput.R[i];
	//	int var20 = myInput.R[i + 1];
	//	int tmp = var18 ^ var20;
	//	if (tmp > 23) {
	//		tmp = 23;
	//	}
	//	var25.R[i] = tmp;
	//}
	//var25[7] = 23;
 //   
 //   for (int i = 0; i < 7; i++) {
	//	int var17 = myInput.X[i];
	//	int var19 = myInput.X[i + 1];
	//	int tmp = var17 ^ var19;
	//	var25.X[i] = tmp;
 //   }
 //   var25.X[7] = 12;


 //   //   var25(@exp.key[22])<+184><+1640> := var1<+8>
 //   int key3[] = {
 //       127, 111, 188, 174, 195, 128, 88, 121, 
 //       123, 103, 57, 123, 97, 74, 37, 59, 
 //       21, 47, 54, 28, 49, 55, 999, 125
 //   };
 //   key3[22] = myInput.key[8];
 //   
 //   for (int i = 0; i < 24; i++) {
	//	var25.key[i] = key3[i];
 //   }

 //   for (int i = 23; i > 0; i--) {
	//	var25.key[i] = var25.key[i] - var25.key[i - 1];
 //   }

	//for (int i = 0; i < 8; i++) {
 //       var25.key[var25.L[i]] -= var25.X[i];
	//	var25.key[var25.R[i]] += var25.X[i];
 //   }

 //   for (int i = 1; i < 24; i++) {
	//	var25.key[i] = var25.key[i] + var25.key[i - 1];
 //   }

    for (int i = 0; i < 24; i++) {
        if (myInput.key[i] != var23.key[i]) {
            printf("wrong");
        }
    }
    printf("right");

    return 0;
}

大概逻辑就是这样，然后直接丢进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
48
49
50
51
52
from z3 import *

v23key = [252, 352, 484, 470, 496, 487, 539, 585, 447, 474, 577, 454, 466, 345, 344, 486, 501, 423, 490, 375, 257, 203,
          265, 125]
s = Solver()
v22L = [0, 15, 2, 10, 6, 9, 1, 4]
v22R = [8, 23, 11, 20, 13, 21, 19, 17]
v22X = [11, -13, 17, -19, 23, -29, 31, -37]
v22 = [BitVec('v22[%d]' % i, 16) for i in range(24)]
for i in range(23, 0, -1):
    v22[i] -= v22[i - 1]
for i in range(8):
    v22[v22L[i]] += v22X[i]
    v22[v22R[i]] -= v22X[i]
for i in range(1, 24):
    v22[i] += v22[i - 1]

v24key = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
for i in range(24):
    v23key[i] ^= v24key[i]
    v23key[i] &= 0xffffffff
v23X = [v22[i * 3] for i in range(8)]
for i in range(23, 0, -1):
    v23key[i] -= v23key[i - 1]
for i in range(8):
    v23key[v22L[i]] -= v23X[i]
    v23key[v22R[i]] += v23X[i]
for i in range(1, 24):
    v23key[i] += v23key[i - 1]

for i in range(24):
    s.add(v23key[i] == v22[i])

if s.check() == sat:
    print("done")
    k = 0
    while s.check() == sat:
        condition = []
        m = s.model()
        print("[%d]" % k)
        for each in range(24):
            for x in m.decls():
                if str("v22[%d]" % each) in str(x):
                    print(chr(m[x].as_long()), end="")
        k += 1
        print()
        for i in range(24):
            condition.append(v22[i] != (m.evaluate(v22[i])))

        s.add(Or(condition))
else:
    print("error")

sctf{r5cbsumyqpjy0stc7u}

Digital_circuit_learning

题目提示了说是stm32，因此打开ida时选择ARM Little-endian架构。

在字符串窗口定位到关键函数

首先是输入以及对输入的校验

image-20230708232055929

第二个则是执行函数

image-20230708232238455

结合初始化函数

image-20230708232336132

对输入的变换函数

image-20230708232431449

结合以上函数可以看出，整体的逻辑如下

首先输入26长度的字符串，除去SCTF{}后进行变换

将变换后的数组塞入array数组的奇数位，而偶数位则塞入函数的地址

初始化完成后则是执行10轮的函数

首先初始化一个字符w，找到array对应输入的第i个字符并执行第i个函数

然后对w进行变换，总执行10轮，且每次执行之后会在结果的第i位留下函数标记

最后是判断函数

image-20230708232858320

可以看出执行的顺序是bdgfciejha

因此逆向的方式是

首先先用字符w生成出正确的输入，然后根据执行函数的顺序将其放入对应的位置，这样就得到了未加密的输入

其次，在依次执行10个函数

最后，逆向变换函数将10位的输入转换成原始输入

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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
def init_array(a1):
    return ((((a1 >> 6) & (a1 >> 2) & 1) == 0) | (2 * a1)) & 0xff


def b(arr):
    for i in range(len(arr)):
        arr[i] -= 1
    return arr


def c(arr):
    for i in range(len(arr)):
        arr[i] += 1
    return arr


def d(arr):
    for i in range(len(arr)):
        arr[i] ^= 0x35
    return arr


def e(arr):
    for i in range(len(arr)):
        arr[i] ^= arr[9 - i]
    return arr


def f(arr):
    for i in range(len(arr)):
        arr[i] ^= arr[(i + 1) % len(arr)]
    return arr


def g(arr):
    for i in range(len(arr)):
        arr[i] = ((arr[i] & 0xf) << 4) | ((arr[i] & 0xf0) >> 4)
    return arr


def h(arr):
    for i in range(len(arr)):
        arr[i] = ((arr[i] & 0x3) << 6) | ((arr[i] & 0xfc) >> 2)
    return arr


def ii(arr):
    for i in range(len(arr)):
        arr[i] = ((arr[i] & 0x7) << 5) | ((arr[i] & 0xf8) >> 3)
    return arr


def j(arr):
    for i in range(len(arr)):
        arr[i] ^= 0xf7
    return arr


array1 = [0] * 10
array1[0] = ord('w')
array = [0] * 10

for i in range(1, 10):
    array1[i] = init_array(array1[i - 1])

index = "bdgfciejha"
for i in range(len(index)):
    array[ord(index[i]) - ord('a')] = array1[i]


print(array)

array = b(array)
array = d(array)
array = g(array)
array = f(array)
array = c(array)
array = ii(array)
array = e(array)
array = j(array)
array = h(array)

out = [0] * 20

for i in range(0, 20, 2):
    if (array[i // 2] & 0xF) > 9:
        out[i + 1] = (array[i // 2] & 0xF) + ord('W')
    else:
        out[i + 1] = (array[i // 2] & 0xF) + ord('0')
    if (array[i // 2] >> 4) > 9:
        out[i] = (array[i // 2] >> 4) + ord('W')
    else:
        out[i] = (array[i // 2] >> 4) + ord('0')

print('STCF{', bytes(out), '}')

STCF{5149ac8b033d602bf6d3}