[GWCTF 2019]babyvm re

阿新 • • 發佈：2022-01-16

BABYVM

基於虛擬機器操作的一個題明面上的check函式和加密邏輯都是假的

操作碼

重點分析這個vm

0xF5, 0xF1, 0xE1, 0x00, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 
  0x20, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x01, 0x00, 0x00, 0x00, 
  0xF2, 0xF1, 0xE4, 0x21, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x02, 
  0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x22, 0x00, 0x00, 0x00, 
  0xF1, 0xE1, 0x03, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x23, 
  0x00, 0x00, 0x00, 0xF1, 0xE1, 0x04, 0x00, 0x00, 0x00, 0xF2, 
  0xF1, 0xE4, 0x24, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x05, 0x00, 
  0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x25, 0x00, 0x00, 0x00, 0xF1, 
  0xE1, 0x06, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x26, 0x00, 
  0x00, 0x00, 0xF1, 0xE1, 0x07, 0x00, 0x00, 0x00, 0xF2, 0xF1, 
  0xE4, 0x27, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x08, 0x00, 0x00, 
  0x00, 0xF2, 0xF1, 0xE4, 0x28, 0x00, 0x00, 0x00, 0xF1, 0xE1, 
  0x09, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x29, 0x00, 0x00, 
  0x00, 0xF1, 0xE1, 0x0A, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 
  0x2A, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0B, 0x00, 0x00, 0x00, 
  0xF2, 0xF1, 0xE4, 0x2B, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0C, 
  0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x2C, 0x00, 0x00, 0x00, 
  0xF1, 0xE1, 0x0D, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x2D, 
  0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0E, 0x00, 0x00, 0x00, 0xF2, 
  0xF1, 0xE4, 0x2E, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0F, 0x00, 
  0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x2F, 0x00, 0x00, 0x00, 0xF1, 
  0xE1, 0x10, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x30, 0x00, 
  0x00, 0x00, 0xF1, 0xE1, 0x11, 0x00, 0x00, 0x00, 0xF2, 0xF1, 
  0xE4, 0x31, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x12, 0x00, 0x00, 
  0x00, 0xF2, 0xF1, 0xE4, 0x32, 0x00, 0x00, 0x00, 0xF1, 0xE1, 
  0x13, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x33, 0x00, 0x00, 
  0x00, 0xF4, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 
  0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 
  0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF5, 0xF1, 
  0xE1, 0x00, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x01, 0x00, 0x00, 
  0x00, 0xF2, 0xF1, 0xE4, 0x00, 0x00, 0x00, 0x00, 0xF1, 0xE1, 
  0x01, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x02, 0x00, 0x00, 0x00, 
  0xF2, 0xF1, 0xE4, 0x01, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x02, 
  0x00, 0x00, 0x00, 0xF1, 0xE2, 0x03, 0x00, 0x00, 0x00, 0xF2, 
  0xF1, 0xE4, 0x02, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x03, 0x00, 
  0x00, 0x00, 0xF1, 0xE2, 0x04, 0x00, 0x00, 0x00, 0xF2, 0xF1, 
  0xE4, 0x03, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x04, 0x00, 0x00, 
  0x00, 0xF1, 0xE2, 0x05, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 
  0x04, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x05, 0x00, 0x00, 0x00, 
  0xF1, 0xE2, 0x06, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x05, 
  0x00, 0x00, 0x00, 0xF1, 0xE1, 0x06, 0x00, 0x00, 0x00, 0xF1, 
  0xE2, 0x07, 0x00, 0x00, 0x00, 0xF1, 0xE3, 0x08, 0x00, 0x00, 
  0x00, 0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00, 0xF6, 0xF7, 0xF1, 
  0xE4, 0x06, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x07, 0x00, 0x00, 
  0x00, 0xF1, 0xE2, 0x08, 0x00, 0x00, 0x00, 0xF1, 0xE3, 0x09, 
  0x00, 0x00, 0x00, 0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00, 0xF6, 
  0xF7, 0xF1, 0xE4, 0x07, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x08, 
  0x00, 0x00, 0x00, 0xF1, 0xE2, 0x09, 0x00, 0x00, 0x00, 0xF1, 
  0xE3, 0x0A, 0x00, 0x00, 0x00, 0xF1, 0xE5, 0x0C, 0x00, 0x00, 
  0x00, 0xF6, 0xF7, 0xF1, 0xE4, 0x08, 0x00, 0x00, 0x00, 0xF1, 
  0xE1, 0x0D, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x13, 0x00, 0x00, 
  0x00, 0xF8, 0xF1, 0xE4, 0x0D, 0x00, 0x00, 0x00, 0xF1, 0xE7, 
  0x13, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0E, 0x00, 0x00, 0x00, 
  0xF1, 0xE2, 0x12, 0x00, 0x00, 0x00, 0xF8, 0xF1, 0xE4, 0x0E, 
  0x00, 0x00, 0x00, 0xF1, 0xE7, 0x12, 0x00, 0x00, 0x00, 0xF1, 
  0xE1, 0x0F, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x11, 0x00, 0x00, 
  0x00, 0xF8, 0xF1, 0xE4, 0x0F, 0x00, 0x00, 0x00, 0xF1, 0xE7, 
  0x11, 0x00, 0x00, 0x00, 0xF4

