[ASIS CTF 2018] Density

[IDA code]

void __fastcall __noreturn main(int a1, char **a2, char **a3)
{
  unsigned int v3; // eax
  char *v4; // rax
  char *v5; // r12
  char *v6; // rbx
  void *v7; // rax
  char *v8; // rbx
  unsigned __int64 v9; // [rsp+8h] [rbp-20h]
 
  v3 = time(0LL);
  srand(v3);
  if ( a1 == 2 )
  {
    v5 = sub_DE0();
    v6 = sub_DE0();
    v7 = (void *)sub_F40(v5, a2[1]);
    v8 = (char *)sub_F40(v7, v6);
    v9 = strlen(v8);
    sub_FB0(v8, &v9);
    sub_14F0(v8, v9);
    putchar(10);
  }
  else if ( a1 != 3 || (v4 = a2[1], *v4 != 45) || v4[1] != 100 || v4[2] )
  {
    puts("usage: ./befshar input");
  }
  else
  {
    puts("error not implemented ");
  }
  exit(0);
}
 
char *sub_DE0()
{
  int v0; // eax
  int v1; // ebp
  int v2; // ebx
  char *v3; // r12
  char *v4; // r13
  __int64 v6; // [rsp+0h] [rbp-98h]
  __int64 v7; // [rsp+8h] [rbp-90h]
  __int64 v8; // [rsp+10h] [rbp-88h]
  __int64 v9; // [rsp+18h] [rbp-80h]
  __int64 v10; // [rsp+20h] [rbp-78h]
  __int64 v11; // [rsp+28h] [rbp-70h]
  __int64 v12; // [rsp+30h] [rbp-68h]
  __int64 v13; // [rsp+38h] [rbp-60h]
  __int64 v14; // [rsp+40h] [rbp-58h]
  __int64 v15; // [rsp+48h] [rbp-50h]
  __int64 v16; // [rsp+50h] [rbp-48h]
  __int64 v17; // [rsp+58h] [rbp-40h]
  __int16 v18; // [rsp+60h] [rbp-38h]
  char v19; // [rsp+62h] [rbp-36h]
 
  v0 = rand();
  v1 = v0 % 14 + 3;
  v2 = v0 % 14;
  v3 = (char *)malloc(v0 % 14 + 4);
  v3[v1] = 0;
  v19 = 0;
  v6 = 5208208757389214273LL;
  v7 = 5786930140093827657LL;
  v8 = 6365651522798441041LL;
  v9 = 7378413942531512921LL;
  v10 = 7957135325236127847LL;
  v11 = 8535856707940741231LL;
  v12 = 3689065129052829815LL;
  v13 = 3398873257388422452LL;
  v14 = 2748641777075299392LL;
  v15 = 3327364263599220775LL;
  v16 = 738377296636492335LL;
  v17 = 9114578090173750363LL;
  v18 = 2400;
  if ( v1 > 0 )
  {
    v4 = v3;
    do
      *(++v4 - 1) = *((_BYTE *)&v6 + rand() % 99);
    while ( v4 != &v3[v2 + 2 + 1] );
  }
  return v3;
}
 
char *__fastcall sub_F40(void *src, void *a2)
{
  size_t v2; // rbx
  size_t v3; // rax
  size_t v4; // r14
  size_t v5; // r12
  char *v6; // rbp
 
  v2 = strlen((const char *)src);
  v3 = strlen((const char *)a2);
  v4 = v3;
  v5 = (signed int)v2 + (signed int)v3 + 1;
  v6 = (char *)malloc(v5);
  memcpy(v6, src, v2);
  memcpy(&v6[v2], a2, v4);
  v6[v5 - 1] = 0;
  return v6;
}
 
