Cybertalents reverse engineering problems solutions

Nov. 23, 2020

I don’t present solutions for all problems, most of these are just some notes with high level ideas on how I solved them, I leave solving the problems as an exercise to the reader.

The Cybertalents reverse ctf had a couple of nice problems, I had two remaining problems one windows keylogger shit for which I was to lazy to write a program to decrypt the flag file since windows crypto api is not fun to be honest, well I googled how to use this windows bcrypt (not to be confused with the password hashing function, this is some Microsoft thing), and I find this 500 line code example, well I wouldn’t want to spend time on that 😂. And another word macro shit, which I had no experience in and I didn’t bother doing.

The only problem with this ctf, is that there a lot of recycled or straight reused problems, which maybe gave other players an advantage over me, since I don’t do problems on that site.

Solution for Curiosity

Simple VM, it uses 4 general purpose registers with a couple of instructions, mul, not, add, load immediate, load from register, syscall (does some read and write), and conditional jump instruction, many ways to reverse this, you could for example build a dis-assembler for the code and integrate it in binary ninja for example to see some nice CFG’s but that won’t be very useful for this problem since, control flow is only used once in the program, for me I chose to build an intel pin tool to print a log. I just run the program with the tool, and enter some random input, and then like figure out what the algorithm does, finally it’s trivial to solve using z3:

Here is my pintool:

#include "pin.H"
#include <fstream>
#include <stdio.h>
#include <iostream>
using namespace std;

KNOB<string> KnobOutputFile(KNOB_MODE_WRITEONCE, "pintool", "o", "pin.out",
			  "specify output file name");
ofstream outFile;
ADDRINT l, h;

void lolbro(CONTEXT* ctx) {
  PIN_REGISTER rax;
  PIN_GetContextRegval(ctx, REG_RAX, reinterpret_cast<UINT8 *>(&rax));

  int pc = rax.dword[0];

  unsigned int reg1, reg2, reg3, reg4;
  PIN_SafeCopy(& reg1, (void*)0x555555756488, sizeof(int));
  PIN_SafeCopy(& reg2, (void*)0x555555756484, sizeof(int));
  PIN_SafeCopy(& reg3, (void*)0x555555756482, sizeof(int));
  PIN_SafeCopy(& reg4, (void*)0x555555756486, sizeof(int));

  outFile << "PC: 0x" << hex << pc << " REG1: 0x" << hex << reg1 << " REG2: 0x" << hex << reg2 << " REG3: 0x" << hex << reg3 << " REG4: 0x" << hex << reg4 << endl;

}

void INS1(CONTEXT* ctx) {
  PIN_REGISTER rdx, rcx;
  PIN_GetContextRegval(ctx, REG_RCX, reinterpret_cast<UINT8 *>(&rcx)); // register offset
  PIN_GetContextRegval(ctx, REG_RDX, reinterpret_cast<UINT8 *>(&rdx)); // value

  outFile << "MEMSTORE: REG" << (int) ((rcx.dword[0] / 8) +1) << " = 0x" << hex << +rdx.byte[0] << endl;
}

int get_register_number_by_address(long long address) {
  switch (address)
    {
    case 0x555555756488:
      return 1;
    case 0x555555756486:
      return 4;
    case 0x555555756484:
      return 2;
    case 0x555555756482:
      return 3;
    default:
      std::cerr << "oy there's an error bro" << std::endl;
      exit(0xff);
    }


}

void INS2(CONTEXT* ctx) {
  PIN_REGISTER rdx, rcx;
  PIN_GetContextRegval(ctx, REG_RCX, reinterpret_cast<UINT8 *>(&rcx)); // store register offset
  PIN_GetContextRegval(ctx, REG_RDX, reinterpret_cast<UINT8 *>(&rdx)); // load register offset
  outFile << "REGSTORE: REG" << (int) ((rcx.dword[0] / 8) +1) << " = REG" << get_register_number_by_address(rdx.qword[0]) << endl;

}

void ADD(CONTEXT* ctx) {
  PIN_REGISTER rsi, rdx;
  PIN_GetContextRegval(ctx, REG_RSI, reinterpret_cast<UINT8 *>(&rsi)); // store register offset
  PIN_GetContextRegval(ctx, REG_RDX, reinterpret_cast<UINT8 *>(&rdx)); // memory value
  outFile << "ADD: REG" << (int) ((rsi.dword[0] / 8) +1) << " += " << "0x" << rdx.dword[0] << endl;
}

void NOT(CONTEXT* ctx) {
  PIN_REGISTER rax;
  PIN_GetContextRegval(ctx, REG_RAX, reinterpret_cast<UINT8 *>(&rax)); // register

  outFile << "NOT: REG" << +rax.byte[0] << " = ~REG" << +rax.byte[0] << endl;

}

