XCTF Final: Spaceship

对 Xctf Final Re 题: SpaceShip 的复现

初步分析

​ 下载得到 ws 后缀的文件 ,谷歌查 ws 后缀文件

​ 不过这不对,根据文件内只有空格、换行符等以及比赛时队友找到 的资料,应该是 WhiteSpace 语言

​ 用工具可以把这个语言转成 python 和汇编形式

https://github.com/Smithers888/BlueSpace

调试

​ 转换得到的 python 文件可以直接运行,所以可以直接调试看逻辑

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
def stssstttsttn():
stack.append(0)

sys.stdout.flush()
try:
x = ord(sys.stdin.read(1))
except EOFError:
x = -1

#x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18 = Ints('x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18')

heap[stack.pop()] = x #调试时改动
stack.append(0)
stack.append(0)
stack[-1] = heap[stack[-1]]
stack.append(16777216)
x = stack.pop()
stack[-1] += x
stack.append(16777216)
x = stack.pop()
stack[-1] %= x
x = stack.pop()

.........

stack.append(0)
stack[-1] = heap[stack[-1]]
stack.append(1)
stack[-1] = heap[stack[-1]]
x = stack.pop()
stack[-1] -= x
try:
if stack.pop() < 0:
return sttsssttssstn
except Z3Exception: #异常
print(stack,heap)

​ 这部分读取并对输入进行运算,从下面这些数字猜测进行了方程的 运算

​ 根据学长的思路可以把输入都转换成 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
16777089: ((((((0 +
(2*((x10 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251 +
(10*((x8 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251 +
(3*((x11 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251, 16777086: 11, 16777085: ((((((0 +
(2*((x10 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251 +
(10*((x8 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251 +
(3*((x11 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251
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
#堆的数据
heap =

{

0: 10
1: 446
2: 0,
3: 16777074
4: 16777077
5: 16777076
6: 0

8: 2
9: 10
10: 10
11: 8
12: 3
13: 11
14: 1753
15: 7
16: 17
17: 6
18: 4
19: 8
20: 16
21: 2117
22: 4
23: 5
24: 3
25: 15
26: 6
27: 6
28: 1071
29: 3
30: 17
31: 5
32: 4
33: 2
34: 16
35: 1116
36: 10
37: 14
38: 4
39: 0
40: 10
41: 9
42: 2190
43: 9
44: 14
45: 4
46: 0
47: 4
48: 9
49: 1764
50: 2
51: 3
52: 1
53: 2
54: 3
55: 1
56: 617
57: 9
58: 14
59: 8
60: 0
61: 3
62: 9
63: 2193
64: 1
65: 17
66: 5
67: 4
68: 2
69: 16
70: 866
71: 8
72: 5
73: 2
74: 15
75: 8
76: 6
77: 1594
78: 5
79: 12
80: 10
81: 13
82: 2
83: 7
84: 1153
85: 10
86: 12
87: 5
88: 13
89: 8
90: 7
91: 1737
92: 5
93: 12
94: 9
95: 13
96: 9
97: 7
98: 1445
99: 4
100: 10
101: 7
102: 8
103: 7
104: 11
105: 2119
106: 5
107: 3
108: 2
109: 2
110: 5
111: 1
112: 1237
113: 9
114: 5
115: 8
116: 15
117: 4
118: 6
119: 1463
120: 7
121: 10
122: 8
123: 8
124: 4
125: 11
126: 2217
127: 6
128: 3
129: 10
130: 2
131: 1
132: 1
133: 1871
}

​ 对照着可以发现 18 个表达式的形式

exp

1
2
3
4
5
6
7
8
9
10
11
12
13
((((((0 +
(2*((x10 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251 +
(10*((x8 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251 +
(3*((x11 + 16777216)%16777216) + 16777216)%16777216 +
16777216)%
16777216)%
3251

​ 因为每个变量都在可见字符范围内,所以上面的表达式可以简化成

1
2*x10+10*x8+3*x11==
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
from z3 import *

heap = {0: 10, 1: 446, 2: 0, 3: 16777074, 4: 16777077, 5: 16777076, 6: 0,
8: 2, 9: 10, 10: 10, 11: 8, 12: 3, 13: 11, 14: 1753, 15: 7, 16: 17, 17: 6, 18: 4, 19: 8, 20: 16, 21: 2117, 22: 4, 23: 5, 24: 3, 25: 15, 26: 6, 27: 6, 28: 1071, 29: 3, 30: 17, 31: 5, 32: 4, 33: 2, 34: 16, 35: 1116, 36: 10, 37: 14, 38: 4, 39: 0, 40: 10, 41: 9, 42: 2190, 43: 9, 44: 14, 45: 4, 46: 0, 47: 4, 48: 9, 49: 1764, 50: 2, 51: 3, 52: 1, 53: 2, 54: 3, 55: 1, 56: 617, 57: 9, 58: 14, 59: 8, 60: 0, 61: 3, 62: 9, 63: 2193, 64: 1, 65: 17, 66: 5, 67: 4, 68: 2, 69: 16, 70: 866, 71: 8, 72: 5, 73: 2, 74: 15, 75: 8, 76: 6, 77: 1594, 78: 5, 79: 12, 80: 10, 81: 13, 82: 2, 83: 7, 84: 1153, 85: 10, 86: 12, 87: 5, 88: 13, 89: 8, 90: 7, 91: 1737, 92: 5, 93: 12, 94: 9, 95: 13, 96: 9, 97: 7, 98: 1445, 99: 4, 100: 10, 101: 7, 102: 8, 103: 7, 104: 11, 105: 2119, 106: 5, 107: 3, 108: 2, 109: 2,
110: 5, 111: 1, 112: 1237, 113: 9, 114: 5, 115: 8, 116: 15, 117: 4, 118: 6, 119: 1463, 120: 7, 121: 10, 122: 8, 123: 8, 124: 4, 125: 11, 126: 2217, 127: 6, 128: 3, 129: 10, 130: 2, 131: 1, 132: 1, 133: 1871}

s=Solver()
x=IntVector('x',18)
for i in range(8,7*18+8,7):
s.add(heap[i]*(x[heap[i+1]]) +heap[i+2]*(x[heap[i+3]]) +heap[i+4]*(x[heap[i+5]])==heap[i+6])

print(s.check())
print(s.model())
ans=s.model()
x10,x8,x11=Ints('x10 x8 x11')
[print(chr(int(str(ans[i]))),end='') for i in x]
#xctf{Wh1t3sym3x!?}

​ 复现得到 flag 后还在谷歌上找到了有人在赛时写了个类似 angr 的对 whitespace 自动求解的 库,有空再研究

https://github.com/umutoztunc/whitesymex

参考资料

作者

0wl

发布于

2021-06-02

更新于

2021-11-16

许可协议

评论