void __fastcall sub_FB0(_BYTE *a1, unsigned __int64 *a2)
{
  unsigned __int64 *v2; // r14
  _BYTE *mix_str; // rbx
  unsigned __int64 v4; // r12
  char *en_str; // r15
  unsigned __int64 v6; // r13
  const unsigned __int16 **v7; // rcx
  signed int v8; // ebp
  __int64 v9; // rdi
  __int64 v10; // rax
  unsigned __int64 v11; // rcx
  int v12; // edx
  char *en_string; // rbp
  char *v14; // rax
  int v15; // esi
  char v16; // al
  char *v17; // rax
  signed __int64 v18; // rax
  int v19; // esi
  signed __int64 v20; // rdx
  char *v21; // rax
  signed __int64 v22; // rax
  int v23; // esi
  signed __int64 v24; // rdx
  char *v25; // rax
  unsigned __int64 v26; // rax
  char *v27; // rax
  __int64 v28; // rdi
  int v29; // esi
  char *v30; // rax
  int v31; // edi
  int v32; // esi
  __int64 v33; // rdi
  const unsigned __int16 **v34; // ST10_8
  const __int32_t **v35; // rax
  char v36; // [rsp+0h] [rbp-58h]
  char v37; // [rsp+0h] [rbp-58h]
  char v38; // [rsp+0h] [rbp-58h]
  const unsigned __int16 **v39; // [rsp+0h] [rbp-58h]
  int v40; // [rsp+8h] [rbp-50h]
 
  v2 = a2;
  mix_str = a1;
  v4 = *a2;
  en_str = (char *)malloc(4 * *a2);
  if ( !en_str )
    sub_13A0("malloc");
  if ( v4 )
  {
    v6 = 0LL;
    v7 = __ctype_b_loc();
    v8 = 0;
    do
    {
      v9 = (char)mix_str[v6];
      if ( (*v7)[v9] & 8 )                      // 특수문자 검사
      {
        en_str[v8] = mix_str[v6];
        v4 = v8++ + 1;
      }
      else if ( (_BYTE)v9 == 32 )
      {
        v4 = v8;
        if ( v8 > 1 && (v33 = en_str[v8 - 1], HIBYTE((*v7)[v33]) & 2) && en_str[v8 - 2] == 43 )
        {
          v34 = v7;
          v35 = __ctype_toupper_loc();
          v7 = v34;
          en_str[v8 - 1] = (*v35)[v33];
        }
        else
        {
          ++v8;
          en_str[v4] = '/';
          v4 = v8;
        }
      }
      else
      {
        if ( !(_BYTE)v9 )
          goto LABEL_9;
        v39 = v7;
        v27 = strchr("@$_!\"#%&'()*+,-./:;<=>?\n", (char)v9);
        v7 = v39;
        if ( v27 )
        {
          v28 = v8;
          v29 = v8 + 1;
          v8 += 2;
          en_str[v28] = '+';
          v4 = v8;
          en_str[v29] = (_BYTE)v27 - (unsigned __int64)"@$_!\"#%&'()*+,-./:;<=>?\n" + 97;
        }
        else
        {
          v30 = strchr("[\\]^{|}~`\t", (char)v9);
          v7 = v39;
          if ( !v30 )
LABEL_9:
            sub_1370("Invalid input, accepting only printable chars");
          v31 = v8 + 1;
          en_str[v8] = '+';
          v32 = v8 + 2;
          v8 += 3;
          v4 = v8;
          en_str[v31] = '+';
          en_str[v32] = (_BYTE)v30 - (unsigned __int64)"[\\]^{|}~`\t" + 97;
        }
      }
      ++v6;
    }
    while ( *v2 > v6 );
    if ( v8 & 3 )
    {
      v10 = v8 + 1;
      do
      {
        v11 = (signed int)v10;
        en_str[v10 - 1] = '/';
        v12 = v10++ & 3;
      }
      while ( v12 );
      *v2 = v11;
    }
    else
    {
      *v2 = v4;
      if ( !v4 )
        goto LABEL_21;
    }
    en_string = en_str;
    v40 = 0;
    do
    {
      v14 = strchr("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/", *en_string);
      if ( !v14 )
        sub_1370("Invalid character in transcoded message");
      v15 = en_string[1];
      v16 = 4 * (unsigned __int64)(v14 - "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/");
      *mix_str = v16;
      v36 = v16;
      v17 = strchr("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/", v15);
      if ( !v17 )
        sub_1370("Invalid character in transcoded message");
      v18 = v17 - "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/";
      v19 = en_string[2];
      v20 = v18;
      LOBYTE(v18) = 16 * v18;
      LOBYTE(v20) = v36 | (unsigned __int64)(v20 >> 4);
      mix_str[1] = v18;
      v37 = v18;
      *mix_str = v20;
      v21 = strchr("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/", v19);
      if ( !v21 )
        sub_1370("Invalid character in transcoded message");
      v22 = v21 - "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/";
      v23 = en_string[3];
      v24 = v22;
      LOBYTE(v22) = (_BYTE)v22 << 6;
      LOBYTE(v24) = v37 | (unsigned __int64)(v24 >> 2);
      mix_str[2] = v22;
      v38 = v22;
      mix_str[1] = v24;
      v25 = strchr("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/", v23);
      if ( !v25 )
        sub_1370("Invalid character in transcoded message");
      v40 += 3;
      mix_str += 3;
      *(mix_str - 1) = v38 | ((_BYTE)v25
                            - (unsigned __int64)"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/");
      v26 = (unsigned __int64)&en_string[4LL - (_QWORD)en_str];
      en_string += 4;
    }
    while ( *v2 > v26 );
    v4 = v40;
  }
LABEL_21:
  *v2 = v4;
  free(en_str);
}
 
size_t __fastcall sub_14F0(const void *a1, size_t a2)
{
  return fwrite(a1, 1uLL, a2, stdout);
}

[Solve]

from z3 import *
 
short = "3B EF A1 F9 BF AA 70 04 88 4B EF 9E D3 57 7E 73 83 5D F9 C1 A8 2C 3F 9C 01 22 12 F9 CD 43 7B 8F 9C E0 7E 2D F9 C8 34 7B 9F 9C 7F 4A FE 72 5B 3E 77 EF A0 74 8F BE 8F E9 0C FA F6 FE F9 F0 FD 5B EA BF 0A".split()
table1 = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
table2 = "@$_!\"#%&'()*+,-./:;<=>?\n"
table3 = "[\\]^{|}~`\t"
length = len(short)
 
key = [BitVec("key[%d]"%i, 8) for i in range(length / 3 * 4)]
s = Solver()
for i in range(length / 3 * 4):
    s.add(key[i] >= 0, key[i] < len(table1))
 
j = 0
for i in range(0, length-1, 3):
    s.add(((key[j] << 2) | (key[j+1] >> 4)) == int(short[i], 16))
    s.add(((key[j+1] << 4) | (key[j+2] >> 2)) == int(short[i+1], 16))
    s.add(((key[j+2] << 6) | (key[j+3])) == int(short[i+2], 16))
    j += 4
 
print s.check()
k = s.model()
 
st = ''
for i in range(length / 3 * 4):
    st += table1[int(str(k[key[i]]))]
 
flag = ''
i = 0
while i < len(st):
    if st[i] == '+':
        i += 1
        if st[i] == '+':
            i += 1
            flag += table3[ord(st[i]) - 97]
        else:
            flag += table2[ord(st[i]) - 97]
    else:
        flag += st[i]
    i += 1
 
print flag
'''
sat
O~$/cASIS{01d_4Nd_GoLD_ASIS_1De4_4H4t_g0e5_f0r_ls!}dI    )M>b|D9W//
'''