void MUL(CONTEXT* ctx) {
  PIN_REGISTER rsi, rdx;
  PIN_GetContextRegval(ctx, REG_RSI, reinterpret_cast<UINT8 *>(&rsi));
  PIN_GetContextRegval(ctx, REG_RDX, reinterpret_cast<UINT8 *>(&rdx));
  outFile << "MUL: REG" << (int) ((rsi.dword[0] / 8) +1) << " *= " << "0x" << rdx.dword[0] << endl;
}

void INPUT(CONTEXT* ctx) {
  outFile << "  INPUT" << endl;
}

void OUTPUT(CONTEXT* ctx) {
  outFile << "  OUTPUT" << endl;
}
void XIT(CONTEXT* ctx) {
  outFile << "XIT" << endl;
}

void REG_ADD_1(CONTEXT* ctx ) {
  PIN_REGISTER rdx;
  PIN_GetContextRegval(ctx, REG_RDX, reinterpret_cast<UINT8 *>(&rdx));
  outFile << "REGADD: REG" << (int) ((rdx.dword[0] / 8) +1) << " += ";
}
void REG_ADD_2(CONTEXT* ctx ) {
  PIN_REGISTER rdx;
  PIN_GetContextRegval(ctx, REG_RDX, reinterpret_cast<UINT8 *>(&rdx));
  outFile << "REG" << (int) ((rdx.dword[0] / 8) +1) << endl;
}

VOID callback_instruction(INS ins, VOID *v) {
  if (INS_Address(ins) == 0x555555554CBD) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)lolbro, IARG_CONTEXT,
		 IARG_END);
  }

  if (INS_Address(ins) == 0x555555554914) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)INS1, IARG_CONTEXT,
		 IARG_END);
  }

  if (INS_Address(ins) == 0x55555555499C) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)INS2, IARG_CONTEXT,
		 IARG_END);
  }
  if (INS_Address(ins) == 0x555555554AC0) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)ADD, IARG_CONTEXT,
		 IARG_END);
  }

  if (INS_Address(ins) == 0x555555554B9E) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)NOT, IARG_CONTEXT,
		 IARG_END);
  }
  if (INS_Address(ins) == 0x555555554B58) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)MUL, IARG_CONTEXT,
		 IARG_END);
  }
  if (INS_Address(ins) == 0x555555554866) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)INPUT, IARG_CONTEXT,
		 IARG_END);
  }
  if (INS_Address(ins) == 0x555555554874) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)OUTPUT, IARG_CONTEXT,
		 IARG_END);
  }
  if (INS_Address(ins) == 0x555555554893) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)XIT, IARG_CONTEXT,
		 IARG_END);
  }

  if (INS_Address(ins) == 0x5555555549FA) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)REG_ADD_1, IARG_CONTEXT,
		 IARG_END);

  }

  if (INS_Address(ins) == 0x555555554A1D) {
    INS_InsertCall(ins, IPOINT_BEFORE, (AFUNPTR)REG_ADD_2, IARG_CONTEXT,
		 IARG_END);
  }


}

VOID fini(INT32 code, VOID *v) { outFile.close(); }

int main(int argc, char *argv[]) {
  if (PIN_Init(argc, argv)) {
    perror("init");
    return 0;
  }
  outFile.open(KnobOutputFile.Value().c_str());
  INS_AddInstrumentFunction(callback_instruction, 0);
  PIN_AddFiniFunction(fini, 0);
  PIN_StartProgram();
  return 0;
}

I just run the program with this tool, and then like solve the constraints with a z3 script:

import z3
s = z3.Solver()
x = [z3.BitVec("x_{}".format(i), 8) for i in range(22)]
for c in x:
    s.add(z3.And(
	  c >= 0x20,
	  c < 0x7f))


""" PC: 0x173 REG1: 0x46 REG2: 0xff20 REG3: 0xff20002d REG4: 0x460000
MEMSTORE: REG3 = 0x74
PC: 0x176 REG1: 0x46 REG2: 0xff20 REG3: 0xff200074 REG4: 0x460000
ADD: REG3 += 0x45
PC: 0x179 REG1: 0x46 REG2: 0xff20 REG3: 0xff2000b9 REG4: 0x460000
REGADD: REG1 += REG3
PC: 0x17a REG1: 0xff REG2: 0xff20 REG3: 0xff2000b9 REG4: 0xff0000
NOT: REG0 = ~REG0
PC: 0x17b REG1: 0xff00 REG2: 0xff20 REG3: 0xff2000b9 REG4: 0xff000000
ADD: REG1 += 0x110
PC: 0x17e REG1: 0x10 REG2: 0xff20 REG3: 0xff2000b9 REG4: 0x100000
REGADD: REG4 += REG1
PC: 0x17f REG1: 0x10 REG2: 0x10ff20 REG3: 0xff2000b9 REG4: 0x100010
MEMSTORE: REG1 = 0x0
PC: 0x182 REG1: 0x0 REG2: 0x10ff20 REG3: 0xff2000b9 REG4: 0x10
"""