操作碼接下來分析對應含義

函式含義

0xF1

unsigned __int64 __fastcall sub_555555400B5F(__int64 a1)
{
  int *v2; // [rsp+28h] [rbp-18h]
  unsigned __int64 v3; // [rsp+38h] [rbp-8h]

  v3 = __readfsqword(0x28u);
  v2 = (*(a1 + 16) + 2LL);
  switch ( *(*(a1 + 16) + 1LL) )
  {
    case 0xE1:
      *a1 = *(sbb + *v2);
      break;
    case 0xE2:
      *(a1 + 4) = *(sbb + *v2);
      break;
    case 0xE3:
      *(a1 + 8) = *(sbb + *v2);
      break;
    case 0xE4:
      *(sbb + *v2) = *a1;
      break;
    case 0xE5:
      *(a1 + 12) = *(sbb + *v2);
      break;
    case 0xE7:
      *(sbb + *v2) = *(a1 + 4);
      break;
    default:
      break;
  }
  *(a1 + 16) += 6LL;
  return __readfsqword(0x28u) ^ v3;
}

類似於move 取決於後面的

0XF2

//0XF2
unsigned __int64 __fastcall sub_555555400A64(__int64 a1)
{
  unsigned __int64 v2; // [rsp+18h] [rbp-8h]

  v2 = __readfsqword(0x28u);
  *a1 ^= *(a1 + 4);
  ++*(a1 + 16);
  return __readfsqword(0x28u) ^ v2;
}

異或xor

0XF5

//0xF5
unsigned __int64 __fastcall sub_555555400AC5(__int64 a1)
{
  const char *buf; // [rsp+10h] [rbp-10h]
  unsigned __int64 v3; // [rsp+18h] [rbp-8h]

  v3 = __readfsqword(0x28u);
  buf = sbb;
  read(0, sbb, 0x20uLL);
  dword_5555556022A4 = strlen(buf);
  if ( dword_5555556022A4 != 21 )
  {
    puts("WRONG!");
    exit(0);
  }
  ++*(a1 + 16);
  return __readfsqword(0x28u) ^ v3;
}

好像是個長度判斷

0XF4

//0XF4
unsigned __int64 __fastcall sub_555555400956(__int64 a1)
{
  unsigned __int64 v2; // [rsp+18h] [rbp-8h]

  v2 = __readfsqword(0x28u);
  ++*(a1 + 16);
  return __readfsqword(0x28u) ^ v2;
}

沒啥用 nop

0XF7

//0XF7
unsigned __int64 __fastcall sub_555555400A08(__int64 a1)
{
  unsigned __int64 v2; // [rsp+18h] [rbp-8h]

  v2 = __readfsqword(0x28u);
  *a1 *= *(a1 + 12);
  ++*(a1 + 16);
  return __readfsqword(0x28u) ^ v2;
}

mul乘積

0XF8

0xF8
unsigned __int64 __fastcall sub_5555554008F0(int *a1)
{
  int v2; // [rsp+14h] [rbp-Ch]
  unsigned __int64 v3; // [rsp+18h] [rbp-8h]

  v3 = __readfsqword(0x28u);
  v2 = *a1;
  *a1 = a1[1];
  a1[1] = v2;
  ++*(a1 + 2);
  return __readfsqword(0x28u) ^ v3;
}

swap 交換

0XF6

//0XF6
unsigned __int64 __fastcall sub_55555540099C(__int64 a1)
{
  unsigned __int64 v2; // [rsp+18h] [rbp-8h]

  v2 = __readfsqword(0x28u);
  *a1 = *(a1 + 8) + 2 * *(a1 + 4) + 3 * *a1;
  ++*(a1 + 16);
  return __readfsqword(0x28u) ^ v2;
}

