# ISITDTU CTF 2024 Write-Up

## Rev - Animal

Challenge cho một file PE64


Chạy thử thì chương trình yêu cầu nhập Flag, sai thì trả về False


Mở bằng IDA64, ta có hàm main của chương trình như dưới đây

int __fastcall main(int argc, const char **argv, const char **envp)
{
  unsigned __int64 v3; // r8
  void **v4; // rcx
  void **v5; // rax
  void **v6; // rax
  void **v7; // rax
  void **v8; // rax
  void **v9; // rax
  const char *v10; // rdx
  void *v11; // rcx
  void *inp[2]; // [rsp+20h] [rbp-50h] BYREF
  __int64 v14; // [rsp+30h] [rbp-40h]
  unsigned __int64 v15; // [rsp+38h] [rbp-38h]
  __int128 v16; // [rsp+40h] [rbp-30h]
  __int64 v17; // [rsp+50h] [rbp-20h]
  __int64 v18; // [rsp+58h] [rbp-18h]

  *(_OWORD *)inp = 0i64;
  v14 = 0i64;
  v15 = 15i64;
  LOBYTE(inp[0]) = 0;
  sub_7FF6FF4C16B0(std::cout, "Enter the flag: ", envp);
  sub_7FF6FF4C1890(std::cin, inp);
  if ( v14 != 36 )
    goto LABEL_20;
  v4 = inp;
  v3 = v15;
  if ( v15 > 0xF )
    v4 = (void **)inp[0];
  v5 = inp;
  if ( v15 > 0xF )
    v5 = (void **)inp[0];
  if ( *((_BYTE *)v4 + 33) != *((_BYTE *)v5 + 34) )
    goto LABEL_20;
  v6 = inp;
  if ( v15 > 0xF )
    v6 = (void **)inp[0];
  if ( 2 * *((char *)v6 + 8) != 194 )
    goto LABEL_20;
  v16 = 0i64;
  v18 = 15i64;
  v7 = inp;
  if ( v15 > 0xF )
    v7 = (void **)inp[0];
  LOBYTE(v16) = *((_BYTE *)v7 + 17);
  v8 = inp;
  if ( v15 > 0xF )
    v8 = (void **)inp[0];
  BYTE1(v16) = *((_BYTE *)v8 + 18);
  v9 = inp;
  if ( v15 > 0xF )
    v9 = (void **)inp[0];
  v17 = 3i64;
  BYTE3(v16) = 0;
  if ( (_WORD)v16 == 'ac' && *((_BYTE *)v9 + 19) == 't' && (unsigned __int8)sub_7FF6FF4C1290(inp) )
    v10 = "True!!";
  else
LABEL_20:
    v10 = "False!!";
  sub_7FF6FF4C16B0(std::cout, v10, v3);
  if ( v15 > 0xF )
  {
    v11 = inp[0];
    if ( v15 + 1 >= 0x1000 )
    {
      v11 = (void *)*((_QWORD *)inp[0] - 1);
      if ( (unsigned __int64)(inp[0] - v11 - 8) > 0x1F )
        invalid_parameter_noinfo_noreturn();
    }
    j_j_free(v11);
  }
  return 0;
}

Chương trình yêu cầu người dùng nhập Flag, sau đó qua nhiều điều kiện để check, nếu đúng thì in ra True, sai thì in ra False. Dưới đây là điều kiện check ``v14 != 36``, qua nhiều lần debug có thể dễ dàng nhận ra chương trình đang check độ dài chuỗi nhập vào có bằng 36 kí tự hay không. Sau đó qua hàm ``main`` ta có thể nhận ra chương trình có check thêm một vài điều kiện cho chuỗi nhập vào như dưới đây:

a1[17] == ord('c')
a1[18] == ord('a')
a1[19] == ord('t')
a1[33] == a1[34]
2 * a1[8] == 194

Sau đó chương trình nhảy vào hàm ``sub_7FF6FF4C1290`` để check tiếp


Phần cuối của hàm ``sub_7FF6FF4C1290`` có một vị trí nhảy đến lệnh ``call rax`` như hình trên, mình debug và nhảy vào đó thì chương trình chạy đến một đoạn shellcode như hình dưới


Dễ dàng nhận ra những điều kiện còn lại của input sẽ được check tại đoạn shellcode này