s.add((~(x[0] + 0x74 + 0x45))+0x110 == 0)

#FLAG{VGHIJKLMNOPQRSTUVWXYZ[

""" PC: 0x183 REG1: 0x47 REG2: 0xff20 REG3: 0xff2000b9 REG4: 0x470000
MUL: REG1 *= 0x3c
PC: 0x186 REG1: 0x10a4 REG2: 0xff20 REG3: 0xff2000b9 REG4: 0x10a40000
MEMSTORE: REG3 = 0x59
PC: 0x189 REG1: 0x10a4 REG2: 0xff20 REG3: 0xff200059 REG4: 0x10a40000
REGADD: REG1 += REG3
PC: 0x18a REG1: 0x10fd REG2: 0xff20 REG3: 0xff200059 REG4: 0x10fd0000
ADD: REG1 += 0xed9b
PC: 0x18d REG1: 0xfe98 REG2: 0xff20 REG3: 0xff200059 REG4: 0xfe980000
REGADD: REG4 += REG1
PC: 0x18e REG1: 0xfe98 REG2: 0xfe98ff20 REG3: 0xff200059 REG4: 0xfe98fe98
MEMSTORE: REG1 = 0x0
PC: 0x191 REG1: 0x0 REG2: 0xfe98ff20 REG3: 0xff200059 REG4: 0xfe98
"""
s.add(x[1] * 0x3c + 0x59 + 0xed9b == 0)

""" PC: 0x192 REG1: 0x48 REG2: 0xfe98ff20 REG3: 0xff200059 REG4: 0x48fe98
MUL: REG1 *= 0x30
PC: 0x195 REG1: 0xd80 REG2: 0xfe98ff20 REG3: 0xff200059 REG4: 0xd80fe98
MEMSTORE: REG3 = 0x3b
PC: 0x198 REG1: 0xd80 REG2: 0xfe98ff20 REG3: 0xff20003b REG4: 0xd80fe98
REGADD: REG1 += REG3
PC: 0x199 REG1: 0xdbb REG2: 0xfe98ff20 REG3: 0xff20003b REG4: 0xdbbfe98
ADD: REG1 += 0xedf5
PC: 0x19c REG1: 0xfbb0 REG2: 0xfe98ff20 REG3: 0xff20003b REG4: 0xfbb0fe98
REGADD: REG4 += REG1
PC: 0x19d REG1: 0xfbb0 REG2: 0xfa48ff20 REG3: 0xff20003b REG4: 0xfbb0fa48
MEMSTORE: REG1 = 0x0
PC: 0x1a0 REG1: 0x0 REG2: 0xfa48ff20 REG3: 0xff20003b REG4: 0xfa48
"""
s.add(x[2] * 0x30 + 0x3b + 0xf5 == 0)

""" PC: 0x1a1 REG1: 0x49 REG2: 0xfa48ff20 REG3: 0xff20003b REG4: 0x49fa48
MUL: REG1 *= 0x9
PC: 0x1a4 REG1: 0x291 REG2: 0xfa48ff20 REG3: 0xff20003b REG4: 0x291fa48
MEMSTORE: REG3 = 0x21
PC: 0x1a7 REG1: 0x291 REG2: 0xfa48ff20 REG3: 0xff200021 REG4: 0x291fa48
REGADD: REG1 += REG3
PC: 0x1a8 REG1: 0x2b2 REG2: 0xfa48ff20 REG3: 0xff200021 REG4: 0x2b2fa48
ADD: REG1 += 0xfd96
PC: 0x1ab REG1: 0x48 REG2: 0xfa48ff20 REG3: 0xff200021 REG4: 0x48fa48
REGADD: REG4 += REG1
PC: 0x1ac REG1: 0x48 REG2: 0xfa90ff20 REG3: 0xff200021 REG4: 0x48fa90
MEMSTORE: REG1 = 0x0
PC: 0x1af REG1: 0x0 REG2: 0xfa90ff20 REG3: 0xff200021 REG4: 0xfa90
"""
s.add(x[3] * 0x9 + 0x21 + 0x96 == 0)

""" PC: 0x1b0 REG1: 0x4a REG2: 0xfa90ff20 REG3: 0xff200021 REG4: 0x4afa90
MEMSTORE: REG3 = 0x92
PC: 0x1b3 REG1: 0x4a REG2: 0xfa90ff20 REG3: 0xff20ff92 REG4: 0x4afa90
REGADD: REG1 += REG3
PC: 0x1b4 REG1: 0xffdc REG2: 0xfa90ff20 REG3: 0xff20ff92 REG4: 0xffdcfa90
REGADD: REG4 += REG1
PC: 0x1b5 REG1: 0xffdc REG2: 0xfa6cff20 REG3: 0xff20ff92 REG4: 0xffdcfa6c
MEMSTORE: REG1 = 0x0
PC: 0x1b8 REG1: 0x0 REG2: 0xfa6cff20 REG3: 0xff20ff92 REG4: 0xfa6c
"""
s.add(x[4] + 0x92 == 0)

