ByteAPK

Flutter rust bridge
ByteCTF{}，总长度45
flag被通过ffi传到rust，然后utf8转成c string,去掉了ByteCTF{和后面的},传到一个函数里面check

unsigned char arr1[] =
{
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 
  0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 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, 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, 
  0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 
  0x00, 0x00, 0x00, 0x00, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 
  0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 
  0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 0x02, 
  0x02, 0x02, 0x02, 0x02, 0x03, 0x03, 0x03, 0x03, 0x03, 0x03, 
  0x03, 0x03, 0x03, 0x03, 0x03, 0x03, 0x03, 0x03, 0x03, 0x03, 
  0x04, 0x04, 0x04, 0x04, 0x04, 0x00, 0x00, 0x00, 0x00, 0x00, 
  0x00, 0x00, 0x00, 0x00, 0x00, 0x00
};
unsigned int enc[32] = {
    0x0001EE59, 0x0000022A, 0x00001415, 0x00040714, 0x000013E0, 0x000008B8, 0xFFFDCEA0, 0x0000313B, 
    0x0003D798, 0xFFFFFE6B, 0x00000C4E, 0x00023884, 0x0000008D, 0x00001DB4, 0xFFFC1328, 0x00001EAC, 
    0x00043C64, 0x0000142B, 0xFFFFF622, 0x00023941, 0xFFFFEF6D, 0x0000120C, 0xFFFBD30F, 0x00001EBE, 
    0x00045158, 0xFFFFEF66, 0x00001D3F, 0x0004C46B, 0xFFFFF97A, 0x00001BFD, 0xFFFBA235, 0x00001ED2
};