_BOOL8 __fastcall sub_FF7E8FF515(char *a1)
{
  int v2; // ebx
  int v3; // esi
  int v4; // r14d
  int v5; // ebp
  int v6; // r9d
  int v7; // edx
  int v8; // r12d
  int v9; // r15d
  int v10; // edi
  int v11; // r13d
  int v12; // r10d
  int v13; // edi
  int v14; // r11d
  int v15; // r9d
  int v16; // eax
  int v17; // r9d
  int v18; // eax
  int v19; // r13d
  int v20; // r11d
  int v21; // ebx
  int v22; // ecx
  int v23; // r11d
  int v24; // eax
  int v25; // edi
  int v26; // r9d
  int v28; // [rsp+38h] [rbp+8h]
  int v29; // [rsp+40h] [rbp+10h]

  v2 = a1[27];
  v3 = a1[1];
  v4 = a1[32];
  v5 = a1[8];
  v6 = a1[29];
  if ( v5 * v3 + v4 * v2 * a1[25] - v6 != 538738 )
    return 0i64;
  v7 = a1[4];
  v8 = a1[10];
  v9 = a1[20];
  if ( a1[7] + v9 * v8 * v7 - a1[6] - a1[11] != 665370 )
    return 0i64;
  v10 = a1[30];
  if ( a1[14] + (a1[16] - 1) * a1[31] - v10 * a1[22] != -2945 )
    return 0i64;
  v11 = a1[18];
  v12 = a1[33];
  if ( v12 + a1[3] - a1[9] - v11 - a1[11] - v7 != -191 )
    return 0i64;
  if ( v3 + v10 + v11 + a1[25] * v6 - v5 != 4853 )
    return 0i64;
  v13 = a1[7];
  v14 = a1[13];
  if ( v14 + a1[5] - v13 * a1[14] * a1[23] * a1[2] != -86153321 )
    return 0i64;
  v15 = a1[9];
  if ( v14 + v15 * a1[5] * a1[12] + v2 * v8 != 873682 )
    return 0i64;
  v16 = v15 * a1[21];
  v17 = a1[6];
  v18 = v11 * v16;
  v19 = a1[22];
  if ( v19 + a1[3] + v18 - v17 != 451644 )
    return 0i64;
  v20 = a1[24];
  if ( a1[21] + a1[34] + v20 + v4 * a1[23] - v7 != 9350 )
    return 0i64;
  v21 = a1[17];
  v22 = a1[19];
  v29 = a1[35];
  v28 = a1[26];
  if ( v20 + v29 + a1[17] - v22 - v28 - v17 != 27 )
    return 0i64;
  v23 = a1[15];
  if ( a1[14] + a1[13] + v23 + a1[23] * v22 - a1[3] == 11247
    && (v24 = v13 * a1[12], v25 = a1[2], v25 + v21 + v24 - v23 - a1[21] == 13297)
    && (v26 = *a1, v5 + v29 + v28 + a1[28] - v26 - v9 == 266)
    && v25 + v21 + v26 + a1[12] * a1[28] - v3 == 10422
    && v19 + v23 + a1[5] * v22 - a1[34] - a1[11] == 9883 )
  {
    return v8 * v12 + a1[16] * (1 - v9) - v26 == -5604;
  }
  else
  {
    return 0i64;
  }
}

Từ những điều kiện trên mình sẽ viết một script dùng z3 để lấy flag

from z3 import *

solver = Solver()

a1 = [Int(f'a1[{i}]') for i in range(36)]
for ch in a1:
    solver.add(ch >= 0x20, ch <= 0x7E)

solver.add(a1[0] == ord('I'))
solver.add(a1[1] == ord('S'))
solver.add(a1[2] == ord('I'))
solver.add(a1[3] == ord('T'))
solver.add(a1[4] == ord('D'))
solver.add(a1[5] == ord('T'))
solver.add(a1[6] == ord('U'))
solver.add(a1[7] == ord('{'))
solver.add(a1[35] == ord('}'))
solver.add(a1[17] == ord('c'))
solver.add(a1[18] == ord('a'))
solver.add(a1[19] == ord('t'))
solver.add(a1[33] == a1[34])
solver.add(2 * a1[8] == 194)
v2 = a1[27]
v3 = a1[1]
v4 = a1[32]
v5 = a1[8]
v6 = a1[29]
v7 = a1[4]
v8 = a1[10]
v9 = a1[20]
v10 = a1[30]
v11 = a1[18]
v12 = a1[33]
v13 = a1[7]
v14 = a1[13]
v15 = a1[9]
v16 = v15 * a1[21]
v17 = a1[6]
v18 = v11 * v16
v19 = a1[22]
v20 = a1[24]
v21 = a1[17]
v22 = a1[19]
v29 = a1[35]
v28 = a1[26]
v23 = a1[15]
v24 = v13 * a1[12]
v25 = a1[2]
v26 = a1[0]


