sudo kurl https//spacewar

游戏的逻辑是在一个25×25的区域内填写数字。

在play()函数中，首先会对我们的每次输入用isValid()进行检查。

isValid()，函数首先会初始化一个bool向量的表(存储0，1的数组)，然后获取board中的值判断是不是0。如果不是0那么获取这个值作为下标获取bool向量中的值判断是不是1，如果是1返回0，如果不是1，把值修改为1。继续进行判断。其实就是判断broad中某一特定的位置的元素是否已经存在。它的检查顺序是，先检查行，再检查列，最后分5x5的块进行检查。

那么逻辑就是检查行，列，块中是否有重复的数字。如果没有返回1，有的话返回0；

checkWin()检查了broad中是否有元素为0 ，如果没有0且isValid()检查也正确就赢得游戏。

很明显这就是一个数独游戏。查看broad的交叉引用就可以看到初始值在__static_initialization_and_destruction_0()中。拿下来用z3解。

解完后判断哪些值是要我们要输入的，用pwndbg把值输入，程序输出flag就行。

1
2
3
import ida_dbg
eax = ida_dbg.get_reg_val("eax")
print(",",eax,end="")
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
from z3 import *
from pwn import *

data =[0, 0, 0, 21, 0, 11, 0, 0, 3, 24, 9, 20, 23, 0, 7, 22, 0, 5, 18, 0, 15, 2, 16, 13, 0, 24, 4, 0, 20, 15, 0, 0, 5, 0, 16, 2, 25, 22, 0, 17, 6, 21, 0, 14, 0, 8, 10, 1, 19, 18, 0, 0, 10, 0, 5, 0, 21, 19, 22, 0, 3, 13, 1, 16, 0, 15, 4, 7, 23, 24, 12, 0, 14, 0, 0, 0, 0, 13, 6, 12, 14, 4, 1, 0, 0, 24, 18, 19, 5, 0, 0, 17, 0, 0, 0, 7, 22, 0, 9, 21, 0, 23, 19, 7, 0, 0, 6, 0, 0, 20, 15, 4, 0, 21, 0, 0, 0, 0, 16, 10, 24, 3, 0, 17, 5, 12, 15, 21, 0, 0, 0, 16, 6, 18, 5, 7, 0, 17, 3, 9, 14, 0, 4, 24, 22, 13, 0, 0, 0, 0, 14, 10, 11, 2, 24, 1, 25, 22, 20, 0, 0, 23, 6, 19, 0, 13, 5, 8, 12, 0, 17, 0, 7, 15, 9, 0, 0, 0, 0, 1, 24, 0, 3, 15, 10, 20, 8, 5, 0, 25, 9, 16, 19, 21, 0, 2, 6, 0, 12, 14, 0, 0, 5, 0, 3, 0, 23, 14, 8, 0, 0, 2, 15, 0, 12, 0, 7, 1, 17, 6, 22, 21, 4, 0, 19, 13, 0, 0, 4, 20, 0, 0, 0, 17, 0, 11, 16, 0, 0, 22, 0, 10, 18, 15, 23, 0, 25, 8, 1, 3, 20, 25, 7, 22, 0, 23, 0, 10, 1, 0, 0, 0, 0, 13, 4, 21, 0, 6, 19, 0, 3, 9, 15, 8, 0, 1, 24, 0, 0, 0, 4, 0, 20, 13, 0, 8, 0, 3, 0, 19, 16, 2, 12, 9, 5, 0, 14, 10, 25, 22, 0, 0, 0, 0, 0, 0, 0, 9, 24, 0, 25, 6, 0, 2, 16, 4, 8, 10, 0, 17, 18, 7, 21, 0, 1, 0, 8, 0, 10, 14, 16, 3, 25, 6, 0, 0, 7, 18, 9, 11, 0, 13, 0, 20, 0, 19, 24, 5, 0, 17, 17, 3, 0, 15, 9, 5, 0, 0, 11, 0, 0, 21, 0, 0, 23, 7, 0, 22, 0, 0, 20, 13, 12, 4, 6, 15, 0, 20, 11, 21, 10, 0, 0, 5, 22, 16, 0, 0, 8, 3, 24, 0, 13, 2, 19, 0, 0, 0, 0, 0, 0, 13, 8, 0, 19, 17, 0, 0, 0, 0, 0, 12, 7, 24, 6, 0, 15, 23, 22, 4, 14, 5, 9, 0, 0, 9, 1, 23, 14, 4, 0, 24, 0, 7, 8, 19, 0, 2, 0, 13, 17, 3, 20, 5, 0, 0, 15, 0, 16, 10, 10, 0, 2, 12, 0, 13, 18, 15, 0, 0, 17, 5, 0, 20, 21, 8, 1, 16, 0, 7, 0, 19, 0, 11, 0, 7, 5, 17, 24, 16, 20, 2, 11, 19, 3, 23, 0, 4, 15, 1, 18, 14, 0, 10, 0, 0, 8, 13, 21, 12, 0, 20, 9, 0, 7, 15, 22, 17, 10, 0, 12, 19, 0, 0, 24, 25, 0, 14, 4, 8, 16, 18, 2, 0, 0, 19, 2, 24, 8, 0, 0, 20, 7, 4, 0, 0, 0, 9, 0, 15, 5, 0, 21, 11, 16, 1, 0, 0, 14, 25, 0, 0, 25, 1, 0, 8, 5, 23, 14, 6, 4, 17, 16, 0, 2, 0, 20, 0, 13, 9, 10, 12, 24, 7, 15, 0, 0, 14, 0, 0, 0, 0, 0, 0, 2, 6, 10, 13, 0, 5, 12, 0, 24, 0, 0, 9, 11, 0, 3, 8, 6, 0, 15, 0, 13, 0, 0, 24, 0, 9, 1, 0, 8, 25, 0, 10, 18, 17, 0, 2, 0, 4, 19, 0, 23
    ] # ida断点读出的数据