__int64 __fastcall final_enc(unsigned __int8 *flag_intern, __int64 a2)
{
  __int64 v2; // x9
  __int64 v3; // x9
  __int64 v4; // x9
  __int64 v5; // x9
  __int64 v6; // x9
  __int64 v7; // x9
  __int64 v8; // x9
  __int64 v9; // x9
  unsigned int v10; // w11
  int v11; // w13
  __int64 v12; // x9
  __int64 v13; // x9
  __int64 v14; // x9
  __int64 v15; // x9
  __int64 v16; // x9
  unsigned int v18; // w10
  int v19; // w13
  __int64 v20; // x9
  __int64 v21; // x9
  __int64 v22; // x9
  __int64 v23; // x9
  __int64 v24; // x9
  unsigned int v25; // w10
  int v26; // w13
  __int64 v27; // x9
  __int64 v28; // x9
  __int64 v29; // x9
  __int64 v30; // x9
  __int64 v31; // x9
  unsigned int v32; // w8
  int v33; // w11
  unsigned __int64 v34; // x20
  __int64 v35; // x21
  unsigned int v36; // w22
  int v37; // w8
  __int64 v38; // x10
  int v39; // w9
  unsigned __int64 v40; // x8
  __int64 v41; // x9
  unsigned __int64 v42; // x10
  unsigned __int64 v43; // x8
  int v44; // w12
  int v45; // w14
  int v46; // w3
  int v47; // w13
  int v48; // w2
  int v49; // w16
  int v50; // w15
  int v51; // w17
  int v52; // w6
  int v53; // w4
  int v54; // w12
  int *v55; // x13
  __int64 v57; // [xsp+8h] [xbp-48h] BYREF
  __int64 v58; // [xsp+10h] [xbp-40h]
  unsigned __int64 v59; // [xsp+18h] [xbp-38h]

  v57 = 0LL;
  v58 = 4LL;
  if ( a2 != 36 )
    return 0LL;
  v2 = arr1[*flag_intern];
  if ( (_DWORD)v2 == 36 )
    return 0LL;
  v3 = arr1[flag_intern[v2]] + v2;
  if ( v3 == 36 )
    return 0LL;
  v4 = v3 + arr1[flag_intern[v3]];
  if ( v4 == 36 )
    return 0LL;
  v5 = v4 + arr1[flag_intern[v4]];
  if ( v5 == 36 )
    return 0LL;
  v6 = v5 + arr1[flag_intern[v5]];
  if ( v6 == 36 )
    return 0LL;
  v7 = v6 + arr1[flag_intern[v6]];
  if ( v7 == 36 )
    return 0LL;
  v8 = v7 + arr1[flag_intern[v7]];
  if ( v8 == 36 )
    return 0LL;
  v9 = v8 + arr1[flag_intern[v8]];
  if ( v9 == 36 )
    return 0LL;
  v10 = flag_intern[v9];
  if ( (char)flag_intern[v9] < 0 )
  {
    if ( v10 < 0xE0 )
    {
      v10 = flag_intern[v9 + 1] & 0x3F | ((v10 & 0x1F) << 6);
    }
    else
    {
      v11 = flag_intern[v9 + 2] & 0x3F | ((flag_intern[v9 + 1] & 0x3F) << 6);
      if ( v10 < 0xF0 )
        v10 = v11 | ((v10 & 0x1F) << 12);
      else
        v10 = flag_intern[v9 + 3] & 0x3F | (v11 << 6) & 0xFFE3FFFF | ((v10 & 7) << 18);
    }
  }
  if ( v10 != 45 )
    return 0LL;
  v12 = v9 + arr1[flag_intern[v9]];
  if ( v12 == 36 )
    return 0LL;
  v13 = v12 + arr1[flag_intern[v12]];
  if ( v13 == 36 )
    return 0LL;
  v14 = v13 + arr1[flag_intern[v13]];
  if ( v14 == 36 )
    return 0LL;
  v15 = v14 + arr1[flag_intern[v14]];
  if ( v15 == 36 )
    return 0LL;
  v16 = v15 + arr1[flag_intern[v15]];
  if ( v16 == 36 )
    return 0LL;
  v18 = flag_intern[v16];
  if ( (char)flag_intern[v16] < 0 )
  {
    if ( v18 < 0xE0 )
    {
      v18 = flag_intern[v16 + 1] & 0x3F | ((v18 & 0x1F) << 6);
    }
    else
    {
      v19 = flag_intern[v16 + 2] & 0x3F | ((flag_intern[v16 + 1] & 0x3F) << 6);
      if ( v18 < 0xF0 )
        v18 = v19 | ((v18 & 0x1F) << 12);
      else
        v18 = flag_intern[v16 + 3] & 0x3F | (v19 << 6) & 0xFFE3FFFF | ((v18 & 7) << 18);
    }
  }
  if ( v18 != 45 )
    return 0LL;
  v20 = v16 + arr1[flag_intern[v16]];
  if ( v20 == 36 )
    return 0LL;
  v21 = v20 + arr1[flag_intern[v20]];
  if ( v21 == 36 )
    return 0LL;
  v22 = v21 + arr1[flag_intern[v21]];
  if ( v22 == 36 )
    return 0LL;
  v23 = v22 + arr1[flag_intern[v22]];
  if ( v23 == 36 )
    return 0LL;
  v24 = v23 + arr1[flag_intern[v23]];
  if ( v24 == 36 )
    return 0LL;
  v25 = flag_intern[v24];
  if ( (char)flag_intern[v24] < 0 )
  {
    if ( v25 < 0xE0 )
    {
      v25 = flag_intern[v24 + 1] & 0x3F | ((v25 & 0x1F) << 6);
    }
    else
    {
      v26 = flag_intern[v24 + 2] & 0x3F | ((flag_intern[v24 + 1] & 0x3F) << 6);
      if ( v25 < 0xF0 )
        v25 = v26 | ((v25 & 0x1F) << 12);
      else
        v25 = flag_intern[v24 + 3] & 0x3F | (v26 << 6) & 0xFFE3FFFF | ((v25 & 7) << 18);
    }
  }
  if ( v25 != 45 )
    return 0LL;
  v27 = v24 + arr1[flag_intern[v24]];
  if ( v27 == 36 )
    return 0LL;
  v28 = v27 + arr1[flag_intern[v27]];
  if ( v28 == 36 )
    return 0LL;
  v29 = v28 + arr1[flag_intern[v28]];
  if ( v29 == 36 )
    return 0LL;
  v30 = v29 + arr1[flag_intern[v29]];
  if ( v30 == 36 )
    return 0LL;
  v31 = v30 + arr1[flag_intern[v30]];
  if ( v31 == 36 )
    return 0LL;
  v32 = flag_intern[v31];
  if ( (char)flag_intern[v31] < 0 )
  {
    if ( v32 < 0xE0 )
    {
      v32 = flag_intern[v31 + 1] & 0x3F | ((v32 & 0x1F) << 6);
    }
    else
    {
      v33 = flag_intern[v31 + 2] & 0x3F | ((flag_intern[v31 + 1] & 0x3F) << 6);
      if ( v32 < 0xF0 )
        v32 = v33 | ((v32 & 0x1F) << 12);
      else
        v32 = flag_intern[v31 + 3] & 0x3F | (v33 << 6) & 0xFFE3FFFF | ((v32 & 7) << 18);
    }
  }
  if ( v32 != 45 )
    return 0LL;
  v34 = 0LL;
  v35 = 0LL;
  while ( 1 )
  {
    v36 = flag_intern[v35];
    if ( (char)flag_intern[v35] < 0 )
    {
      v37 = flag_intern[v35 + 1] & 0x3F;
      if ( v36 < 0xE0 )
      {
        v35 += 2LL;
        v36 = v37 & 0xFFFFF83F | ((v36 & 0x1F) << 6);
      }
      else
      {
        v38 = v35 + 3;
        v39 = flag_intern[v35 + 2] & 0x3F | (v37 << 6);
        if ( v36 < 0xF0 )
        {
          v36 = v39 | ((v36 & 0x1F) << 12);
          v35 += 3LL;
        }
        else
        {
          v35 += 4LL;
          v36 = flag_intern[v38] & 0x3F | (v39 << 6) & 0xFFE3FFFF | ((v36 & 7) << 18);
        }
      }
    }
    else
    {
      ++v35;
    }
    if ( v36 != 45 )
      break;
LABEL_55:
    if ( v35 == 36 )
      goto LABEL_67;
  }
  if ( v36 != 0x110000 )
  {
    if ( v34 == v57 )
      sub_3B688(&v57, a2);
    *(_DWORD *)(v58 + 4 * v34++) = v36;
    v59 = v34;
    goto LABEL_55;
  }
LABEL_67:
  v40 = v34 >> 3;
  v41 = 0LL;
  if ( (v34 & 7) != 0 )
    ++v40;
  v42 = v40 + 1;
  v43 = 8LL;
  while ( --v42 )
  {
    if ( v43 > v34 )
      goto LABEL_88;
    if ( v43 - 8 >= 0x19 )
    {
      v43 = 40LL;
      v34 = 32LL;
LABEL_88:
      panic(v43, v34, (__int64)&off_801E0);
    }
    v45 = *(_DWORD *)(v58 + v41 * 4 + 8);
    v44 = *(_DWORD *)(v58 + v41 * 4 + 12);
    v46 = *(_DWORD *)(v58 + v41 * 4);
    v47 = *(_DWORD *)(v58 + v41 * 4 + 4);
    v48 = *(_DWORD *)(v58 + v41 * 4 + 16);
    v49 = *(_DWORD *)(v58 + v41 * 4 + 20);
    v50 = *(_DWORD *)(v58 + v41 * 4 + 24);
    v51 = *(_DWORD *)(v58 + v41 * 4 + 28);
    if ( v51 + v47 * v44 * v49 - (v46 + v50 + v45 * v48) == enc[v41] )
    {
      v52 = v46 * v49;
      if ( v44 - v48 - v46 * v49 + v51 * v47 + v45 + v50 == enc[v41 + 1]
        && v52 - (v48 + v51 * v47) + v45 + v50 * v44 == enc[v41 + 2] )
      {
        v53 = v48 * v46;
        if ( v47 + v48 * v46 - (v51 + v45) + v50 * v49 * v44 == enc[v41 + 3]
          && v49 * v44 + v47 + v45 * v48 - (v50 + v51 * v46) == enc[v41 + 4]
          && v52 + v47 * v44 + v45 - (v50 + v48 * v51) == enc[v41 + 5]
          && v51 - v47 + v45 * v49 + v50 - v53 * v44 == enc[v41 + 6] )
        {
          v43 += 8LL;
          v54 = v44 - v51 - (v47 + v49);
          v55 = &enc[v41];
          v41 += 8LL;
          if ( v54 + v53 + v50 * v45 == v55[7] )
            continue;
        }
      }
    }
    if ( v57 )
      c_free(v58, 4 * v57, 4LL);
    return 0LL;
  }
  if ( v57 )
    c_free(v58, 4 * v57, 4LL);
  return 1LL;
}