""" PC: 0x1b9 REG1: 0x4b REG2: 0xfa6cff20 REG3: 0xff20ff92 REG4: 0x4bfa6c
MEMSTORE: REG3 = 0x9f
PC: 0x1bc REG1: 0x4b REG2: 0xfa6cff20 REG3: 0xff20ff9f REG4: 0x4bfa6c
REGADD: REG1 += REG3
PC: 0x1bd REG1: 0xffea REG2: 0xfa6cff20 REG3: 0xff20ff9f REG4: 0xffeafa6c
REGADD: REG4 += REG1
PC: 0x1be REG1: 0xffea REG2: 0xfa56ff20 REG3: 0xff20ff9f REG4: 0xffeafa56
MEMSTORE: REG1 = 0x0
PC: 0x1c1 REG1: 0x0 REG2: 0xfa56ff20 REG3: 0xff20ff9f REG4: 0xfa56"""

s.add(x[5] + 0x9f == 0)

""" PC: 0x1c2 REG1: 0x4c REG2: 0xfa56ff20 REG3: 0xff20ff9f REG4: 0x4cfa56
MEMSTORE: REG3 = 0x6a
PC: 0x1c5 REG1: 0x4c REG2: 0xfa56ff20 REG3: 0xff20006a REG4: 0x4cfa56
ADD: REG3 += 0x38
PC: 0x1c8 REG1: 0x4c REG2: 0xfa56ff20 REG3: 0xff2000a2 REG4: 0x4cfa56
REGADD: REG1 += REG3
PC: 0x1c9 REG1: 0xee REG2: 0xfa56ff20 REG3: 0xff2000a2 REG4: 0xeefa56
NOT: REG0 = ~REG0
PC: 0x1ca REG1: 0xff11 REG2: 0xfa56ff20 REG3: 0xff2000a2 REG4: 0xff11fa56
ADD: REG1 += 0x10f
PC: 0x1cd REG1: 0x20 REG2: 0xfa56ff20 REG3: 0xff2000a2 REG4: 0x20fa56
REGADD: REG4 += REG1
PC: 0x1ce REG1: 0x20 REG2: 0xfa76ff20 REG3: 0xff2000a2 REG4: 0x20fa76
MEMSTORE: REG1 = 0x0
PC: 0x1d1 REG1: 0x0 REG2: 0xfa76ff20 REG3: 0xff2000a2 REG4: 0xfa76"""

s.add(~(0x6a + 0x38 + x[6]) + 0x10f == 0)

""" PC: 0x1d2 REG1: 0x4d REG2: 0xfa76ff20 REG3: 0xff2000a2 REG4: 0x4dfa76
MEMSTORE: REG3 = 0x87
PC: 0x1d5 REG1: 0x4d REG2: 0xfa76ff20 REG3: 0xff20ff87 REG4: 0x4dfa76
REGADD: REG1 += REG3
PC: 0x1d6 REG1: 0xffd4 REG2: 0xfa76ff20 REG3: 0xff20ff87 REG4: 0xffd4fa76
REGADD: REG4 += REG1
PC: 0x1d7 REG1: 0xffd4 REG2: 0xfa4aff20 REG3: 0xff20ff87 REG4: 0xffd4fa4a
MEMSTORE: REG1 = 0x0
PC: 0x1da REG1: 0x0 REG2: 0xfa4aff20 REG3: 0xff20ff87 REG4: 0xfa4a"""

s.add(x[7] + 0x87 == 0)

""" PC: 0x1db REG1: 0x4e REG2: 0xfa4aff20 REG3: 0xff20ff87 REG4: 0x4efa4a
MEMSTORE: REG3 = 0x8d
PC: 0x1de REG1: 0x4e REG2: 0xfa4aff20 REG3: 0xff20ff8d REG4: 0x4efa4a
REGADD: REG1 += REG3
PC: 0x1df REG1: 0xffdb REG2: 0xfa4aff20 REG3: 0xff20ff8d REG4: 0xffdbfa4a
REGADD: REG4 += REG1
PC: 0x1e0 REG1: 0xffdb REG2: 0xfa25ff20 REG3: 0xff20ff8d REG4: 0xffdbfa25
MEMSTORE: REG1 = 0x0
PC: 0x1e3 REG1: 0x0 REG2: 0xfa25ff20 REG3: 0xff20ff8d REG4: 0xfa25"""
s.add(x[8] + 0x8d == 0)