table = [[0]*25 for _ in range(25)] # 把获取的表转成二维数组
index =0
for i in range(25):
    for j in range(25):
        table[i][j] = data[index]
        index += 1

# 创建z3求解器
s = Solver()
var=[[Int(f'a_{i}_{j}') for i in range(25)] for j in range(25)] #创建变量，给每一个位置创建一个变量

for i in range(25):
    for j in range(25):
        if table[i][j] == 0:  #为零
            s.add(1 <= var[i][j])  # 限制范围
            s.add(var[i][j] <= 25)
        else:
            s.add(var[i][j] == table[i][j])
for i in range(25): s.add(Distinct(var[i])) # 遍历每个行，设置每行数据不能重复
for i in range(25): s.add(Distinct([row[i] for row in var])) # 设置列不能重复
for i in range(0, 25, 5):
    for j in range(0, 25, 5):
        s.add(Distinct([var[i + k // 5][j + k % 5] for k in range(25)])) #设置每个5x5的块不能重复
# print(s.check())

m = s.model()
b = [[int(str(m[var[i][j]])) for j in range(25)] for i in range(25)] #创建新列表，把答案提取出来
# print(b)

context.terminal=["open-wsl.exe","-c"]# 以新wsl窗口运行
io = process(["./chall"]) # 用pwntools进行io输入，把结果输入

for i in range(25):
    for j in range(25):
        if table[i][j] == 0: #判断位置是否需要填入
            io.sendline(str(i + 1).encode())
            io.sendline(str(j + 1).encode())
            io.sendline(str(b[i][j]).encode())
io.sendline(str(-1).encode())
io.interactive()

队里大佬的脚本参考

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
a = [[0, 0, 0, 21, 0, 11, 0, 0, 3, 24, 9, 20, 23, 0, 7, 22, 0, 5, 18, 0, 15, 2, 16, 13, 0], [24, 4, 0, 20, 15, 0, 0, 5, 0, 16, 2, 25, 22, 0, 17, 6, 21, 0, 14, 0, 8, 10, 1, 19, 18], [0, 0, 10, 0, 5, 0, 21, 19, 22, 0, 3, 13, 1, 16, 0, 15, 4, 7, 23, 24, 12, 0, 14, 0, 0], [0, 0, 13, 6, 12, 14, 4, 1, 0, 0, 24, 18, 19, 5, 0, 0, 17, 0, 0, 0, 7, 22, 0, 9, 21], [0, 23, 19, 7, 0, 0, 6, 0, 0, 20, 15, 4, 0, 21, 0, 0, 0, 0, 16, 10, 24, 3, 0, 17, 5], [12, 15, 21, 0, 0, 0, 16, 6, 18, 5, 7, 0, 17, 3, 9, 14, 0, 4, 24, 22, 13, 0, 0, 0, 0], [14, 10, 11, 2, 24, 1, 25, 22, 20, 0, 0, 23, 6, 19, 0, 13, 5, 8, 12, 0, 17, 0, 7, 15, 9], [0, 0, 0, 0, 1, 24, 0, 3, 15, 10, 20, 8, 5, 0, 25, 9, 16, 19, 21, 0, 2, 6, 0, 12, 14], [0, 0, 5, 0, 3, 0, 23, 14, 8, 0, 0, 2, 15, 0, 12, 0, 7, 1, 17, 6, 22, 21, 4, 0, 19], [13, 0, 0, 4, 20, 0, 0, 0, 17, 0, 11, 16, 0, 0, 22, 0, 10, 18, 15, 23, 0, 25, 8, 1, 3], [20, 25, 7, 22, 0, 23, 0, 10, 1, 0, 0, 0, 0, 13, 4, 21, 0, 6, 19, 0, 3, 9, 15, 8, 0], [1, 24, 0, 0, 0, 4, 0, 20, 13, 0, 8, 0, 3, 0, 19, 16, 2, 12, 9, 5, 0, 14, 10, 25, 22], [0, 0, 0, 0, 0, 0, 0, 9, 24, 0, 25, 6, 0, 2, 16, 4, 8, 10, 0, 17, 18, 7, 21, 0, 1], [0, 8, 0, 10, 14, 16, 3, 25, 6, 0, 0, 7, 18, 9, 11, 0, 13, 0, 20, 0, 19, 24, 5, 0, 17], [17, 3, 0, 15, 9, 5, 0, 0, 11, 0, 0, 21, 0, 0, 23, 7, 0, 22, 0, 0, 20, 13, 12, 4, 6], [15, 0, 20, 11, 21, 10, 0, 0, 5, 22, 16, 0, 0, 8, 3, 24, 0, 13, 2, 19, 0, 0, 0, 0, 0], [0, 13, 8, 0, 19, 17, 0, 0, 0, 0, 0, 12, 7, 24, 6, 0, 15, 23, 22, 4, 14, 5, 9, 0, 0], [9, 1, 23, 14, 4, 0, 24, 0, 7, 8, 19, 0, 2, 0, 13, 17, 3, 20, 5, 0, 0, 15, 0, 16, 10], [10, 0, 2, 12, 0, 13, 18, 15, 0, 0, 17, 5, 0, 20, 21, 8, 1, 16, 0, 7, 0, 19, 0, 11, 0], [7, 5, 17, 24, 16, 20, 2, 11, 19, 3, 23, 0, 4, 15, 1, 18, 14, 0, 10, 0, 0, 8, 13, 21, 12], [0, 20, 9, 0, 7, 15, 22, 17, 10, 0, 12, 19, 0, 0, 24, 25, 0, 14, 4, 8, 16, 18, 2, 0, 0], [19, 2, 24, 8, 0, 0, 20, 7, 4, 0, 0, 0, 9, 0, 15, 5, 0, 21, 11, 16, 1, 0, 0, 14, 25], [0, 0, 25, 1, 0, 8, 5, 23, 14, 6, 4, 17, 16, 0, 2, 0, 20, 0, 13, 9, 10, 12, 24, 7, 15], [0, 0, 14, 0, 0, 0, 0, 0, 0, 2, 6, 10, 13, 0, 5, 12, 0, 24, 0, 0, 9, 11, 0, 3, 8], [6, 0, 15, 0, 13, 0, 0, 24, 0, 9, 1, 0, 8, 25, 0, 10, 18, 17, 0, 2, 0, 4, 19, 0, 23]]

from z3 import *
s = Solver()
x = [[Int(f"a_{i}_{j}") for j in range(25)] for i in range(25)]
for i in range(25):
    for j in range(25):
        if a[i][j] == 0:
            s.add(1 <= x[i][j])
            s.add(x[i][j] <= 25)
        else:
            s.add(x[i][j] == a[i][j])
for i in range(25): s.add(Distinct(x[i]))
for i in range(25): s.add(Distinct([row[i] for row in x]))
for i in range(0, 25, 5):
    for j in range(0, 25, 5):
        s.add(Distinct([x[i + k // 5][j + k % 5] for k in range(25)]))
print(s.check())

m = s.model()
b = [[int(str(m[x[i][j]])) for j in range(25)] for i in range(25)]

from pwn import *
io = process(["./chall"])
for i in range(25):
    for j in range(25):
        if a[i][j] == 0:
            io.sendline(str(i + 1).encode())
            io.sendline(str(j + 1).encode())
            io.sendline(str(b[i][j]).encode())
io.sendline(str(-1).encode())
io.interactive()

# TRX{H0w_0ft3n_d0_y0u_th1nk_4b0ut_th3_R0m4n_3mp1r3?!?:D}

vm

在sub_2589函数内有大概的逻辑，有一些RC4的加密特征。

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
file是我们的code文件
设定一个索引 index =0
switch(file):每一个case定义了一些关于s[]盒的不同类型的操作方法
每次进case会得到一个新的索引 index_tmp = index + 1;
switch(index_tmp)，根据index_tmp的值进行不同的对s[]的操作，每一类操作的值是差不多的，只有操作方法不一样
我们令file[index_tmp + 1] == f[1];  file[index_tmp + 2] == sf[2];
那么大概操作有
0 s[f[1] -8 ] op s[f[2] -8]
1 s[f[1]] op s[f[2]]
2 s[f[1]] op s[s[f[2] - 8]]
3 s[s[f[1] -8 ]] op s[f[2]]
4 s[s[f[1] -8 ]] op s[s[f[2] -8]]
5 s[f[1] -8 ] op f[2]
6 s[f[1] -8 ] op s[f[2]]
7 s[f[1] -8 ] op s[s[f[2] -8]]
8 s[f[1]] op f[2]
9 s[s[f[1] -8 ]] op f[2]
10 s[f[1]] op s[f[2] -8]
11 s[s[f[1] -8 ]] op s[f[2] -8]
每次操作完后会把index后移四字节，即每四字节就是一组操作。
case 5的操作稍微有些不同
0 s[f[1]-8] = ~s[f[2] -8]
1 s[f[1]] = ~s[f[2]]
4 s[s[f[1]-8]] = ~s[s[f[2] -8]]
每次操作完后index向后移动3字节,3字节为一组操作

case 8多了一个操作
12 s[f[1] -8] ^= s[f[2] + 256]

case 11对结果进行验证，index后移一个字节，可能是用来对其数据的。

动调看大概的逻辑

我们可以发现，首先执行的就是case 9的case8，也就是8 s[f[1]] = f[2]。查看s[]的值可以知道这里初始化了一个256的表。

然后执行

case 0的case5，也就是5 s[f[1] -8 ] += f[2]。

case 0 的case0，0 s[f[1] -8 ] += s[f[2] -8]

case 9 的case0，s[f[1] -8 ] = s[f[2] -8]

case9 的case6，6 s[f[1] -8 ] = s[f[2]]

case9 的case2，2 s[f[1]] = s[s[f[2] - 8]]

case9 的case11，11 s[s[f[1] -8 ]] = s[f[2] -8]

case9 的case6，6 s[f[1] -8 ] = s[f[2]]

回到最上面的case 0继续循环

根据rc4的流程来看上面就是用密钥打乱盒的过程，那么密钥是不会在s盒里的，所以密钥就是f[2]

后面的流程也是差不多的，如果我们对输入的数据下断点我们就会被定位到异或的位置，在case 8的case 12，也就是

12 s[f[1] -8] ^= s[f[2] + 256]，s[f[2] + 256]

因为这里加了256所以访问的数据超出了盒的范围从而访问到了我们的输入数据，动调也能看到我们的输入数据就在s[]盒的末尾。

然后就是case 10的case 5对数据进行比较，也就是

5 s[f[1] -8 ] == f[2]

再case 11检查结果，然后返回到case0 和case9的一些操作，再到上面的异或，再检比较数据，依次循环。所以f[2]就是密文。

RC4加密就是一个异或，我们在比较密文和异或的的地方下断点并附加一个python脚本（脚本1）读取寄存器的值。获取到数据后异或解密就行。

image-20250223203445748

image-20250223203511544

脚本1

1
2
3
4
5
6
7
8
9
10
import ida_dbg
ecx = ida_dbg.get_reg_val("ecx")
print(",",ecx,end="")
# 41, 171, 94, 48, 92, 61, 91, 58, 187, 37, 132, 101, 212, 82, 19, 183, 180, 99, 210, 69, 194, 35, 198, 104, 249, 119, 76, 162, 108, 46

import ida_dbg
al = ida_dbg.get_reg_val("al")
print(",",al,end="")
#125, 249, 6, 75, 14, 126, 111, 101, 138, 86, 219, 81, 139, 32, 32, 214, 216, 60, 191, 113, 177, 87, 245, 26, 137, 70, 127, 193, 95, 83

脚本2

1
2
3
4
5
6
7
8
9

m = [125, 249, 6, 75, 14, 126, 111, 101, 138, 86, 219, 81, 139, 32, 32, 214, 216, 60, 191, 113, 177, 87, 245, 26, 137, 70, 127, 193, 95, 83]
b =""
k = [41, 171, 94, 48, 92, 61, 91, 58, 187, 37, 132, 101, 212, 82, 19, 183, 180, 99, 210, 69, 194, 35, 198, 104, 249, 119, 76, 162, 108, 46]
for l,n in zip(m,k):
    c = chr(l^n)
    b+=c
print(b)
#TRX{RC4_1s_4_r3al_m4st3rp13c3}

LLL

这题是真的s。文件是standard ML语言文件，用smlnj运行，在运行时会自动显示变量和操作，可以用AI把函数名改一下会好看点。总的来说就是上面定义了一些操作，下面的lll变量中嵌套了大量的程序控制流来调用上面定义的逻辑。可以用自动化脚本提取操作，并用z3求解。不过这涉及到很多问题。而且不怎么实用，暂时先不分析了。可以参考TRX CTF 2025 LLL 写作 | yqroo — TRX CTF 2025 LLL Writeup | yqroo

不过在sml文件里加如下指令可以加深打印逻辑的深度以后可能用到。

1
2
Control.Print.printDepth := 300;
Control.Print.printLength := 300;