signal

IDA 载入分析，发现是VM

抄成python出来，与z3打组合技解

from z3 import *
s = Solver()
x = [BitVec(f"x{i}", 8) for i in range(15)]
vmIns = open('signal.exe', 'rb').read()[0x1e40:0x1e40+456]
Str = [0] * 1000
end = 114
v9 = 0
v4 = 0
v8 = 0
v7 = 0
v6 = 0
v5 = 0
while v9 < end:
    ins = vmIns[v9 * 4]
    if ins == 1:
        Str[v6 + 100] = v4
        v9 += 1
        v6 += 1
        v8 += 1
    elif ins == 2:
        v4 = vmIns[(v9 + 1) * 4] + Str[v8]
        v9 += 2
    elif ins == 3:
        v4 = Str[v8] - (vmIns[(v9 + 1) * 4] & 0xff)
        v9 += 2
    elif ins == 4:
        v4 = vmIns[(v9 + 1) * 4] ^ Str[v8]
        v9 += 2
    elif ins == 5:
        v4 = vmIns[(v9 + 1) * 4] * Str[v8]
        v9 += 2
    elif ins == 6:
        v9+=1
    elif ins == 7:
        print(Str[v7 + 100])
        s.add(Str[v7 + 100] == vmIns[(v9 + 1) * 4])
        v7 += 1
        v9 += 2
    elif ins == 8:
        Str[v5] = v4
        v9 += 1
        v5 += 1
    elif ins == 10:
        print("Read")
        for i, v in enumerate(x):
            # s.add(v > 0x20, v < 0x7f)
            Str[i] = v
        v9 += 1
    elif ins == 11:
        v4 = Str[v8] - 1
        v9 += 1
    elif ins == 12:
        v4 = Str[v8] + 1
        v9 += 1
    else:
        print(f"unknown insn {ins}")

print(s.check())
m = s.model()
for i in x:
    print(chr(m[i].as_long()), end ='')
'''
Read
(16 ^ x0) - 5
3*(32 ^ x1)
x2 - 2 - 1
4 ^ x3 + 1
3*x4 - 33
x5 - 1 - 1
(9 ^ x6) - 32
36 ^ 81 + x7
x8 + 1 - 1
37 + 2*x9
65 ^ 54 + x10
1*(32 + x11)
37 + 3*x12
(9 ^ x13) - 32
65 + x14 + 1
sat
757515121f3d478
'''

flag为flag{757515121f3d478}