""" PC: 0x1e4 REG1: 0x4f REG2: 0xfa25ff20 REG3: 0xff20ff8d REG4: 0x4ffa25
MEMSTORE: REG3 = 0x38
PC: 0x1e7 REG1: 0x4f REG2: 0xfa25ff20 REG3: 0xff200038 REG4: 0x4ffa25
ADD: REG3 += 0x4f
PC: 0x1ea REG1: 0x4f REG2: 0xfa25ff20 REG3: 0xff200087 REG4: 0x4ffa25
REGADD: REG1 += REG3
PC: 0x1eb REG1: 0xd6 REG2: 0xfa25ff20 REG3: 0xff200087 REG4: 0xd6fa25
NOT: REG0 = ~REG0
PC: 0x1ec REG1: 0xff29 REG2: 0xfa25ff20 REG3: 0xff200087 REG4: 0xff29fa25
ADD: REG1 += 0xf1
PC: 0x1ef REG1: 0x1a REG2: 0xfa25ff20 REG3: 0xff200087 REG4: 0x1afa25
REGADD: REG4 += REG1
PC: 0x1f0 REG1: 0x1a REG2: 0xfa3fff20 REG3: 0xff200087 REG4: 0x1afa3f
MEMSTORE: REG1 = 0x0
PC: 0x1f3 REG1: 0x0 REG2: 0xfa3fff20 REG3: 0xff200087 REG4: 0xfa3f"""
s.add(~(x[9] + 0x38 + 0x4f) + 0xf1 == 0)

""" PC: 0x1f4 REG1: 0x50 REG2: 0xfa3fff20 REG3: 0xff200087 REG4: 0x50fa3f
MEMSTORE: REG3 = 0x60
PC: 0x1f7 REG1: 0x50 REG2: 0xfa3fff20 REG3: 0xff200060 REG4: 0x50fa3f
ADD: REG3 += 0x61
PC: 0x1fa REG1: 0x50 REG2: 0xfa3fff20 REG3: 0xff2000c1 REG4: 0x50fa3f
REGADD: REG1 += REG3
PC: 0x1fb REG1: 0x111 REG2: 0xfa3fff20 REG3: 0xff2000c1 REG4: 0x111fa3f
NOT: REG0 = ~REG0
PC: 0x1fc REG1: 0xfeee REG2: 0xfa3fff20 REG3: 0xff2000c1 REG4: 0xfeeefa3f
ADD: REG1 += 0x135
PC: 0x1ff REG1: 0x23 REG2: 0xfa3fff20 REG3: 0xff2000c1 REG4: 0x23fa3f
REGADD: REG4 += REG1
PC: 0x200 REG1: 0x23 REG2: 0xfa62ff20 REG3: 0xff2000c1 REG4: 0x23fa62
MEMSTORE: REG1 = 0x0
PC: 0x203 REG1: 0x0 REG2: 0xfa62ff20 REG3: 0xff2000c1 REG4: 0xfa62"""
s.add( ~(x[10] + 0x60 + 0x61) + 0x135 == 0)

""" PC: 0x204 REG1: 0x51 REG2: 0xfa62ff20 REG3: 0xff2000c1 REG4: 0x51fa62
MEMSTORE: REG3 = 0x5b
PC: 0x207 REG1: 0x51 REG2: 0xfa62ff20 REG3: 0xff20005b REG4: 0x51fa62
ADD: REG3 += 0x5e
PC: 0x20a REG1: 0x51 REG2: 0xfa62ff20 REG3: 0xff2000b9 REG4: 0x51fa62
REGADD: REG1 += REG3
PC: 0x20b REG1: 0x10a REG2: 0xfa62ff20 REG3: 0xff2000b9 REG4: 0x10afa62
NOT: REG0 = ~REG0
PC: 0x20c REG1: 0xfef5 REG2: 0xfa62ff20 REG3: 0xff2000b9 REG4: 0xfef5fa62
ADD: REG1 += 0x119
PC: 0x20f REG1: 0xe REG2: 0xfa62ff20 REG3: 0xff2000b9 REG4: 0xefa62
REGADD: REG4 += REG1
PC: 0x210 REG1: 0xe REG2: 0xfa70ff20 REG3: 0xff2000b9 REG4: 0xefa70
MEMSTORE: REG1 = 0x0
PC: 0x213 REG1: 0x0 REG2: 0xfa70ff20 REG3: 0xff2000b9 REG4: 0xfa70"""
s.add( ~(x[11] + 0x5b + 0x5e) + 0x119 == 0)

""" PC: 0x214 REG1: 0x52 REG2: 0xfa70ff20 REG3: 0xff2000b9 REG4: 0x52fa70
MEMSTORE: REG3 = 0x48
PC: 0x217 REG1: 0x52 REG2: 0xfa70ff20 REG3: 0xff200048 REG4: 0x52fa70
ADD: REG3 += 0x32
PC: 0x21a REG1: 0x52 REG2: 0xfa70ff20 REG3: 0xff20007a REG4: 0x52fa70
REGADD: REG1 += REG3
PC: 0x21b REG1: 0xcc REG2: 0xfa70ff20 REG3: 0xff20007a REG4: 0xccfa70
NOT: REG0 = ~REG0
PC: 0x21c REG1: 0xff33 REG2: 0xfa70ff20 REG3: 0xff20007a REG4: 0xff33fa70
ADD: REG1 += 0xe4
PC: 0x21f REG1: 0x17 REG2: 0xfa70ff20 REG3: 0xff20007a REG4: 0x17fa70
REGADD: REG4 += REG1
PC: 0x220 REG1: 0x17 REG2: 0xfa87ff20 REG3: 0xff20007a REG4: 0x17fa87
MEMSTORE: REG1 = 0x0
PC: 0x223 REG1: 0x0 REG2: 0xfa87ff20 REG3: 0xff20007a REG4: 0xfa87"""
s.add( ~(x[12] + 0x48 + 0x32) + 0xe4 == 0)