一個函式

解析指令碼

格式化一下

opca = [[0xF5],
        [0xF1, 0xE1, 0x00, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x20, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x01, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x21, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x02, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x22, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x03, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x23, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x04, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x24, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x05, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x25, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x06, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x26, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x07, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x27, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x08, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x28, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x09, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x29, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0A, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x2A, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0B, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x2B, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0C, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x2C, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0D, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x2D, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0E, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x2E, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0F, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x2F, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x10, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x30, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x11, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x31, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x12, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x32, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x13, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x33, 0x00, 0x00, 0x00],

        [0xF4],
        [0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
         0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
         0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
         0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
         0x00, 0x00, ]
        [0xF5],
        [0xF1, 0xE1, 0x00, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x01, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x00, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x01, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x02, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x01, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x02, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x03, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x02, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x03, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x04, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x03, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x04, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x05, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x04, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x05, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x06, 0x00, 0x00, 0x00],
        [0xF2],
        [0xF1, 0xE4, 0x05, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x06, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x07, 0x00, 0x00, 0x00],
        [0xF1, 0xE3, 0x08, 0x00, 0x00, 0x00],
        [0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00],
        [0xF6],
        [0xF7],
        [0xF1, 0xE4, 0x06, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x07, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x08, 0x00, 0x00, 0x00],
        [0xF1, 0xE3, 0x09, 0x00, 0x00, 0x00],
        [0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00],
        [0xF6],
        [0xF7],
        [0xF1, 0xE4, 0x07, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x08, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x09, 0x00, 0x00, 0x00],
        [0xF1, 0xE3, 0x0A, 0x00, 0x00, 0x00],
        [0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00],
        [0xF6],
        [0xF7],
        [0xF1, 0xE4, 0x08, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0D, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x13, 0x00, 0x00, 0x00],
        [0xF8],
        [0xF1, 0xE4, 0x0D, 0x00, 0x00, 0x00],
        [0xF1, 0xE7, 0x13, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0E, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x12, 0x00, 0x00, 0x00],
        [0xF8],
        [0xF1, 0xE4, 0x0E, 0x00, 0x00, 0x00],
        [0xF1, 0xE7, 0x12, 0x00, 0x00, 0x00],
        [0xF1, 0xE1, 0x0F, 0x00, 0x00, 0x00],
        [0xF1, 0xE2, 0x11, 0x00, 0x00, 0x00],
        [0xF8],
        [0xF1, 0xE4, 0x0F, 0x00, 0x00, 0x00],
        [0xF1, 0xE7, 0x11, 0x00, 0x00, 0x00],
        [0xF4]]

for x in opca:
    if x[0] == 0xF1:
        if x[1] == 0xE1:
            print(f"move e1 flag[{x[2]}]")
        if x[1] == 0xE2:
            print(f"move e2 flag[{x[2]}]")
        if x[1] == 0xE3:
            print(f"move e3 flag[{x[2]}]")
        if x[1] == 0xE4:
            print(f"move flag[{x[2]}] e1")
        if x[1] == 0xE5:
            print(f"move e4 flag[{x[2]}]")
        if x[1] == 0xE7:
            print(f"move flag[{x[2]}] e2")
    elif x[0] == 0xf2:
        print("xor e1 e2")
    # elif x[0] == 0XF4:
    #     print("nop")
    elif x[0] == 0xF5:
        print("len")
    elif x[0] == 0xF6:
        print("mov e1 3*e1+2*e2+e3")
    elif x[0] == 0xf7:
        print("mul e1 e2")
    elif x[0] == 0xf8:
        print("swap e1 e2")

結果為

#一看第一段就是假的
read_len
move e1 flag[0]
xor e1 e2
move flag[32] e1
move e1 flag[1]
xor e1 e2
move flag[33] e1
move e1 flag[2]
xor e1 e2
move flag[34] e1
move e1 flag[3]
xor e1 e2
move flag[35] e1
move e1 flag[4]
xor e1 e2
move flag[36] e1
move e1 flag[5]
xor e1 e2
move flag[37] e1
move e1 flag[6]
xor e1 e2
move flag[38] e1
move e1 flag[7]
xor e1 e2
move flag[39] e1
move e1 flag[8]
xor e1 e2
move flag[40] e1
move e1 flag[9]
xor e1 e2
move flag[41] e1
move e1 flag[10]
xor e1 e2
move flag[42] e1
move e1 flag[11]
xor e1 e2
move flag[43] e1
move e1 flag[12]
xor e1 e2
move flag[44] e1
move e1 flag[13]
xor e1 e2
move flag[45] e1
move e1 flag[14]
xor e1 e2
move flag[46] e1
move e1 flag[15]
xor e1 e2
move flag[47] e1
move e1 flag[16]
xor e1 e2
move flag[48] e1
move e1 flag[17]
xor e1 e2
move flag[49] e1
move e1 flag[18]
xor e1 e2
move flag[50] e1
move e1 flag[19]
xor e1 e2
move flag[51] e1

