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就行。
import ida_dbg
eax = ida_dbg.get_reg_val("eax")
print(",",eax,end="")
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()
队里大佬的脚本参考
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的加密特征。
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）读取寄存器的值。获取到数据后异或解密就行。
脚本1
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
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}
队里大佬的脚本，参考。
code = open("./attachment/bytecode.bin", "rb").read()
mnemonic = ["ADD", "SUB", "MUL", "DIV", "MOD", "NOT", "OR", "AND", "XOR", "MOV", "TEST", "END"]
mnemonic = list(map(lambda x: x.rjust(4), mnemonic))
key = []
ct = []
pc = 0
while pc < len(code):
op = code[pc]
assert 0 <= op <= len(mnemonic)
instruction = f"NOP"
if op == 11:
instruction = f"{mnemonic[op]}"
pc += 1
elif op != 5: # NOT
typ = code[pc + 1]
x, y = code[pc + 2], code[pc + 3]
if typ == 0: instruction = f"{mnemonic[op]} s[{x-8}], s[{y-8}]"
if typ == 1: instruction = f"{mnemonic[op]} s[{x}], s[{y}]"
if typ == 2: instruction = f"{mnemonic[op]} s[{x}], s[s[{y-8}]]"
if typ == 3: instruction = f"{mnemonic[op]} s[s[{x-8}]], s[{y}]"
if typ == 4: instruction = f"{mnemonic[op]} s[s[{x-8}]], s[s[{y-8}]]"
if typ == 5: instruction = f"{mnemonic[op]} s[{x-8}], {y}"
if typ == 6: instruction = f"{mnemonic[op]} s[{x-8}], s[{y}]"
if typ == 7: instruction = f"{mnemonic[op]} s[{x-8}], s[s[{y-8}]]"
if typ == 8: instruction = f"{mnemonic[op]} s[{x}], {y}"
if typ == 9: instruction = f"{mnemonic[op]} s[s[{x-8}]], {y}"
if typ == 10: instruction = f"{mnemonic[op]} s[{x}], s[{y-8}]"
if typ == 11: instruction = f"{mnemonic[op]} s[s[{x-8}]], s[{y-8}]"
if typ == 12:
assert op == 8 # XOR
instruction = f"{mnemonic[op]} s[s[{x-8}]], flag[{y}]"
if instruction != "NOP": pc += 4
if op == 0 and typ == 5: key.append(y)
if op == 10: ct.append(y)
else:
typ = code[pc + 1]
x, y = code[pc + 2], code[pc + 3]
if typ == 0: instruction = f"{mnemonic[op]} s[{x-8}]"
if typ == 1: instruction = f"{mnemonic[op]} s[{x}]"
if typ == 4: instruction = f"{mnemonic[op]} s[s[{x-8}]]"
if instruction != "NOP": pc += 3
instruction = instruction.replace("s[-8]", "i")
instruction = instruction.replace("s[-7]", "j")
instruction = instruction.replace("s[-6]", "k")
instruction = instruction.replace("s[-5]", "x")
instruction = instruction.replace("s[-4]", "y")
instruction = instruction.replace("s[-3]", "z")
print(instruction)
assert instruction != "NOP", code[pc:pc+4].hex()
from Crypto.Cipher import ARC4
key = bytes(key[:256])
ct = bytes(ct)
print(ARC4.new(key).decrypt(ct))
# 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文件里加如下指令可以加深打印逻辑的深度以后可能用到。
Control.Print.printDepth := 300;
Control.Print.printLength := 300;