""" PC: 0x224 REG1: 0x53 REG2: 0xfa87ff20 REG3: 0xff20007a REG4: 0x53fa87
MEMSTORE: REG3 = 0x8d
PC: 0x227 REG1: 0x53 REG2: 0xfa87ff20 REG3: 0xff20ff8d REG4: 0x53fa87
REGADD: REG1 += REG3
PC: 0x228 REG1: 0xffe0 REG2: 0xfa87ff20 REG3: 0xff20ff8d REG4: 0xffe0fa87
REGADD: REG4 += REG1
PC: 0x229 REG1: 0xffe0 REG2: 0xfa67ff20 REG3: 0xff20ff8d REG4: 0xffe0fa67
MEMSTORE: REG1 = 0x0
PC: 0x22c REG1: 0x0 REG2: 0xfa67ff20 REG3: 0xff20ff8d REG4: 0xfa67"""
s.add( x[13] + 0x8d  == 0)

"""PC: 0x22d REG1: 0x54 REG2: 0xfa67ff20 REG3: 0xff20ff8d REG4: 0x54fa67
MEMSTORE: REG3 = 0x28
PC: 0x230 REG1: 0x54 REG2: 0xfa67ff20 REG3: 0xff200028 REG4: 0x54fa67
ADD: REG3 += 0x58
PC: 0x233 REG1: 0x54 REG2: 0xfa67ff20 REG3: 0xff200080 REG4: 0x54fa67
REGADD: REG1 += REG3
PC: 0x234 REG1: 0xd4 REG2: 0xfa67ff20 REG3: 0xff200080 REG4: 0xd4fa67
NOT: REG0 = ~REG0
PC: 0x235 REG1: 0xff2b REG2: 0xfa67ff20 REG3: 0xff200080 REG4: 0xff2bfa67
ADD: REG1 += 0xe0
PC: 0x238 REG1: 0xb REG2: 0xfa67ff20 REG3: 0xff200080 REG4: 0xbfa67
REGADD: REG4 += REG1
PC: 0x239 REG1: 0xb REG2: 0xfa72ff20 REG3: 0xff200080 REG4: 0xbfa72
MEMSTORE: REG1 = 0x0
PC: 0x23c REG1: 0x0 REG2: 0xfa72ff20 REG3: 0xff200080 REG4: 0xfa72"""
s.add(~(x[14] + 0x28 + 0x58) + 0xe0 == 0)

"""PC: 0x23d REG1: 0x55 REG2: 0xfa72ff20 REG3: 0xff200080 REG4: 0x55fa72
MEMSTORE: REG3 = 0x50
PC: 0x240 REG1: 0x55 REG2: 0xfa72ff20 REG3: 0xff200050 REG4: 0x55fa72
ADD: REG3 += 0x74
PC: 0x243 REG1: 0x55 REG2: 0xfa72ff20 REG3: 0xff2000c4 REG4: 0x55fa72
REGADD: REG1 += REG3
PC: 0x244 REG1: 0x119 REG2: 0xfa72ff20 REG3: 0xff2000c4 REG4: 0x119fa72
NOT: REG0 = ~REG0
PC: 0x245 REG1: 0xfee6 REG2: 0xfa72ff20 REG3: 0xff2000c4 REG4: 0xfee6fa72
ADD: REG1 += 0x126
PC: 0x248 REG1: 0xc REG2: 0xfa72ff20 REG3: 0xff2000c4 REG4: 0xcfa72
REGADD: REG4 += REG1
PC: 0x249 REG1: 0xc REG2: 0xfa7eff20 REG3: 0xff2000c4 REG4: 0xcfa7e
MEMSTORE: REG1 = 0x0
PC: 0x24c REG1: 0x0 REG2: 0xfa7eff20 REG3: 0xff2000c4 REG4: 0xfa7e"""
s.add(~(x[15] + 0x50 + 0x74) + 0x126 == 0)