#從這段開始是真的 直接逆
read_len
#下面三段都是異或
move e1 flag[0]
move e2 flag[1]
xor e1 e2
move flag[0] e1

move e1 flag[1]
move e2 flag[2]
xor e1 e2
move flag[1] e1

move e1 flag[2]
move e2 flag[3]
xor e1 e2
move flag[2] e1

move e1 flag[3]
move e2 flag[4]
xor e1 e2
move flag[3] e1

move e1 flag[4]
move e2 flag[5]
xor e1 e2
move flag[4] e1

move e1 flag[5]
move e2 flag[6]
xor e1 e2
move flag[5] e1
#下面三段都是相乘
move e1 flag[6]
move e2 flag[7]
move e3 flag[8]
move e4 flag[12]
mov e1 3*e1+2*e2+e3
mul e1 e4
move flag[6] e1

move e1 flag[7]
move e2 flag[8]
move e3 flag[9]
move e4 flag[12]
mov e1 3*e1+2*e2+e3
mul e1 e4
move flag[7] e1

move e1 flag[8]
move e2 flag[9]
move e3 flag[10]
move e4 flag[12]
mov e1 3*e1+2*e2+e3
mul e1 e4
move flag[8] e1
#下面三段都是交換
move e1 flag[13]
move e2 flag[19]
swap e1 e2
move flag[13] e1
move flag[19] e2

move e1 flag[14]
move e2 flag[18]
swap e1 e2
move flag[14] e1
move flag[18] e2

move e1 flag[15]
move e2 flag[17]
swap e1 e2
move flag[15] e1
move flag[17] e2

flag z3求解！

from z3 import *

flag = [0x69, 0x45, 0x2A, 0x37, 0x09, 0x17, 0xC5, 0x0B, 0x5C, 0x72,
        0x33, 0x76, 0x33, 0x21, 0x74, 0x31, 0x5F, 0x33, 0x73, 0x72,
        0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
        0x00, 0x00]
flag[15], flag[17] = flag[17], flag[15]
flag[14], flag[18] = flag[18], flag[14]
flag[13], flag[19] = flag[19], flag[13]
#
# so = Solver()
# e1 = BitVec("e1", 8)
# e2 = BitVec("e2",8)
# e3 = BitVec("e3", 8)
# e4 = BitVec("e4", 8)
#
# so.add(e2 == 0x72)
# so.add(e3 == 0x33)
# so.add(e4 == 0x33)
# so.add((3 * e1 + 2 * e2 + e3) * e4 == 0x5C)
# print(so.check())
# print(so.model())
flag[8] = 95
#
# so = Solver()
# e1 = BitVec("e1", 8)
# e2 = BitVec("e2",8)
# e3 = BitVec("e3", 8)
# e4 = BitVec("e4", 8)
#
# so.add(e2 == flag[8])
# so.add(e3 == flag[9])
# so.add(e4 == flag[12])
# so.add((3 * e1 + 2 * e2 + e3) * e4== flag[7])
# print(so.check())
# print(so.model())

flag[7] = 51

so = Solver()
e1 = BitVec("e1", 8)
e2 = BitVec("e2", 8)
e3 = BitVec("e3", 8)
e4 = BitVec("e4", 8)

so.add(e2 == flag[7])
so.add(e3 == flag[8])
so.add(e4 == flag[12])
so.add((3 * e1 + 2 * e2 + e3) * e4 == flag[6])
print(so.check())
print(so.model())

flag[6] = 118
flag[5]^=flag[6]
flag[4]^=flag[5]
flag[3]^=flag[4]
flag[2]^=flag[3]
flag[1]^=flag[2]
flag[0]^=flag[1]
print(flag)
for x in flag:
        print(chr(x),end="")

Y0u_hav3_r3v3rs3_1t!