solver.add(v5 * v3 + v4 * v2 * a1[25] - v6 == 538738)
solver.add(a1[7] + v9 * v8 * v7 - a1[6] - a1[11] == 665370)
solver.add(a1[14] + (a1[16] - 1) * a1[31] - v10 * a1[22] == -2945)
solver.add(v12 + a1[3] - a1[9] - v11 - a1[11] - v7 == -191)
solver.add(v3 + v10 + v11 + a1[25] * v6 - v5 == 4853)
solver.add(v14 + a1[5] - v13 * a1[14] * a1[23] * a1[2] == -86153321)
solver.add(v14 + v15 * a1[5] * a1[12] + v2 * v8 == 873682)
solver.add(v19 + a1[3] + v18 - v17 == 451644)
solver.add(a1[21] + a1[34] + v20 + v4 * a1[23] - v7 == 9350)
solver.add(v20 + v29 + a1[17] - v22 - v28 - v17 == 27)
solver.add(a1[14] + a1[13] + v23 + a1[23] * v22 - a1[3] == 11247)
solver.add(v25 + v21 + v24 - v23 - a1[21] == 13297)
solver.add(v5 + v29 + v28 + a1[28] - v26 - v9 == 266)
solver.add(v25 + v21 + v26 + a1[12] * a1[28] - v3 == 10422)
solver.add(v19 + v23 + a1[5] * v22 - a1[34] - a1[11] == 9883)
solver.add(v8 * v12 + a1[16] * (1 - v9) - v26 == -5604)
if solver.check() == sat:
    model = solver.model()
    result = ''.join(chr(model.evaluate(a1[i]).as_long()) for i in range(36))
    print("Solution:", result)
else:
    print("No solution found")

Chạy Script trên và mình lấy được flag của challenge: ``ISITDTU{a_g0lden_cat_1n_y0ur_area!!}``

## Rev - re02

Chương trình cho một file ``re02.nes``. Đây là định dạng tệp của các trò chơi trên hệ máy Nintendo Entertainment System (NES), một trong những hệ máy chơi game phổ biến nhất vào thập niên 80. Các file này chứa dữ liệu ROM của game, bao gồm mã lệnh, đồ họa, âm thanh, và bản đồ của game, cho phép các trình giả lập chạy chúng trên nhiều nền tảng hiện đại.