""" PC: 0x24d REG1: 0x56 REG2: 0xfa7eff20 REG3: 0xff2000c4 REG4: 0x56fa7e
MEMSTORE: REG3 = 0x26
PC: 0x250 REG1: 0x56 REG2: 0xfa7eff20 REG3: 0xff200026 REG4: 0x56fa7e
ADD: REG3 += 0x3e
PC: 0x253 REG1: 0x56 REG2: 0xfa7eff20 REG3: 0xff200064 REG4: 0x56fa7e
REGADD: REG1 += REG3
PC: 0x254 REG1: 0xba REG2: 0xfa7eff20 REG3: 0xff200064 REG4: 0xbafa7e
NOT: REG0 = ~REG0
PC: 0x255 REG1: 0xff45 REG2: 0xfa7eff20 REG3: 0xff200064 REG4: 0xff45fa7e
ADD: REG1 += 0xd2
PC: 0x258 REG1: 0x17 REG2: 0xfa7eff20 REG3: 0xff200064 REG4: 0x17fa7e
REGADD: REG4 += REG1
PC: 0x259 REG1: 0x17 REG2: 0xfa95ff20 REG3: 0xff200064 REG4: 0x17fa95
MEMSTORE: REG1 = 0x0
PC: 0x25c REG1: 0x0 REG2: 0xfa95ff20 REG3: 0xff200064 REG4: 0xfa95"""
s.add( ~(x[16] + 0x26 + 0x3e) + 0xd2 == 0)

""" PC: 0x25d REG1: 0x57 REG2: 0xfa95ff20 REG3: 0xff200064 REG4: 0x57fa95
MEMSTORE: REG3 = 0x5e
PC: 0x260 REG1: 0x57 REG2: 0xfa95ff20 REG3: 0xff20005e REG4: 0x57fa95
ADD: REG3 += 0x6a
PC: 0x263 REG1: 0x57 REG2: 0xfa95ff20 REG3: 0xff2000c8 REG4: 0x57fa95
REGADD: REG1 += REG3
PC: 0x264 REG1: 0x11f REG2: 0xfa95ff20 REG3: 0xff2000c8 REG4: 0x11ffa95
NOT: REG0 = ~REG0
PC: 0x265 REG1: 0xfee0 REG2: 0xfa95ff20 REG3: 0xff2000c8 REG4: 0xfee0fa95
ADD: REG1 += 0x12a
PC: 0x268 REG1: 0xa REG2: 0xfa95ff20 REG3: 0xff2000c8 REG4: 0xafa95
REGADD: REG4 += REG1
PC: 0x269 REG1: 0xa REG2: 0xfa9fff20 REG3: 0xff2000c8 REG4: 0xafa9f
MEMSTORE: REG1 = 0x0
PC: 0x26c REG1: 0x0 REG2: 0xfa9fff20 REG3: 0xff2000c8 REG4: 0xfa9f"""
s.add( ~(x[17] + 0x5e + 0x6a) + 0x12a == 0)

""" PC: 0x26d REG1: 0x58 REG2: 0xfa9fff20 REG3: 0xff2000c8 REG4: 0x58fa9f
MEMSTORE: REG3 = 0x6d
PC: 0x270 REG1: 0x58 REG2: 0xfa9fff20 REG3: 0xff20006d REG4: 0x58fa9f
ADD: REG3 += 0x2a
PC: 0x273 REG1: 0x58 REG2: 0xfa9fff20 REG3: 0xff200097 REG4: 0x58fa9f
REGADD: REG1 += REG3
PC: 0x274 REG1: 0xef REG2: 0xfa9fff20 REG3: 0xff200097 REG4: 0xeffa9f
NOT: REG0 = ~REG0
PC: 0x275 REG1: 0xff10 REG2: 0xfa9fff20 REG3: 0xff200097 REG4: 0xff10fa9f
ADD: REG1 += 0x112
PC: 0x278 REG1: 0x22 REG2: 0xfa9fff20 REG3: 0xff200097 REG4: 0x22fa9f
REGADD: REG4 += REG1
PC: 0x279 REG1: 0x22 REG2: 0xfac1ff20 REG3: 0xff200097 REG4: 0x22fac1
MEMSTORE: REG1 = 0x0
PC: 0x27c REG1: 0x0 REG2: 0xfac1ff20 REG3: 0xff200097 REG4: 0xfac1"""
s.add( ~(x[18] + 0x6d + 0x2a) + 0x112 == 0)

""" PC: 0x27d REG1: 0x59 REG2: 0xfac1ff20 REG3: 0xff200097 REG4: 0x59fac1
MEMSTORE: REG3 = 0x97
PC: 0x280 REG1: 0x59 REG2: 0xfac1ff20 REG3: 0xff20ff97 REG4: 0x59fac1
REGADD: REG1 += REG3
PC: 0x281 REG1: 0xfff0 REG2: 0xfac1ff20 REG3: 0xff20ff97 REG4: 0xfff0fac1
REGADD: REG4 += REG1
PC: 0x282 REG1: 0xfff0 REG2: 0xfab1ff20 REG3: 0xff20ff97 REG4: 0xfff0fab1
MEMSTORE: REG1 = 0x0
PC: 0x285 REG1: 0x0 REG2: 0xfab1ff20 REG3: 0xff20ff97 REG4: 0xfab1"""
s.add( x[19] + 0x97 == 0 )