通过观察，注意到前面的一堆是在检验是否是UUID，后面则是一个标准的z3题目。
exp

from regadgets import *
from z3 import *

enc = [
    0x0001EE59, 0x0000022A, 0x00001415, 0x00040714, 0x000013E0, 0x000008B8, 0xFFFDCEA0, 0x0000313B, 
    0x0003D798, 0xFFFFFE6B, 0x00000C4E, 0x00023884, 0x0000008D, 0x00001DB4, 0xFFFC1328, 0x00001EAC, 
    0x00043C64, 0x0000142B, 0xFFFFF622, 0x00023941, 0xFFFFEF6D, 0x0000120C, 0xFFFBD30F, 0x00001EBE, 
    0x00045158, 0xFFFFEF66, 0x00001D3F, 0x0004C46B, 0xFFFFF97A, 0x00001BFD, 0xFFFBA235, 0x00001ED2
]

for j in range(4):
    x = [BitVec(f"x{i+1}", 32) for i in range(8)]
    x1, x2, x3, x4, x5, x6, x7, x8 = tuple(i for i in x)
    s = Solver()
    for i in x:
        s.add(i > 0x20, i < 0x80)
    s.add(x8 + x2 * x4 * x6 - (x1 + x7 + x3 * x5) == enc[0+j*8])
    v52 = x1 * x6
    s.add(x4 - x5 - x1 * x6 + x8 * x2 + x3 + x7 == enc[1+j*8])
    s.add(v52 - (x5 + x8 * x2) + x3 + x7 * x4 == enc[2+j*8])
    v53 = x5 * x1
    s.add(x2 + x5 * x1 - (x8 + x3) + x7 * x6 * x4 == enc[3+j*8])
    s.add(x6 * x4 + x2 + x3 * x5 - (x7 + x8 * x1) == enc[4+j*8])
    s.add(v52 + x2 * x4 + x3 - (x7 + x5 * x8) == enc[5+j*8])
    s.add(x8 - x2 + x3 * x6 + x7 - v53 * x4 == enc[6+j*8])
    v54 = x4 - x8 - (x2 + x6)
    s.add(v54 + v53 + x7 * x3 == enc[7+j*8])
    
    if s.check() == sat:
        m = s.model()
        for i in x:
            l = m[i].as_long()
            print(l2b(l).decode(),end='')
            # 32e750c8fb214562af22973fb5176b9c
            # ByteCTF{32e750c8-fb21-4562-af22-973fb5176b9c}