5.elf

5.elf教会了我需要注意数据的类型与数据的长度，不然也容易犯错误

关键在于看懂那几个强制类型转化，和运算符的顺序

其main函数为

int __cdecl main(int argc, const char **argv, const char **envp)
{
  char s[64]; // [rsp+0h] [rbp-1D0h] BYREF
  int v5[84]; // [rsp+40h] [rbp-190h] BYREF此处为int型4字节一个
  __int64 v6; // [rsp+190h] [rbp-40h]此处为int64，64bit 8字节一个
  __int64 v7[3]; // [rsp+198h] [rbp-38h] BYREF此处为int64 8字节一个
  _BYTE v8[15]; // [rsp+1B0h] [rbp-20h]此处为1字节一个
  char v9; // [rsp+1BFh] [rbp-11h]
  int v10; // [rsp+1C0h] [rbp-10h]
  int v11; // [rsp+1C4h] [rbp-Ch]
  int j; // [rsp+1C8h] [rbp-8h]
  int i; // [rsp+1CCh] [rbp-4h]

  *(_QWORD *)v8 = 0xA718337232343F22LL;
  *(_QWORD *)&v8[7] = 0x7A1EC18428F131A7LL;
  v6 = 0x1412100D0A070401LL;
  v7[0] = 0x2A2724211F1D1A17LL;
  qmemcpy((char *)v7 + 6, "'*-/147:=@CFILOR", 16);
  qmemcpy(v5, "\n", sizeof(v5));
  i = 0;
  j = 0;
  v11 = 0;
  v10 = 0;
  v9 = 0;
  memset(s, 0, sizeof(s));
  puts("PLZ input");
  __isoc99_scanf("%s", s);
  for ( i = 0; i <= 14; ++i )
  {
    for ( j = 0; j <= 1; ++j )
    {
      v10 = *((char *)&v7[-1] + v11 + j);//v7先用了括号访问符此处指针指向的是v7[0]前8个字节的数据
      switch ( v5[v10] )//此处都有强制类型转化但本质是一致的取的是数据的低八位，注意v5是int型占四字节
      {
        case 2:
          s[i] += LOBYTE(v5[v10 + 1]);
          break;
        case 3:
          s[i] -= LOBYTE(v5[v10 + 1]);
          break;
        case 4:
          s[i] ^= LOBYTE(v5[v10 + 1]);
          break;
        case 5:
          s[i] *= (unsigned __int8)v5[v10 + 1];
          break;
        case 11:
          --s[i];
          break;
        case 12:
          ++s[i];
          break;
        default:
          continue;
      }
    }
    v11 += 2;
  }
  for ( i = 0; i <= 14; ++i )
  {
    if ( s[i] != v8[i] )
    {
      printf("wrong wrong wrong");
      return 0;
    }
  }
  printf("woc,you got it,flag is your input");
  return 0;
}

根据其加密和数据类型可以通过动态调试获得几个数组的原始数据

如图v5是四个字节为一段数据（注意高位低位区别）

v5=[
0x0A,0x04,0x10,0x08,
0x03,0x05,0x01,0x04,
0x20,0x08,0x05,0x03,
0x01,0x03,0x02,0x08,
0x0B,0x01,0x0C,0x08,
0x04,0x04,0x01,0x05,
0x03,0x08,0x03,0x21,
0x01,0x0B,0x08,0x0B,
0x01,0x04,0x09,0x08,
0x03,0x20,0x01,0x02,
0x51,0x08,0x04,0x24,
0x01,0x0C,0x08,0x0B,
0x01,0x05,0x02,0x08,
0x02,0x25,0x01,0x02,
0x36,0x08,0x04,0x41,
0x01,0x02,0x20,0x08,
0x05,0x01,0x01,0x05,
0x03,0x08,0x02,0x25,
0x01,0x04,0x09,0x08,
0x03,0x20,0x01,0x02,
0x41,0x08,0x0C,0x01
]#此处仅有低位有数据可以直接去掉0x00的数据便于访问

v7=[
0x01,0x04,0x07,0x0a,0x0d,0x10,0x12,0x14,
0x17,0x1a,0x1d,0x1f,0x21,0x24,0x27,
0x2a,0x2d,0x2f,0x31,0x34,0x37,0x3a,0x3d,
0x40,0x43,0x46,0x49,0x4c,0x4f,0x52,0x00,
0x00,0x22,0x3f,0x34,0x32,0x72,0x33,0x18,
0xa7,0x31]#v7最开始进行的是v7[-1]，因为python的[-1]跟c不同，此处可以直接将其数组前移8字节，在后续访问时可以不用使用v7[-1]

v8=[
0x22,0x3f,0x34,0x32,0x72,0x33,0x18,0xa7,
0x31,0xf1,0x28,0x84,0xc1,0x1e,0x7a,0x00]#直接从动态调试中取就行

具体解密如下

from z3 import*
v8=[
0x22,0x3f,0x34,0x32,0x72,0x33,0x18,0xa7,
0x31,0xf1,0x28,0x84,0xc1,0x1e,0x7a,0x00]
v7=[
0x01,0x04,0x07,0x0a,0x0d,0x10,0x12,0x14,
0x17,0x1a,0x1d,0x1f,0x21,0x24,0x27,
0x2a,0x2d,0x2f,0x31,0x34,0x37,0x3a,0x3d,
0x40,0x43,0x46,0x49,0x4c,0x4f,0x52,0x00,
0x00,0x22,0x3f,0x34,0x32,0x72,0x33,0x18,
0xa7,0x31]
v5=[
0x0A,0x04,0x10,0x08,
0x03,0x05,0x01,0x04,
0x20,0x08,0x05,0x03,
0x01,0x03,0x02,0x08,
0x0B,0x01,0x0C,0x08,
0x04,0x04,0x01,0x05,
0x03,0x08,0x03,0x21,
0x01,0x0B,0x08,0x0B,
0x01,0x04,0x09,0x08,
0x03,0x20,0x01,0x02,
0x51,0x08,0x04,0x24,
0x01,0x0C,0x08,0x0B,
0x01,0x05,0x02,0x08,
0x02,0x25,0x01,0x02,
0x36,0x08,0x04,0x41,
0x01,0x02,0x20,0x08,
0x05,0x01,0x01,0x05,
0x03,0x08,0x02,0x25,
0x01,0x04,0x09,0x08,
0x03,0x20,0x01,0x02,
0x41,0x08,0x0C,0x01
]
flag = [BitVec('flag[%2d]' % i, 8) for i in range(15)]
out=[0]*15
for i in range(15):
    out[i]=flag[i]
i=0
j=0
v11=0
v10=0
v9=0
for i in range(15):
    for j in range(2):
        v10=v7[v11+j]
        match v5[v10]:
            case 2:
                out[i]=out[i]+v5[v10+1]
            case 3:
                out[i]=out[i]-v5[v10+1]
            case 4:
                out[i]=out[i]^v5[v10+1]
            case 5:
                out[i]=out[i]*v5[v10+1]
            case 11:
                out[i]-=1
            case 12:
                out[i]+=1
            case _:
                continue
    v11+=2
f=Solver()
for i in range(15):
    f.add(out[i]==v8[i])
while(f.check()==sat):
    condition = []
    m = f.model()
    p=""
    for i in range(15):
        p+=chr(int("%s" % (m[flag[i]])))
        condition.append(flag[i]!=int("%s" % (m[flag[i]])))
    print(p)
    f.add(Or(condition))

解出来有两个解，依次输入其中试试

上一个为正确的解：757515121f3d478