""" PC: 0x286 REG1: 0x5a REG2: 0xfab1ff20 REG3: 0xff20ff97 REG4: 0x5afab1
MEMSTORE: REG3 = 0x92
PC: 0x289 REG1: 0x5a REG2: 0xfab1ff20 REG3: 0xff20ff92 REG4: 0x5afab1
REGADD: REG1 += REG3
PC: 0x28a REG1: 0xffec REG2: 0xfab1ff20 REG3: 0xff20ff92 REG4: 0xffecfab1
REGADD: REG4 += REG1
PC: 0x28b REG1: 0xffec REG2: 0xfa9dff20 REG3: 0xff20ff92 REG4: 0xffecfa9d
MEMSTORE: REG1 = 0x0
PC: 0x28e REG1: 0x0 REG2: 0xfa9dff20 REG3: 0xff20ff92 REG4: 0xfa9d"""
s.add( x[20] + 0x92 == 0 )


""" PC: 0x28f REG1: 0x5b REG2: 0xfa9dff20 REG3: 0xff20ff92 REG4: 0x5bfa9d
MEMSTORE: REG3 = 0x99
PC: 0x292 REG1: 0x5b REG2: 0xfa9dff20 REG3: 0xff20ff99 REG4: 0x5bfa9d
REGADD: REG1 += REG3
PC: 0x293 REG1: 0xfff4 REG2: 0xfa9dff20 REG3: 0xff20ff99 REG4: 0xfff4fa9d
REGADD: REG4 += REG1
PC: 0x294 REG1: 0xfff4 REG2: 0xfa91ff20 REG3: 0xff20ff99 REG4: 0xfff4fa91
MEMSTORE: REG1 = 0x0
PC: 0x297 REG1: 0x0 REG2: 0xfa91ff20 REG3: 0xff20ff99 REG4: 0xfa91"""
s.add( x[21] + 0x99 == 0)

""" PC: 0x298 REG1: 0xa REG2: 0xfa91ff20 REG3: 0xff20ff99 REG4: 0xafa91
MUL: REG1 *= 0x27
PC: 0x29b REG1: 0x186 REG2: 0xfa91ff20 REG3: 0xff20ff99 REG4: 0x186fa91
MEMSTORE: REG3 = 0x40
PC: 0x29e REG1: 0x186 REG2: 0xfa91ff20 REG3: 0xff200040 REG4: 0x186fa91
REGADD: REG1 += REG3
PC: 0x29f REG1: 0x1c6 REG2: 0xfa91ff20 REG3: 0xff200040 REG4: 0x1c6fa91
ADD: REG1 += 0xecb5
PC: 0x2a2 REG1: 0xee7b REG2: 0xfa91ff20 REG3: 0xff200040 REG4: 0xee7bfa91
REGADD: REG4 += REG1
PC: 0x2a3 REG1: 0xee7b REG2: 0xe90cff20 REG3: 0xff200040 REG4: 0xee7be90c
REGSTORE: REG1 = REG4
PC: 0x2a4 REG1: 0xe90c REG2: 0xe90cff20 REG3: 0xff200040 REG4: 0xe90ce90c
MEMSTORE: REG2 = 0x67
PC: 0x2a7 REG1: 0xe90c REG2: 0xe90c0067 REG3: 0x670040 REG4: 0xe90ce90c
PC: 0x67 REG1: 0xe90c REG2: 0xe90c0067 REG3: 0x670040 REG4: 0xe90ce90c
MEMSTORE: REG1 = 0x1
PC: 0x6a REG1: 0x1 REG2: 0xe90c0067 REG3: 0x670040 REG4: 0x1e90c
MEMSTORE: REG2 = 0x19
PC: 0x6d REG1: 0x1 REG2: 0xe90c0019 REG3: 0x190040 REG4: 0x1e90c
ADD: REG2 += 0x3e
PC: 0x70 REG1: 0x1 REG2: 0xe90c0057 REG3: 0x570040 REG4: 0x1e90c"""


print(s.check())
print(s.model())
m = s.model()
flag = ""
for c in x:
    flag += chr(m[c].as_long())
print(flag)

Solution for Handbook

Some movfuscator shit, takes 16 bytes of input and compares it with some random string, use findcrypt, identify aes sbox, identify the key which was AAAABBBBCCCCDDDD.

Solution for Lim Rootkit

Use resource hacker, dump the 2 files, xor some 2 strings and get the flag.

Solution for Dead lock

Hardest part is finding a working tool it’s UndertaleModtool, there is a room called secret, just replace the order of room0 and secret, save and get the flag

Solution for login if you can

Chrome can disassemble wasm files, look at the data assume it’s xor, xor data with some constant 1 byte key. Get the flag.