Để phân tích file này, mình sẽ sử dụng Ghidra với Extension [này](https://github.com/ilyakharlamov/Ghidra-Nes-Rom-Decompiler-Plugin) để hỗ trợ đọc mã giả

Bằng cách Search, mình thấy được hai chuỗi ``Correct! ISITDTU{`` và ``GIVE ME THE PASSWORD`` ở dưới


Trace theo các địa chỉ trên thì mình thấy chúng được khai báo tại biến ``DAT_93a0`` và được gọi tại hàm ``reset``

void reset(byte param_1)

{
  undefined uVar1;
  byte bVar2;
  char cVar3;
  char cVar4;
  short sVar5;
  bool bVar6;
  
  JOYPAD_PORT2 = 0x40;
  sVar5 = CONCAT11((char)((ushort)register0x22 >> 8),0xff);
  PPUMASK = 0;
  APU_DELTA_REG = 0;
  PPUCTRL = 0;
  do {
  } while (-1 < (char)(param_1 & PPUSTATUS));
  do {
  } while (-1 < (char)(param_1 & PPUSTATUS));
  PPUADDR = 0x20;
  do {
    PPUADDR = PPUADDR - 1;
  } while (PPUADDR != 0);
  cVar3 = '\x10';
  bVar2 = PPUADDR;
  do {
    do {
      bVar2 = bVar2 + 1;
    } while (bVar2 != 0);
    cVar3 = cVar3 + -1;
    PPUDATA = PPUADDR;
  } while (cVar3 != '\0');
  do {
    *(undefined *)(ushort)bVar2 = 0;
    *(undefined *)(bVar2 + 0x100) = 0;
    *(undefined *)(bVar2 + 0x200) = 0;
    *(undefined *)(bVar2 + 0x300) = 0;
    *(undefined *)(bVar2 + 0x400) = 0;
    *(undefined *)(bVar2 + 0x500) = 0;
    *(undefined *)(bVar2 + 0x600) = 0;
    *(undefined *)(bVar2 + 0x700) = 0;
    bVar2 = bVar2 + 1;
  } while (bVar2 != 0);
  *(undefined2 *)(sVar5 + -1) = 0x8067;
  FUN_8276(4,0);
  *(undefined2 *)(sVar5 + -1) = 0x806a;
  FUN_824b();
  *(undefined2 *)(sVar5 + -1) = 0x806d;
  FUN_82a3();
  *(undefined2 *)(sVar5 + -1) = 0x8070;
  FUN_937d();
  *(undefined2 *)(sVar5 + -1) = 0x8073;
  FUN_932e();
  DAT_0031._0_1_ = 0;
  DAT_0031._1_1_ = 8;
  write_1(DAT_0016,0x80);
  PPUCTRL = 0x80;
  write_1(DAT_0018,6);
  cVar3 = read_1(DAT_0001);
  do {
    cVar4 = read_1(DAT_0001);
  } while (cVar3 == cVar4);
  cVar3 = '4';
  cVar4 = '\x18';
  do {
    do {
      cVar3 = cVar3 + -1;
    } while (cVar3 != '\0');
    cVar4 = cVar4 + -1;
  } while (cVar4 != '\0');
  write_1(DAT_0000,PPUSTATUS & 0x80);
  *(undefined2 *)(sVar5 + -1) = 0x80a0;
  FUN_827d();
  *(undefined2 *)(sVar5 + -1) = 0x80a7;
  FUN_8502(0,0);
  uVar1 = read_1(DAT_0000);
  *(undefined2 *)(sVar5 + -1) = 0x80b0;
  FUN_8a9c(uVar1,0xa0,-0x6d);
  *(undefined2 *)(sVar5 + -1) = 0x80b7;
  FUN_8e83(0xa0,0x93);
  write_1(DAT_0019,0xfd);
  write_1(DAT_001a,0xfd);
  PPUSCROLL = 0;
  DAT_0030 = 0;
  do {
    *(undefined2 *)(sVar5 + -1) = 0x909e;
    FUN_8365();
    *(undefined2 *)(sVar5 + -1) = 0x90a3;
    DAT_033b = FUN_84c5(0);
    if (DAT_033b != '\0') {
      if (DAT_033b == -0x80) {
        DAT_033b = 't';
      }
      if (DAT_033b == '@') {
        DAT_033b = 'u';
      }
      if (DAT_033b == ' ') {
        DAT_033b = 'a';
      }
      if (DAT_033b == '\x10') {
        DAT_033b = 'n';
      }
      if (DAT_033b == '\x02') {
        DAT_033b = 'l';
      }
      if (DAT_033b == '\x01') {
        DAT_033b = 'i';
      }
      if (DAT_033b == '\b') {
        DAT_033b = 'n';
      }
      if (DAT_033b == '\x04') {
        DAT_033b = 'h';
      }
      *(char *)(DAT_0030 + 0x300) = DAT_033b;
      DAT_0030 = DAT_0030 + 1;
      DAT_033b = '\0';
    }
  } while (DAT_0030 < 0x10);
  *(undefined2 *)(sVar5 + -1) = 0x9123;
  FUN_827d();
  *(undefined2 *)(sVar5 + -1) = 0x912a;
  FUN_8228(199,0x93);
  *(undefined2 *)(sVar5 + -1) = 0x9131;
  LAB_PPUADDR_8560(0xca);
  bVar6 = CARRY1(DAT_0300,DAT_0301);
  cVar3 = bVar6 != false;
  if (CARRY1(DAT_0300 + DAT_0301,DAT_0302) != false) {
    cVar3 = cVar3 + '\x01';
  }
  if ((cVar3 == '\x01') &&
     ((byte)(DAT_0300 + DAT_0301 + DAT_0302 + (bVar6 == false && bVar6)) == 'J')) {
    bVar6 = CARRY1(DAT_0301,DAT_0302);
    cVar4 = '\0';
    if (bVar6 != false) {
      cVar4 = cVar3;
    }
    if (CARRY1(DAT_0301 + DAT_0302,DAT_0303) != false) {
      cVar4 = cVar4 + '\x01';
    }
    if ((cVar4 == '\x01') &&
       ((byte)(DAT_0301 + DAT_0302 + DAT_0303 + (bVar6 == false && bVar6)) == 'D')) {
      bVar6 = CARRY1(DAT_0302,DAT_0303);
      cVar3 = '\0';
      if (bVar6 != false) {
        cVar3 = cVar4;
      }
      if (CARRY1(DAT_0302 + DAT_0303,DAT_0304) != false) {
        cVar3 = cVar3 + '\x01';
      }
      if ((cVar3 == '\x01') &&
         ((byte)(DAT_0302 + DAT_0303 + DAT_0304 + (bVar6 == false && bVar6)) == ';')) {
        bVar6 = CARRY1(DAT_0303,DAT_0304);
        cVar4 = '\0';
        if (bVar6 != false) {
          cVar4 = cVar3;
        }
        if (CARRY1(DAT_0303 + DAT_0304,DAT_0305) != false) {
          cVar4 = cVar4 + '\x01';
        }
        if ((cVar4 == '\x01') &&
           ((byte)(DAT_0303 + DAT_0304 + DAT_0305 + (bVar6 == false && bVar6)) == 'C')) {
          bVar6 = CARRY1(DAT_0304,DAT_0305);
          cVar3 = '\0';
          if (bVar6 != false) {
            cVar3 = cVar4;
          }
          if (CARRY1(DAT_0304 + DAT_0305,DAT_0306) != false) {
            cVar3 = cVar3 + '\x01';
          }
          if ((cVar3 == '\x01') &&
             ((byte)(DAT_0304 + DAT_0305 + DAT_0306 + (bVar6 == false && bVar6)) == 'C')) {
            bVar6 = CARRY1(DAT_0305,DAT_0306);
            cVar4 = '\0';
            if (bVar6 != false) {
              cVar4 = cVar3;
            }
            if (CARRY1(DAT_0305 + DAT_0306,DAT_0307) != false) {
              cVar4 = cVar4 + '\x01';
            }
            if ((cVar4 == '\x01') &&
               ((byte)(DAT_0305 + DAT_0306 + DAT_0307 + (bVar6 == false && bVar6)) == '?')) {
              bVar6 = CARRY1(DAT_0306,DAT_0307);
              cVar3 = '\0';
              if (bVar6 != false) {
                cVar3 = cVar4;
              }
              if (CARRY1(DAT_0306 + DAT_0307,DAT_0308) != false) {
                cVar3 = cVar3 + '\x01';
              }
              if ((cVar3 == '\x01') &&
                 ((byte)(DAT_0306 + DAT_0307 + DAT_0308 + (bVar6 == false && bVar6)) == 'B')) {
                bVar6 = CARRY1(DAT_0307,DAT_0308);
                cVar4 = '\0';
                if (bVar6 != false) {
                  cVar4 = cVar3;
                }
                if (CARRY1(DAT_0307 + DAT_0308,DAT_0309) != false) {
                  cVar4 = cVar4 + '\x01';
                }
                if ((cVar4 == '\x01') &&
                   ((byte)(DAT_0307 + DAT_0308 + DAT_0309 + (bVar6 == false && bVar6)) == '=')) {
                  bVar6 = CARRY1(DAT_0308,DAT_0309);
                  cVar3 = '\0';
                  if (bVar6 != false) {
                    cVar3 = cVar4;
                  }
                  if (CARRY1(DAT_0308 + DAT_0309,DAT_030a) != false) {
                    cVar3 = cVar3 + '\x01';
                  }
                  if ((cVar3 == '\x01') &&
                     ((byte)(DAT_0308 + DAT_0309 + DAT_030a + (bVar6 == false && bVar6)) == 'C')) {
                    bVar6 = CARRY1(DAT_0309,DAT_030a);
                    cVar4 = '\0';
                    if (bVar6 != false) {
                      cVar4 = cVar3;
                    }
                    if (CARRY1(DAT_0309 + DAT_030a,DAT_030b) != false) {
                      cVar4 = cVar4 + '\x01';
                    }
                    if ((cVar4 == '\x01') &&
                       ((byte)(DAT_0309 + DAT_030a + DAT_030b + (bVar6 == false && bVar6)) == '?'))
                    {
                      bVar6 = CARRY1(DAT_030a,DAT_030b);
                      cVar3 = '\0';
                      if (bVar6 != false) {
                        cVar3 = cVar4;
                      }
                      if (CARRY1(DAT_030a + DAT_030b,DAT_030c) != false) {
                        cVar3 = cVar3 + '\x01';
                      }
                      if ((cVar3 == '\x01') &&
                         ((byte)(DAT_030a + DAT_030b + DAT_030c + (bVar6 == false && bVar6)) == 'J')
                         ) {
                        bVar6 = CARRY1(DAT_030b,DAT_030c);
                        cVar4 = '\0';
                        if (bVar6 != false) {
                          cVar4 = cVar3;
                        }
                        if (CARRY1(DAT_030b + DAT_030c,DAT_030d) != false) {
                          cVar4 = cVar4 + '\x01';
                        }
                        if ((cVar4 == '\x01') &&
                           ((byte)(DAT_030b + DAT_030c + DAT_030d + (bVar6 == false && bVar6)) ==
                            'Q')) {
                          bVar6 = CARRY1(DAT_030c,DAT_030d);
                          cVar3 = '\0';
                          if (bVar6 != false) {
                            cVar3 = cVar4;
                          }
                          if (CARRY1(DAT_030c + DAT_030d,DAT_030e) != false) {
                            cVar3 = cVar3 + '\x01';
                          }
                          if ((cVar3 == '\x01') &&
                             ((byte)(DAT_030c + DAT_030d + DAT_030e + (bVar6 == false && bVar6)) ==
                              'J')) {
                            bVar6 = CARRY1(DAT_030d,DAT_030e);
                            cVar4 = '\0';
                            if (bVar6 != false) {
                              cVar4 = cVar3;
                            }
                            if (CARRY1(DAT_030d + DAT_030e,DAT_030f) != false) {
                              cVar4 = cVar4 + '\x01';
                            }
                            if ((cVar4 == '\x01') &&
                               ((byte)(DAT_030d + DAT_030e + DAT_030f + (bVar6 == false && bVar6))
                                == 'D')) {
                              DAT_002f = 0;
                              while (bVar2 = (&DAT_93a0)[DAT_002f], (&DAT_93a0)[DAT_002f] != 0) {
                                uVar1 = (&DAT_93a0)[DAT_002f];
                                *(undefined2 *)(sVar5 + -1) = 0x92f5;
                                LAB_PPUDATA_8567(uVar1);
                                DAT_002f = DAT_002f + 1;
                              }
                              while (DAT_002f = bVar2, DAT_002f < 0x2b) {
                                DAT_0033 = *(byte *)(DAT_002f + 0x310);
                                DAT_0039 = (byte *)CONCAT11(3,DAT_002f & 0xf);
                                bVar2 = *DAT_0039 ^ DAT_0033;
                                *(undefined2 *)(sVar5 + -1) = 0x931e;
                                LAB_PPUDATA_8567(bVar2);
                                bVar2 = DAT_002f + 1;
                              }
                              *(undefined2 *)(sVar5 + -1) = 0x932b;
                              LAB_PPUDATA_8567(0x7d);
                            }
                          }
                        }
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  bVar2 = read_1(DAT_0018);
  write_1(DAT_0018,bVar2 | 0x18);
  FUN_8365();
  return;
}

Có thể thấy hàm này rất dài, và nếu chỉ có vậy thì vẫn không thể rõ được chương trình sẽ làm những gì cả, vì vậy mình quyết định sử dụng tool [Mesen](https://www.mesen.ca/). Tool này sẽ hỗ trợ giả lập môi trường, giúp người dùng thực thi file và debug qua chương trình


Sử dụng Masen để chạy thử và theo dõi Memory của nó, mình nhận ra chương trình không hiển thị gì, nhưng bằng cách nhập một số kí tự, các chữ cái ``t``, ``u``, ``a``, ``n``, ``l``, ``i``, ``h`` sẽ được hiển thị tại địa chỉ ``0x300`` trên memory

Tuy nhiên ta chỉ được phép nhập tối đa 16 kí tự, nếu không thì chương trình sẽ bị crash như ảnh dưới


Sau nhiều lần nhập thử mình nhận ra quy tắc nhập sẽ như sau:
- Nhập nút lên: memory ghi vào chữ ``n``
- Nhập nút xuống: memory ghi vào chữ ``h``
- Nhập nút trái: memory ghi vào chữ ``l``
- Nhập nút phải: memory ghi vào chữ ``i``
- Nhập nút ``q``: memory ghi vào chữ ``a``
- Nhập nút ``a``: memory ghi vào chữ ``u``
- Nhập nút ``s``: memory ghi vào chữ ``t``

Bây giờ mình cần phải tìm điều kiện để kiểm tra những kí tự được nhập vào, và mình đọc lại hàm ``reset``, mình có đoạn chương trình dưới đây

  if ((cVar3 == '\x01') &&
     ((byte)(DAT_0300 + DAT_0301 + DAT_0302 + (bVar6 == false && bVar6)) == 'J')) {
    bVar6 = CARRY1(DAT_0301,DAT_0302);
    cVar4 = '\0';
    if (bVar6 != false) {
      cVar4 = cVar3;
    }
    if (CARRY1(DAT_0301 + DAT_0302,DAT_0303) != false) {
      cVar4 = cVar4 + '\x01';
    }
    if ((cVar4 == '\x01') &&
       ((byte)(DAT_0301 + DAT_0302 + DAT_0303 + (bVar6 == false && bVar6)) == 'D')) {
      bVar6 = CARRY1(DAT_0302,DAT_0303);
      cVar3 = '\0';
      if (bVar6 != false) {
        cVar3 = cVar4;
      }
      if (CARRY1(DAT_0302 + DAT_0303,DAT_0304) != false) {
        cVar3 = cVar3 + '\x01';
      }
      if ((cVar3 == '\x01') &&
         ((byte)(DAT_0302 + DAT_0303 + DAT_0304 + (bVar6 == false && bVar6)) == ';')) {
        bVar6 = CARRY1(DAT_0303,DAT_0304);
        cVar4 = '\0';
        if (bVar6 != false) {
          cVar4 = cVar3;
        }
        if (CARRY1(DAT_0303 + DAT_0304,DAT_0305) != false) {
          cVar4 = cVar4 + '\x01';
        }
        if ((cVar4 == '\x01') &&
           ((byte)(DAT_0303 + DAT_0304 + DAT_0305 + (bVar6 == false && bVar6)) == 'C')) {
          bVar6 = CARRY1(DAT_0304,DAT_0305);
          cVar3 = '\0';
          if (bVar6 != false) {
            cVar3 = cVar4;
          }
          if (CARRY1(DAT_0304 + DAT_0305,DAT_0306) != false) {
            cVar3 = cVar3 + '\x01';
          }
          if ((cVar3 == '\x01') &&
             ((byte)(DAT_0304 + DAT_0305 + DAT_0306 + (bVar6 == false && bVar6)) == 'C')) {
            bVar6 = CARRY1(DAT_0305,DAT_0306);
            cVar4 = '\0';
            if (bVar6 != false) {
              cVar4 = cVar3;
            }
            if (CARRY1(DAT_0305 + DAT_0306,DAT_0307) != false) {
              cVar4 = cVar4 + '\x01';
            }
            if ((cVar4 == '\x01') &&
               ((byte)(DAT_0305 + DAT_0306 + DAT_0307 + (bVar6 == false && bVar6)) == '?')) {
              bVar6 = CARRY1(DAT_0306,DAT_0307);
              cVar3 = '\0';
              if (bVar6 != false) {
                cVar3 = cVar4;
              }
              if (CARRY1(DAT_0306 + DAT_0307,DAT_0308) != false) {
                cVar3 = cVar3 + '\x01';
              }
              if ((cVar3 == '\x01') &&
                 ((byte)(DAT_0306 + DAT_0307 + DAT_0308 + (bVar6 == false && bVar6)) == 'B')) {
                bVar6 = CARRY1(DAT_0307,DAT_0308);
                cVar4 = '\0';
                if (bVar6 != false) {
                  cVar4 = cVar3;
                }
                if (CARRY1(DAT_0307 + DAT_0308,DAT_0309) != false) {
                  cVar4 = cVar4 + '\x01';
                }
                if ((cVar4 == '\x01') &&
                   ((byte)(DAT_0307 + DAT_0308 + DAT_0309 + (bVar6 == false && bVar6)) == '=')) {
                  bVar6 = CARRY1(DAT_0308,DAT_0309);
                  cVar3 = '\0';
                  if (bVar6 != false) {
                    cVar3 = cVar4;
                  }
                  if (CARRY1(DAT_0308 + DAT_0309,DAT_030a) != false) {
                    cVar3 = cVar3 + '\x01';
                  }
                  if ((cVar3 == '\x01') &&
                     ((byte)(DAT_0308 + DAT_0309 + DAT_030a + (bVar6 == false && bVar6)) == 'C')) {
                    bVar6 = CARRY1(DAT_0309,DAT_030a);
                    cVar4 = '\0';
                    if (bVar6 != false) {
                      cVar4 = cVar3;
                    }
                    if (CARRY1(DAT_0309 + DAT_030a,DAT_030b) != false) {
                      cVar4 = cVar4 + '\x01';
                    }
                    if ((cVar4 == '\x01') &&
                       ((byte)(DAT_0309 + DAT_030a + DAT_030b + (bVar6 == false && bVar6)) == '?'))
                    {
                      bVar6 = CARRY1(DAT_030a,DAT_030b);
                      cVar3 = '\0';
                      if (bVar6 != false) {
                        cVar3 = cVar4;
                      }
                      if (CARRY1(DAT_030a + DAT_030b,DAT_030c) != false) {
                        cVar3 = cVar3 + '\x01';
                      }
                      if ((cVar3 == '\x01') &&
                         ((byte)(DAT_030a + DAT_030b + DAT_030c + (bVar6 == false && bVar6)) == 'J')
                         ) {
                        bVar6 = CARRY1(DAT_030b,DAT_030c);
                        cVar4 = '\0';
                        if (bVar6 != false) {
                          cVar4 = cVar3;
                        }
                        if (CARRY1(DAT_030b + DAT_030c,DAT_030d) != false) {
                          cVar4 = cVar4 + '\x01';
                        }
                        if ((cVar4 == '\x01') &&
                           ((byte)(DAT_030b + DAT_030c + DAT_030d + (bVar6 == false && bVar6)) ==
                            'Q')) {
                          bVar6 = CARRY1(DAT_030c,DAT_030d);
                          cVar3 = '\0';
                          if (bVar6 != false) {
                            cVar3 = cVar4;
                          }
                          if (CARRY1(DAT_030c + DAT_030d,DAT_030e) != false) {
                            cVar3 = cVar3 + '\x01';
                          }
                          if ((cVar3 == '\x01') &&
                             ((byte)(DAT_030c + DAT_030d + DAT_030e + (bVar6 == false && bVar6)) ==
                              'J')) {
                            bVar6 = CARRY1(DAT_030d,DAT_030e);
                            cVar4 = '\0';
                            if (bVar6 != false) {
                              cVar4 = cVar3;
                            }
                            if (CARRY1(DAT_030d + DAT_030e,DAT_030f) != false) {
                              cVar4 = cVar4 + '\x01';
                            }
                            if ((cVar4 == '\x01') &&
                               ((byte)(DAT_030d + DAT_030e + DAT_030f + (bVar6 == false && bVar6))
                                == 'D')) {
                              DAT_002f = 0;

``DAT_0300`` tương đương với vị trí ``0x300`` trong memory, nó tương đương với kí tự đầu tiên của chuỗi sau khi biến đổi từ input nhập vào, tương tự các biến ``DAT_030d`` tương ứng kí tự thứ ``0xD``,... Đây chính là nơi check điều kiện nhập vào. Dựa vào đây mình sẽ viết script để lấy chuỗi nhập chính xác

from z3 import *

bitvecs =  [BitVec(f'v{i}', 8) for i in range(16)]
solver = Solver()
valid_chars = [ord(c) for c in "tuanlinh"]
for v in bitvecs:   
    solver.add(Or([v == c for c in valid_chars]))
solver.add((bitvecs[0] + bitvecs[1] + bitvecs[2]) & 0xFF == ord('J'))
solver.add((bitvecs[3] + bitvecs[1] + bitvecs[2]) & 0xFF == ord('D'))
solver.add((bitvecs[3] + bitvecs[4] + bitvecs[2]) & 0xFF == ord(';')) 
solver.add((bitvecs[3] + bitvecs[4] + bitvecs[5]) & 0xFF == ord('C'))
solver.add((bitvecs[4] + bitvecs[5] + bitvecs[6]) & 0xFF == ord('C'))
solver.add((bitvecs[5] + bitvecs[6] + bitvecs[7]) & 0xFF == ord('?'))
solver.add((bitvecs[6] + bitvecs[7] + bitvecs[8]) & 0xFF == ord('B')) 
solver.add((bitvecs[7] + bitvecs[8] + bitvecs[9]) & 0xFF == ord('='))
solver.add((bitvecs[8] + bitvecs[9] + bitvecs[10]) & 0xFF == ord('C'))
solver.add((bitvecs[9] + bitvecs[10] + bitvecs[11]) & 0xFF == ord('?'))
solver.add((bitvecs[10] + bitvecs[11] + bitvecs[12]) & 0xFF == ord('J'))
solver.add((bitvecs[12] + bitvecs[11] + bitvecs[13]) & 0xFF == ord('Q'))
solver.add((bitvecs[14] + bitvecs[13] + bitvecs[12]) & 0xFF == ord('J'))
solver.add((bitvecs[13] + bitvecs[14] + bitvecs[15]) & 0xFF == ord('D'))

if solver.check() == sat:
    model = solver.model()
    result = ''.join(chr(model.evaluate(bitvecs[i]).as_long()) for i in range(16))
    print(result)
else:
    print("wrong")

Kết quả của Script trên là chuỗi ``tuanlinhlinhtuan``. Bây giờ mình chỉ cần dựa vào những quy tắc nhập mình đưa ra trước đó để nhập sao cho đúng input như trên là được, và mình đã lấy được flag của Challenge như ở hình dưới.