[Hard] Metagaming

1. Locating the huge list of all vm handlers

if constexpr (Insn.opcode == 0) {
    regs[Insn.op0] = Flag.at(Insn.op1);
} else if constexpr (Insn.opcode == 1) {
    regs[Insn.op0] = Insn.op1;
} else if constexpr (Insn.opcode == 2) {
    regs[Insn.op0] ^= Insn.op1;
} else if constexpr (Insn.opcode == 3) {
    regs[Insn.op0] ^= regs[Insn.op1];
} else if constexpr (Insn.opcode == 4) {
    regs[Insn.op0] |= Insn.op1;
} else if constexpr (Insn.opcode == 5) {
    regs[Insn.op0] |= regs[Insn.op1];
} else if constexpr (Insn.opcode == 6) {
    regs[Insn.op0] &= Insn.op1;
} else if constexpr (Insn.opcode == 7) {
    regs[Insn.op0] &= regs[Insn.op1];
...

1.1 Naming the handlers (0 = read flag, 1 = mov, 2 = xor_imm, 3 = xor_reg, etc..) 2. Getting the vm commands

program_t<flag, insn_t(12, 13, 10), insn_t(21, 0, 0), insn_t(0, 13, 13), insn_t(0, 14, 0), insn_t(15, 11, 12), insn_t(24, 14, 0), insn_t(5, 0, 14), insn_t(0, 14, 1), ...>;

3. Lifting to z3 (i cheated a bit and ignored all the junk payloads)

chunks = [0 for _ in range(15)]

for i in range(len(flag)):
    pos = i % 4
    cur_reg = (i - (i % 4)) // 4

    if pos == 0:
        chunks[cur_reg] = 0

    chunks[cur_reg] |= (flag[i] << (pos * 8))

for cmd in payload:
    opcode, op0, op1 = cmd
    if opcode == 2:
        chunks[op0] ^= BitVecVal(op1, 32)
    elif opcode == 8:
        chunks[op0] += BitVecVal(op1, 32)
    elif opcode == 10:
        chunks[op0] -= BitVecVal(op1, 32)
    elif opcode == 3:
        chunks[op0] ^= chunks[op1]

s.add(chunks[0] == 0x3ee88722)
s.add(chunks[1] == 0xecbdbe2)
s.add(chunks[2] == 0x60b843c4)
s.add(chunks[3] == 0x5da67c7)
s.add(chunks[4] == 0x171ef1e9)
s.add(chunks[5] == 0x52d5b3f7)
s.add(chunks[6] == 0x3ae718c0)
s.add(chunks[7] == 0x8b4aacc2)
s.add(chunks[8] == 0xe5cf78dd)

5. Profit

m = s.model()
fl = ''.join(map(chr, [m[x].as_long() for x in flag]))
assert fl == 'HTB{m4n_1_l0v4_cXX_TeMpl4t35_9fb60c17b0}'

3.1 Second option is to just revert the math operations

from numpy import uint32

s = [uint32(0) for i in range(15)]

s[9] = uint32(0x4a848edf) ^ 0x8f
s[8] = uint32(0xe5cf78dd) ^ s[9]
s[7] = uint32(0x8b4aacc2) ^ s[8]
s[6] = uint32(0x3ae718c0) ^ s[7]
s[5] = uint32(0x52d5b3f7) ^ s[6]
s[4] = uint32(0x171ef1e9) ^ s[5]
s[3] = uint32(0x5da67c7) ^ s[4]
s[2] = uint32(0x60b843c4) ^ s[3]
s[1] = uint32(0xecbdbe2) ^ s[2]
s[0] = uint32(0x3ee88722) ^ s[1]

instrs = INSTRUCTIONS.strip().split("\n")[::-1]
for i in instrs:

    op, dst, rhs = i.split(" ")

    is_imm = op.endswith("IMM")
    operation = op.split('_')[0]

    if dst == "14" or (not is_imm and (operation == "OR" and rhs == "14")):
        continue

    if int(dst) > 9 or not is_imm:
        continue

    if operation == "ADD":
        s[int(dst)] = uint32(s[int(dst)]) - uint32(rhs)
    elif operation == "XOR":
        s[int(dst)] = uint32(s[int(dst)]) ^ uint32(rhs)
    elif operation == "SUB":
        s[int(dst)] = uint32(s[int(dst)]) + uint32(rhs)

for v in s[:10]:
    print(bytes.fromhex(hex(v)[2:]))

print("".join([bytes.fromhex(hex(v)[2:]).decode()[::-1] for v in s[:10]]))