BUUCTF RE WriteUp 4

[GXYCTF] simple CPP

这个和之前的重复了啊，主函数逻辑很简单

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
__int64 sub_7FF7BDA61290()
{
  bool v0; // si
  __int64 v1; // rax
  unsigned __int8 *v2; // rax
  unsigned __int8 *data1; // rbx
  int cnt; // er10
  __int64 cnt_; // r11
  _BYTE *inputs; // r9
  void **halt; // r8
  __int64 byteNow; // rdi
  __int64 v9; // r15
  __int64 v10; // r12
  __int64 v11; // rbp
  signed int cnt1; // ecx
  unsigned __int8 *data1_; // rdx
  __int64 bytes; // rdi
  __int64 *v15; // r14
  __int64 v16; // rbp
  __int64 v17; // r13
  __int64 *v18; // rdi
  __int64 v19; // r12
  __int64 v20; // r15
  __int64 v21; // rbp
  __int64 v22; // rdx
  __int64 v23; // rbp
  __int64 v24; // rbp
  __int64 v25; // r10
  __int64 v26; // rdi
  __int64 v27; // r8
  bool v28; // dl
  __int64 v29; // rax
  void *v30; // rdx
  const char *v31; // rax
  __int64 v32; // rax
  _BYTE *v33; // rcx
  __int64 v35; // [rsp+20h] [rbp-68h]
  void *input; // [rsp+30h] [rbp-58h]
  unsigned __int64 strlen; // [rsp+40h] [rbp-48h]
  unsigned __int64 v38; // [rsp+48h] [rbp-40h]

  v0 = 0;
  strlen = 0i64;
  v38 = 15i64;
  LOBYTE(input) = 0;
  LODWORD(v1) = printf(std::cout, "I'm a first timer of Logic algebra , how about you?");
  std::basic_ostream<char,std::char_traits<char>>::operator<<(v1, cout);
  printf(std::cout, "Let's start our game,Please input your flag:");
  scanf(std::cin, &input);
  std::basic_ostream<char,std::char_traits<char>>::operator<<(std::cout, cout);
  if ( strlen - 5 > 0x19 )
  {
    LODWORD(v32) = printf(std::cout, "Wrong input ,no GXY{} in input words");
    std::basic_ostream<char,std::char_traits<char>>::operator<<(v32, cout);
    goto LABEL_45;
  }
  v2 = (unsigned __int8 *)sub_7FF7BDA624C8(0x20ui64);
  data1 = v2;
  if ( v2 )
  {
    *(_QWORD *)v2 = 0i64;
    *((_QWORD *)v2 + 1) = 0i64;
    *((_QWORD *)v2 + 2) = 0i64;
    *((_QWORD *)v2 + 3) = 0i64;
  }
  else
  {
    data1 = 0i64;
  }
  cnt = 0;
  if ( strlen > 0 )
  {
    cnt_ = 0i64;
    do
    {
      inputs = &input;
      if ( v38 >= 0x10 )
        inputs = input;
      halt = &Dst;
      if ( (unsigned __int64)qword_7FF7BDA66060 >= 0x10 )
        halt = (void **)Dst;
      data1[cnt_] = inputs[cnt_] ^ *((_BYTE *)halt + cnt++ % 27);
      ++cnt_;
    }
    while ( cnt < strlen );
  }
  byteNow = 0i64;
  v9 = 0i64;
  v10 = 0i64;
  v11 = 0i64;
  if ( (signed int)strlen > 30 )
    goto LABEL_28;
  cnt1 = 0;
  if ( (signed int)strlen <= 0 )
    goto LABEL_28;
  data1_ = data1;
  do
  {
    bytes = *data1_ + byteNow;
    ++cnt1;
    ++data1_;
    switch ( cnt1 )
    {
      case 8:
        v11 = bytes;
        goto LABEL_24;
      case 16:
        v10 = bytes;
        goto LABEL_24;
      case 24:
        v9 = bytes;
LABEL_24:
        bytes = 0i64;
        break;
      case 32:
        printf(std::cout, "ERRO,out of range");
        exit(1);
        break;
    }
    byteNow = bytes << 8;
  }
  while ( cnt1 < (signed int)strlen );
  if ( v11 )
  {
    v15 = (__int64 *)sub_7FF7BDA624C8(0x20ui64);
    *v15 = v11;
    v15[1] = v10;
    v15[2] = v9;
    v15[3] = byteNow;
    goto LABEL_29;
  }
LABEL_28:
  v15 = 0i64;
LABEL_29:
  v35 = v15[2];
  v16 = v15[1];
  v17 = *v15;
  v18 = (__int64 *)sub_7FF7BDA6223C(0x20ui64);
  if ( IsDebuggerPresent() )
  {
    printf(std::cout, "Hi , DO not debug me !");
    Sleep(0x7D0u);
    exit(0);
  }
  v19 = v16 & v17;
  *v18 = v16 & v17;
  v20 = v35 & ~v17;
  v18[1] = v20;
  v21 = ~v16;
  v22 = v35 & v21;
  v18[2] = v35 & v21;
  v23 = v17 & v21;
  v18[3] = v23;
  if ( v20 != 1176889593874i64 )
  {
    v18[1] = 0i64;
    v20 = 0i64;
  }
  v24 = v20 | v19 | v22 | v23;
  v25 = v15[1];
  v26 = v15[2];
  v27 = v22 & *v15 | v26 & (v19 | v25 & ~*v15 | ~(v25 | *v15));
  v28 = 0;
  if ( v27 == 577031497978884115i64 )
    v28 = v24 == 4483974544037412639i64;
  if ( (v24 ^ v15[3]) == 4483974543195470111i64 )
    v0 = v28;
  if ( (v20 | v19 | v25 & v26) != (~*v15 & v26 | 0xC00020130082C0Ci64) || v0 != 1 )
  {
    printf(std::cout, "Wrong answer!try again");
    j_j_free(data1);
  }
  else
  {
    LODWORD(v29) = printf(std::cout, "Congratulations!flag is GXY{");
    v30 = &input;
    if ( v38 >= 0x10 )
      v30 = input;
    v31 = (const char *)sub_7FF7BDA61FD0(v29, v30, strlen);
    printf(v31, "}");
    j_j_free(data1);
  }
LABEL_45:
  if ( v38 >= 0x10 )
  {
    v33 = input;
    if ( v38 + 1 >= 0x1000 )
    {
      v33 = (_BYTE *)*((_QWORD *)input - 1);
      if ( (unsigned __int64)((_BYTE *)input - v33 - 8) > 0x1F )
        invalid_parameter_noinfo_noreturn();
    }
    j_j_free(v33);
  }
  return 0i64;
}

就是对输入的数同i_will_check_is_debug_or_not进行xor之后，得到的东西转化为hex之后直接进行一堆位运算得到结果，写个z3 看看

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
from z3 import *
import binascii
key = 'i_will_check_is_debug_or_not'

s = Solver()
x = BitVec('x', 64)
y = BitVec('y', 64)
z = BitVec('z', 64)
k = BitVec('k', 64)
xAndY = y & x
zAndNorX = z & ~x
norY = ~y
zAndNorY = z & ~y
xAndNorY = x & ~y
s.add(zAndNorX == 0x11204161012)
bigSum = zAndNorX | xAndY | zAndNorY | xAndNorY
bigSum2 = zAndNorY & x | z & (xAndY | y & (~x) | ~(y | x))
s.add(bigSum2 == 0x8020717153E3013)
s.add(bigSum == 4483974544037412639)
s.add((bigSum ^ k) == 4483974543195470111)
s.add((zAndNorX | xAndY | y & z) == ((~x) & z | 0xC00020130082C0C))
print(s.check())

m = s.model()
out = []
x = m[x]
y = m[y]
z = m[z]
k = m[k]

out.append(x)
out.append(y)
out.append(z)
out.append(k)
s = []
for i in range(len(out)):
    h = hex(int(str(out[i]), 10))[2:]
    h = h.zfill(len(h) + (len(h))%2)
    print(h)
    out[i] = binascii.unhexlify(h)
    s += list(out[i])
for i in range(len(s)):
    s[i] ^= ord(key[i%27])

print(''.join([chr(x) for x in s]))

We1l_D0ndeajoa_Slgebra_am_ii

明显不对啊这个，看了一下官方的wp，他的y直接硬给出来了可还行，而且这个k我手动解出来和官方给的也不一样，有点坑哦

之后看了看别人的wp，发现原来在比赛时发公告给了第二部分为e!P0or_a

hhhh，你高兴就好

flagWe1l_D0ne!P0or_algebra_am_ii

WUSTCTF level2

upx加壳的linux x86 文件，脱了

看一下汇编就出来

wctf2020{Just_upx_-d}

BabyDriver

下载下来是个sys文件，拖进IDA看看，发现一幅地图，迷宫题，找到主函数

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
__int64 __fastcall sub_140001380(__int64 a1, __int64 a2)
{
  __int64 v2; // rbx
  __int64 v3; // rdi
  __int64 v4; // rax
  int position; // ecx
  __int16 *inputS; // rsi
  __int64 v7; // rbp
  __int16 inputTrans; // dx
  char v9; // dl
  CHAR *v10; // rcx

  v2 = a2;
  if ( *(_DWORD *)(a2 + '0') >= 0 )
  {
    v3 = *(_QWORD *)(a2 + 24);
    v4 = *(_QWORD *)(a2 + 56) >> 3;
    if ( (_DWORD)v4 )
    {
      position = pos;
      inputS = (__int16 *)(v3 + 2);
      v7 = (unsigned int)v4;
      while ( *(_WORD *)(v3 + 4) )
      {
LABEL_28:
        inputS += 6;
        if ( !--v7 )
          goto ret;
      }
      map[position] = '.';
      inputTrans = *inputS;
      if ( *inputS == 23 )
      {
        if ( position & 0xFFFFFFF0 )
        {
          position -= 0x10;
          goto LABEL_21;
        }
        position += 0xD0;
        pos = position;
      }
      if ( inputTrans == 37 )
      {
        if ( (position & 0xFFFFFFF0) != 0xD0 )
        {
          position += 0x10;
          goto LABEL_21;
        }
        position -= 0xD0;
        pos = position;
      }
      if ( inputTrans == 36 )
      {
        if ( position & 0xF )
        {
          --position;
          goto LABEL_21;
        }
        position += 15;
        pos = position;
      }
      if ( inputTrans != 38 )
        goto LABEL_22;
      if ( (position & 0xF) == 15 )
        position -= 15;
      else
        ++position;
LABEL_21:
      pos = position;
LABEL_22:
      v9 = map[position];
      if ( v9 == '*' )
      {
        v10 = "failed!\n";
      }
      else
      {
        if ( v9 != '#' )
        {
LABEL_27:
          map[position] = 'o';
          goto LABEL_28;
        }
        v10 = "success! flag is flag{md5(input)}\n";
      }
      pos = 16;
      DbgPrint(v10);
      position = pos;
      goto LABEL_27;
    }
  }
ret:
  if ( *(_BYTE *)(v2 + 65) )
    *(_BYTE *)(*(_QWORD *)(v2 + 184) + 3i64) |= 1u;
  return *(unsigned int *)(v2 + 48);
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
****************0x0
o.*..*......*..*0x1
*.**...**.*.*.**0x2
*.****.**.*.*.**0x3
*...**....*.*.**0x4
***..***.**.*..*0x5
*.**.***.**.**.*0x6
*.**.******.**.*0x7
*.**....***.**.*0x8
*.*****.***....*0x9
*...***.********0xa
**..***......#**0xb
**.*************0xc
****************0xd

这个输入明显不是能够手动输入的啊，看一下别人的WP之后，键盘扫描码??? 那我康康

不知道从哪儿找到的这张表，对照一下，就出了

1
2
3
4
I -> ↑
J -> ←
K -> ↓
L -> →

LKKKLLKLKKKLLLKKKLLLLLL

pic

[FlareOn] Overlong

函数真的超简单，运行起来也不让你输入flag什么的，就三个函数，加密弹窗

1
2
3
4
5
6
7
8
9
10
11
12
int __stdcall start(int a1, int a2, int a3, int a4)
{
  unsigned int end; // eax
  char Text[128]; // [esp+0h] [ebp-84h]
  unsigned int v7; // [esp+80h] [ebp-4h]

  end = decrypt(Text, (int)&data, 0x1Cu);
  v7 = end;
  Text[end] = 0;
  MessageBoxA(0, Text, Caption, 0);
  return 0;
}

这个解密函数看了一大堆，不太明白，data后面有一大串，给patch成Text长度128，跑一下，发现啥也没弹出

死活弹不出，于是查看data长度，把0x1c给patch成0xaf，出了，原来不应该在外面改汇编，会覆盖掉后面的push offset data直接在函数里面改一下eax就行，直接出了

I_a_M_t_h_e_e_n_C_o_D_i_n_g@flare-on.com

[MRCTF] Xor

读取字符串找到关键函数，发现无法F5，直接撸汇编

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
.text:00401090 sub_401090      proc near               ; CODE XREF: start-8D↓p
.text:00401090                 push    offset aGiveMeYourFlag ; "Give Me Your Flag String:\n"
.text:00401095                 call    sub_401020
.text:0040109A                 push    64h
.text:0040109C                 push    offset byte_4212C0
.text:004010A1                 push    offset aS       ; "%s"
.text:004010A6                 call    sub_401050
.text:004010AB                 mov     edx, offset byte_4212C0
.text:004010B0                 add     esp, 10h
.text:004010B3                 lea     ecx, [edx+1]
.text:004010B6
.text:004010B6 loc_4010B6:                             ; CODE XREF: sub_401090+2B↓j
.text:004010B6                 mov     al, [edx]
.text:004010B8                 inc     edx
.text:004010B9                 test    al, al
.text:004010BB                 jnz     short loc_4010B6
.text:004010BD                 sub     edx, ecx
.text:004010BF                 cmp     edx, 1Bh
.text:004010C2                 jnz     short loc_4010FF
.text:004010C4                 xor     eax, eax
.text:004010C6                 db      66h, 66h
.text:004010C6                 nop     word ptr [eax+eax+00000000h]
.text:004010D0
.text:004010D0 loc_4010D0:                             ; CODE XREF: sub_401090+53↓j
.text:004010D0                 mov     cl, byte_4212C0[eax]
.text:004010D6                 xor     cl, al
.text:004010D8                 cmp     cl, ds:byte_41EA08[eax]
.text:004010DE                 jnz     short loc_4010FF
.text:004010E0                 inc     eax
.text:004010E1                 cmp     eax, edx
.text:004010E3                 jb      short loc_4010D0
.text:004010E5                 push    offset aRight   ; "Right!\n"
.text:004010EA                 call    sub_401020
.text:004010EF                 push    offset aPause   ; "pause"
.text:004010F4                 call    sub_404B7E
.text:004010F9                 add     esp, 8
.text:004010FC                 xor     eax, eax
.text:004010FE                 retn
.text:004010FF ; ---------------------------------------------------------------------------
.text:004010FF
.text:004010FF loc_4010FF:                             ; CODE XREF: sub_401090+32↑j
.text:004010FF                                         ; sub_401090+4E↑j
.text:004010FF                 push    offset aWrong   ; "Wrong!\n"
.text:00401104                 call    sub_401020
.text:00401109                 push    offset aPause   ; "pause"
.text:0040110E                 call    sub_404B7E
.text:00401113                 add     esp, 8
.text:00401116                 push    0               ; uExitCode
.text:00401118                 call    sub_40355F
.text:0040111D                 int     3               ; Trap to Debugger
.text:0040111D sub_401090      endp

主要逻辑比较简单，他给你塞了几个花指令让你无法逆向，其实也很简单，nop掉就行，对每一位进行按index异或，跑一下就出来了

1
2
3
4
5
s = 'MSAWB~FXZ:J:`tQJ"N@ bpdd}8g'
s = [ord(x) for x in s]
for i in range(len(s)):
    s[i] ^= i
print(''.join([chr(x) for x in s]))

MRCTF{@_R3@1ly_E2_R3verse!}

[MRCTF2020] hello_world_go

是用go编译的，好在没有去符号，拖进IDA，查看main_main函数

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
__int64 __fastcall main_main(__int64 a1, __int64 a2)
{
  __int64 v2; // r8
  __int64 v3; // r9
  __int64 v4; // r8
  __int64 v5; // r9
  __int64 v6; // rdx
  __int64 v7; // r8
  __int64 strlen; // rcx
  __int64 v9; // rdx
  __int64 v10; // r9
  signed __int64 v11; // rax
  __int64 result; // rax
  __int64 v13; // ST58_8
  __int64 *v14; // [rsp+8h] [rbp-A8h]
  char v15; // [rsp+18h] [rbp-98h]
  __int64 *v16; // [rsp+60h] [rbp-50h]
  __int128 v17; // [rsp+68h] [rbp-48h]
  __int128 v18; // [rsp+78h] [rbp-38h]
  __int128 v19; // [rsp+88h] [rbp-28h]
  __int128 v20; // [rsp+98h] [rbp-18h]

  if ( (unsigned __int64)&v18 + 8 <= *(_QWORD *)(__readfsqword(0xFFFFFFF8) + 16) )
    runtime_morestack_noctxt(a1, a2);
  runtime_newobject(a1, a2);
  v16 = v14;
  *(_QWORD *)&v20 = &unk_4AC9C0;
  *((_QWORD *)&v20 + 1) = &off_4EA530;
  fmt_Fprint(a1, a2, (__int64)&v20, (__int64)&unk_4AC9C0, v2, v3, (__int64)&go_itab__os_File_io_Writer, os_Stdout);
  *(_QWORD *)&v19 = &unk_4A96A0;
  *((_QWORD *)&v19 + 1) = v16;
  fmt_Fscanf(
    a1,
    a2,
    (__int64)&go_itab__os_File_io_Reader,
    (__int64)&v19,
    v4,
    v5,
    (__int64)&go_itab__os_File_io_Reader,
    os_Stdin,
    (__int64)&unk_4D07C9,
    2LL);
  strlen = v16[1];
  if ( strlen != 24 )
    goto LABEL_3;
  v13 = *v16;
  runtime_memequal(a1, a2, v6, (unsigned __int64)&unk_4D3C58);
  if ( !v15 )
  {
    strlen = 24LL;
LABEL_3:
    runtime_cmpstring(a1, a2, (__int64)&unk_4D3C58, strlen, v7);
    if ( (signed __int64)&v19 >= 0 )
      v11 = 1LL;
    else
      v11 = -1LL;
    goto LABEL_5;
  }
  v11 = 0LL;
LABEL_5:
  if ( v11 )
  {
    *(_QWORD *)&v17 = &unk_4AC9C0;
    *((_QWORD *)&v17 + 1) = &off_4EA550;
    result = fmt_Fprintln(
               a1,
               a2,
               v9,
               (__int64)&go_itab__os_File_io_Writer,
               v7,
               v10,
               (__int64)&go_itab__os_File_io_Writer,
               os_Stdout);
  }
  else
  {
    *(_QWORD *)&v18 = &unk_4AC9C0;
    *((_QWORD *)&v18 + 1) = &off_4EA540;
    result = fmt_Fprintln(
               a1,
               a2,
               v9,
               (__int64)&go_itab__os_File_io_Writer,
               v7,
               v10,
               (__int64)&go_itab__os_File_io_Writer,
               os_Stdout);
  }
  return result;
}

IDA反编译的go真的是又臭又长，而且只能赢看，就跟踪呗，好在跟着跟着就有了，flag在runtime_cmpstring(a1, a2, (__int64)&unk_4D3C58, strlen, v7);这一句对比直接就出来了

flag{hello_world_gogogo}

[WUSTCTF]level3

变表base64，中间有个变换的过程，懒得看了直接动态出结果

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
__int64 O_OLookAtYou()
{
  char v0; // ST03_1
  __int64 result; // rax
  signed int i; // [rsp+2h] [rbp-4h]

  for ( i = 0; i <= 9; ++i )
  {
    v0 = base64_table[i];
    base64_table[i] = base64_table[19 - i];
    result = 19 - i;
    base64_table[result] = v0;
  }
  return result;
}

写个脚本

1
2
3
4
5
6
7
8
9
10
11
12
import base64

afterTable = 'TSRQPONMLKJIHGFEDCBAUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/'
table = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/'
cipher = 'd2G0ZjLwHjS7DmOzZAY0X2lzX3CoZV9zdNOydO9vZl9yZXZlcnGlfD=='
Acipher = ''
for i in cipher:
    index = afterTable.find(i)
    Acipher += str(table[index])

s = base64.b64decode(Acipher.encode())
print(s)

wctf2020{Base64_is_the_start_of_reverse}

WUSTCTF CrossFun

一堆直接给flag 的函数

1
2
3
4
5
6
7
8
9
_BOOL8 __fastcall iven_1s_brave(_BYTE *a1)
{
  return a1[15] == 100
      && a1[8] == 123
      && a1[18] == 51
      && a1[28] == 95
      && a1[21] == 114
      && (unsigned int)iven_1s_great(a1);
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
a1 = [0]*40
a1[10] = 112
a1[13] = 64
a1[3] = 102
a1[26] = 114
a1[20] = 101
a1[7] = 48
a1[16] = 95
a1[11] = 112
a1[23] = 101
a1[30] = 117
a1[0] = 119 
a1[6] = 50
a1[22] = 115
a1[31] = 110
a1[12] = 95
a1[15] = 100
a1[8] = 123
a1[18] = 51
a1[28] = 95
a1[21] = 114
a1[2] = 116
a1[9] = 99
a1[32] = 125
a1[19] = 118
a1[5] = 48
a1[14] = 110
a1[4] = 50
a1[17] = 114
a1[29] = 102
a1[17] = 114
a1[24] = 95
a1[1] = 99
a1[25] = 64
a1[27] = 101
print(''.join([chr(x) for x in a1]))

wctf2020{cpp_@nd_r3verse_@re_fun}

[2019 红帽杯]xx

看了一下是个x64的exe，cpp写的，去符号了，main里面流程非常长，有够阴间的，这种按位检验，可以用pintools给爆破出来么

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
__int64 __fastcall sub_1400011A0(__int64 a1, __int64 a2)
{
  unsigned __int64 inputLength; // rbx
  signed __int64 strlen; // rax
  __int128 *v4; // rax
  __int64 Table; // r11
  __int128 *head4; // r14
  int v7; // edi
  __int128 *v8; // rsi
  char chr; // r10
  int idx; // edx
  __int64 v11; // r8
  unsigned __int64 tableLen; // rcx
  signed __int64 v13; // rcx
  unsigned __int64 cnt; // rax
  unsigned __int64 i; // rax
  _BYTE *v16; // rax
  size_t v17; // rsi
  _BYTE *v18; // rbx
  _BYTE *afterTrans; // r9
  signed int index_; // er11
  char *current_chr; // r8
  signed __int64 v22; // rcx
  char chr_change; // al
  signed __int64 v24; // r9
  signed __int64 index; // rdx
  __int64 v26; // rax
  size_t Size; // [rsp+20h] [rbp-48h]
  __int128 strhead4; // [rsp+28h] [rbp-40h]
  int v30; // [rsp+38h] [rbp-30h]
  int v31; // [rsp+3Ch] [rbp-2Ch]
  int input[4]; // [rsp+40h] [rbp-28h]
  int v33; // [rsp+50h] [rbp-18h]

  *(_OWORD *)input = 0i64;
  v33 = 0;
  scan(std::cin, a2, input);
  inputLength = -1i64;
  strlen = -1i64;
  do
    ++strlen;
  while ( *((_BYTE *)input + strlen) );
  if ( strlen != 19 )
  {
    print(std::cout, "error\n");
    _exit((unsigned __int64)input);
  }
  v4 = (__int128 *)sub_140001E5C(5ui64);
  Table = *(_QWORD *)&table;
  head4 = v4;
  v7 = 0;
  v8 = v4;
  do
  {
    chr = *((_BYTE *)v8 + (char *)input - (char *)v4);
    idx = 0;
    *(_BYTE *)v8 = chr;
    v11 = 0i64;
    tableLen = -1i64;
    do
      ++tableLen;
    while ( *(_BYTE *)(Table + tableLen) );
    if ( tableLen )
    {
      do
      {
        if ( chr == *(_BYTE *)(Table + v11) )   // idx = findstr(chr, table)
          break;
        ++idx;
        ++v11;
      }
      while ( idx < tableLen );
    }
    v13 = -1i64;
    do
      ++v13;
    while ( *(_BYTE *)(Table + v13) );
    if ( idx == v13 )
      _exit(Table);
    v8 = (__int128 *)((char *)v8 + 1);
  }
  while ( (char *)v8 - (char *)v4 < 4 );        // 检测前4个是键盘ascii字母
  *((_BYTE *)v4 + 4) = 0;
  do
    ++inputLength;
  while ( *((_BYTE *)input + inputLength) );
  cnt = 0i64;
  strhead4 = *head4;
  while ( *((_BYTE *)&strhead4 + cnt) )
  {
    if ( !*((_BYTE *)&strhead4 + cnt + 1) )
    {
      ++cnt;
      break;
    }
    if ( !*((_BYTE *)&strhead4 + cnt + 2) )
    {
      cnt += 2i64;
      break;
    }
    if ( !*((_BYTE *)&strhead4 + cnt + 3) )
    {
      cnt += 3i64;
      break;
    }
    cnt += 4i64;
    if ( cnt >= 0x10 )
      break;
  }
  for ( i = cnt + 1; i < 0x10; ++i )
    *((_BYTE *)&strhead4 + i) = 0;
  v16 = xxtea((__int64)input, inputLength, (unsigned __int8 *)&strhead4, &Size);
  v17 = Size;
  v18 = v16;
  afterTrans = sub_140001E5C(Size);
  index_ = 1;
  *afterTrans = v18[2];
  current_chr = afterTrans + 1;
  afterTrans[1] = *v18;
  afterTrans[2] = v18[3];
  afterTrans[3] = v18[1];
  afterTrans[4] = v18[6];
  afterTrans[5] = v18[4];
  afterTrans[6] = v18[7];
  afterTrans[7] = v18[5];
  afterTrans[8] = v18[10];
  afterTrans[9] = v18[8];
  afterTrans[10] = v18[11];
  afterTrans[11] = v18[9];
  afterTrans[12] = v18[14];
  afterTrans[13] = v18[12];
  afterTrans[14] = v18[15];
  afterTrans[15] = v18[13];
  afterTrans[16] = v18[18];
  afterTrans[17] = v18[16];
  afterTrans[18] = v18[19];
  afterTrans[19] = v18[17];
  afterTrans[20] = v18[22];
  afterTrans[21] = v18[20];
  afterTrans[22] = v18[23];
  for ( afterTrans[23] = v18[21]; index_ < v17; ++current_chr )
  {
    v22 = 0i64;
    if ( index_ / 3 > 0 )
    {
      chr_change = *current_chr;
      do
      {
        chr_change ^= afterTrans[v22++];
        *current_chr = chr_change;
      }
      while ( v22 < index_ / 3 );
    }
    ++index_;
  }
  *(_QWORD *)&strhead4 = 0xC0953A7C6B40BCCEi64;
  v24 = afterTrans - (_BYTE *)&strhead4;
  *((_QWORD *)&strhead4 + 1) = 0x3502F79120209BEFi64;
  index = 0i64;
  v30 = 0xC8021823;
  v31 = 0xFA5656E7;
  do
  {
    if ( *((_BYTE *)&strhead4 + index) != *((_BYTE *)&strhead4 + index + v24) )// afterTrans 和 固定值进行比较
      _exit(v7 * v7);
    ++v7;
    ++index;
  }
  while ( index < 24 );
  v26 = print(std::cout, "You win!");
  std::basic_ostream<char,std::char_traits<char>>::operator<<(v26, sub_1400017F0);
  return 0i64;
}

给爷逆向了两天，终于理清了逻辑

  • 首先把你的输入前4个字母进行比较，如果是字母表里面的就继续，反之就exit
  • 然后把输入的前4个字母变成密钥
  • 使用密钥进行XXTEA加密
  • 进行置换
  • 对比

然后知道原理之后直接写脚本，pintools也没爆破出来，看原理只能爆破出前面4个是字母，其余爆破不出来

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
import struct  

data = [
  0xCE, 0xBC, 0x40, 0x6B, 0x7C, 0x3A, 0x95, 0xC0, 0xEF, 0x9B, 
  0x20, 0x20, 0x91, 0xF7, 0x02, 0x35, 0x23, 0x18, 0x02, 0xC8, 
  0xE7, 0x56, 0x56, 0xFA
]
print(data)
for i in range(0x18 - 1, 0, -1):
    idx = 0
    if(i // 3 > 0):
        while(idx < i//3):
            data[i] ^= data[idx]
            idx += 1

table = [1, 3, 0, 2, 5, 7, 4, 6, 9, 11, 8, 10, 13, 15, 12, 14, 17, 19, 16, 18, 21, 23, 20, 22]
afterTable = []
for i in table:
  afterTable.append(data[i])

data = afterTable
  
_DELTA = 0x9E3779B9  
  
def _long2str(v, w):  
    n = (len(v) - 1) << 2  
    if w:  
        m = v[-1]  
        if (m < n - 3) or (m > n): return ''  
        n = m  
    s = struct.pack('<%iL' % len(v), *v)  
    return s[0:n] if w else s  
  
def _str2long(s, w):  
    n = len(s)  
    m = (4 - (n & 3) & 3) + n  

    v = list(struct.unpack('<%iL' % (m >> 2), s))  
    if w: v.append(n)  
    return v  
  
def encrypt(str, key):  
    if str == '': return str  
    v = _str2long(str, True)  
    k = _str2long(key.ljust(16, "\0"), False)  
    n = len(v) - 1  
    z = v[n]  
    y = v[0]  
    sum = 0  
    q = 6 + 52 // (n + 1)  
    while q > 0:  
        sum = (sum + _DELTA) & 0xffffffff  
        e = sum >> 2 & 3  
        for p in range(n):  
            y = v[p + 1]  
            v[p] = (v[p] + ((z >> 5 ^ y << 2) + (y >> 3 ^ z << 4) ^ (sum ^ y) + (k[p & 3 ^ e] ^ z))) & 0xffffffff  
            z = v[p]  
        y = v[0]  
        v[n] = (v[n] + ((z >> 5 ^ y << 2) + (y >> 3 ^ z << 4) ^ (sum ^ y) + (k[n & 3 ^ e] ^ z))) & 0xffffffff  
        z = v[n]  
        q -= 1  
    return _long2str(v, False)  
  
def decrypt(str, key):  
    if str == '': return str  
    v = _str2long(str, False)  
    k = _str2long(key, False)  
    n = len(v) - 1  
    z = v[n]  
    y = v[0]  
    q = 6 + 52 // (n + 1)  
    sum = (q * _DELTA) & 0xffffffff  
    while (sum != 0):  
        e = sum >> 2 & 3  
        for p in range(n, 0, -1):  
            z = v[p - 1]  
            v[p] = (v[p] - ((z >> 5 ^ y << 2) + (y >> 3 ^ z << 4) ^ (sum ^ y) + (k[p & 3 ^ e] ^ z))) & 0xffffffff  
            y = v[p]  
        z = v[n]  
        v[0] = (v[0] - ((z >> 5 ^ y << 2) + (y >> 3 ^ z << 4) ^ (sum ^ y) + (k[0 & 3 ^ e] ^ z))) & 0xffffffff  
        y = v[0]  
        sum = (sum - _DELTA) & 0xffffffff  
    return _long2str(v, True)  
  
de = decrypt(bytes(data), bytes([ord(x) for x in 'flag'] + [0]*12))
print(de)

网上找了个脚本跑一下，直接出来了

flag{CXX_and_++tea}

equation

啊这，我没学过js啊，而且一堆括号我看个🔨哦

找WP，然后发现一个js的轮子，用PyExecJs跑一遍，得到一堆方程组，看样子就是用Z3

1
2
3
4
5
6
7
    function deEquation(str) {
  for (let i = 0; i <= 1; i++) {
  str = str.replace(/l\[(\D*?)](\+l|-l|==)/g, (m, a, b) => 'l[' + eval(a) + ']' + b);
  }
  str = str.replace(/==(\D*?)&&/g, (m, a) => '==' + eval(a) + '&&');
  return str;
}

这个轮子最后解不出一小段

1
+(!+[]+!+[]+!+[]+!+[]+!+[]+!+[]+!+[]+!+[]+[+!+[]])

找到这个网站http://codertab.com/JsUnFuck

解出来是81

这么长一大串电脑都卡死了，太恶心了，然后是一堆方程组

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
l[40]+l[35]+l[34]-l[0]-l[15]-l[37]+l[7]+l[6]-l[26]+l[20]+l[19]+l[8]-l[17]-l[14]-l[38]+l[1]-l[9]+l[22]+l[41]+l[3]-l[29]-l[36]-l[25]+l[5]+l[32]-l[16]+l[12]-l[24]+l[30]+l[39]+l[10]+l[2]+l[27]+l[28]+l[21]+l[33]-l[18]+l[4]==861
l[31]+l[26]+l[11]-l[33]+l[27]-l[3]+l[12]+l[30]+l[1]+l[32]-l[16]+l[7]+l[10]-l[25]+l[38]-l[41]-l[14]-l[19]+l[29]+l[36]-l[9]-l[28]-l[6]-l[0]-l[22]-l[18]+l[20]-l[37]+l[4]-l[24]+l[34]-l[21]-l[39]-l[23]-l[8]-l[40]+l[15]-l[35]==-448
l[26]+l[14]+l[15]+l[9]+l[13]+l[30]-l[11]+l[18]+l[23]+l[7]+l[3]+l[12]+l[25]-l[24]-l[39]-l[35]-l[20]+l[40]-l[8]+l[10]-l[5]-l[33]-l[31]+l[32]+l[19]+l[21]-l[6]+l[1]+l[16]+l[17]+l[29]+l[22]-l[4]-l[36]+l[41]+l[38]+l[2]+l[0]==1244
l[5]+l[22]+l[15]+l[2]-l[28]-l[10]-l[3]-l[13]-l[18]+l[30]-l[9]+l[32]+l[19]+l[34]+l[23]-l[17]+l[16]-l[7]+l[24]-l[39]+l[8]-l[12]-l[40]-l[25]+l[37]-l[35]+l[11]-l[14]+l[20]-l[27]+l[4]-l[33]-l[21]+l[31]-l[6]+l[1]+l[38]-l[29]==-39
l[41]-l[29]+l[23]-l[4]+l[20]-l[33]+l[35]+l[3]-l[19]-l[21]+l[11]+l[26]-l[24]-l[17]+l[37]+l[1]+l[16]-l[0]-l[13]+l[7]+l[10]+l[14]+l[22]+l[39]-l[40]+l[34]-l[38]+l[32]+l[25]-l[2]+l[15]+l[6]+l[28]-l[8]-l[5]-l[31]-l[30]-l[27]==485
l[13]+l[19]+l[21]-l[2]-l[33]-l[0]+l[39]+l[31]-l[23]-l[41]+l[38]-l[29]+l[36]+l[24]-l[20]-l[9]-l[32]+l[37]-l[35]+l[40]+l[7]-l[26]+l[15]-l[10]-l[6]-l[16]-l[4]-l[5]-l[30]-l[14]-l[22]-l[25]-l[34]-l[17]-l[11]-l[27]+l[1]-l[28]==-1068
l[32]+l[0]+l[9]+l[14]+l[11]+l[18]-l[13]+l[24]-l[2]-l[15]+l[19]-l[21]+l[1]+l[39]-l[8]-l[3]+l[33]+l[6]-l[5]-l[35]-l[28]+l[25]-l[41]+l[22]-l[17]+l[10]+l[40]+l[34]+l[27]-l[20]+l[23]+l[31]-l[16]+l[7]+l[12]-l[30]+l[29]-l[4]==939
l[19]+l[11]+l[20]-l[16]+l[40]+l[25]+l[1]-l[31]+l[28]-l[23]+l[14]-l[9]-l[27]+l[35]+l[39]-l[37]-l[8]-l[22]+l[5]-l[6]+l[0]-l[32]+l[24]+l[33]+l[29]+l[38]+l[15]-l[2]+l[30]+l[7]+l[12]-l[3]-l[17]+l[34]+l[41]-l[4]-l[13]-l[26]==413
l[22]+l[4]-l[9]+l[34]+l[35]+l[17]+l[3]-l[24]+l[38]-l[5]-l[41]-l[31]-l[0]-l[25]+l[33]+l[15]-l[1]-l[10]+l[16]-l[29]-l[12]+l[26]-l[39]-l[21]-l[18]-l[6]-l[40]-l[13]+l[8]+l[37]+l[19]+l[14]+l[32]+l[28]-l[11]+l[23]+l[36]+l[7]==117
l[32]+l[16]+l[3]+l[11]+l[34]-l[31]+l[14]+l[25]+l[1]-l[30]-l[33]-l[40]-l[4]-l[29]+l[18]-l[27]+l[13]-l[19]-l[12]+l[23]-l[39]-l[41]-l[8]+l[22]-l[5]-l[38]-l[9]-l[37]+l[17]-l[36]+l[24]-l[21]+l[2]-l[26]+l[20]-l[7]+l[35]-l[0]==-313
l[40]-l[1]+l[5]+l[7]+l[33]+l[29]+l[12]+l[38]-l[31]+l[2]+l[14]-l[35]-l[8]-l[24]-l[39]-l[9]-l[28]+l[23]-l[17]-l[22]-l[26]+l[32]-l[11]+l[4]-l[36]+l[10]+l[20]-l[18]-l[16]+l[6]-l[0]+l[3]-l[30]+l[37]-l[19]+l[21]+l[25]-l[15]==-42
l[21]+l[26]-l[17]-l[25]+l[27]-l[22]-l[39]-l[23]-l[15]-l[20]-l[32]+l[12]+l[3]-l[6]+l[28]+l[31]+l[13]-l[16]-l[37]-l[30]-l[5]+l[41]+l[29]+l[36]+l[1]+l[11]+l[24]+l[18]-l[40]+l[19]-l[35]+l[2]-l[38]+l[14]-l[9]+l[4]+l[0]-l[33]==289
l[29]+l[31]+l[32]-l[17]-l[7]+l[34]+l[2]+l[14]+l[23]-l[4]+l[3]+l[35]-l[33]-l[9]-l[20]-l[37]+l[24]-l[27]+l[36]+l[15]-l[18]-l[0]+l[12]+l[11]-l[38]+l[6]+l[22]+l[39]-l[25]-l[10]-l[19]-l[1]+l[13]-l[41]+l[30]-l[16]+l[28]-l[26]==-117
l[5]+l[37]-l[39]+l[0]-l[27]+l[12]+l[41]-l[22]+l[8]-l[16]-l[38]+l[9]+l[15]-l[35]-l[29]+l[18]+l[6]-l[25]-l[28]+l[36]+l[34]+l[32]-l[14]-l[1]+l[20]+l[40]-l[19]-l[4]-l[7]+l[26]+l[30]-l[10]+l[13]-l[21]+l[2]-l[23]-l[3]-l[33]==-252
l[29]+l[10]-l[41]-l[9]+l[12]-l[28]+l[11]+l[40]-l[27]-l[8]+l[32]-l[25]-l[23]+l[39]-l[1]-l[36]-l[15]+l[33]-l[20]+l[18]+l[22]-l[3]+l[6]-l[34]-l[21]+l[19]+l[26]+l[13]-l[4]+l[7]-l[37]+l[38]-l[2]-l[30]-l[0]-l[35]+l[5]+l[17]==-183
l[6]-l[8]-l[20]+l[34]-l[33]-l[25]-l[4]+l[3]+l[17]-l[13]-l[15]-l[40]+l[1]-l[30]-l[14]-l[28]-l[35]+l[38]-l[22]+l[2]+l[24]-l[29]+l[5]+l[9]+l[37]+l[23]-l[18]+l[19]-l[21]+l[11]+l[36]+l[41]-l[7]-l[32]+l[10]+l[26]-l[0]+l[31]==188
l[3]+l[6]-l[41]+l[10]+l[39]+l[37]+l[1]+l[8]+l[21]+l[24]+l[29]+l[12]+l[27]-l[38]+l[11]+l[23]+l[28]+l[33]-l[31]+l[14]-l[5]+l[32]-l[17]+l[40]-l[34]+l[20]-l[22]-l[16]+l[19]+l[2]-l[36]-l[7]+l[18]+l[15]+l[26]-l[0]-l[4]+l[35]==1036
l[28]-l[33]+l[2]+l[37]-l[12]-l[9]-l[39]+l[16]-l[32]+l[8]-l[36]+l[31]+l[10]-l[4]+l[21]-l[25]+l[18]+l[24]-l[0]+l[29]-l[26]+l[35]-l[22]-l[41]-l[6]+l[15]+l[19]+l[40]+l[7]+l[34]+l[17]-l[3]-l[13]+l[5]+l[23]+l[11]-l[27]+l[1]==328
l[22]-l[32]+l[17]-l[9]+l[20]-l[18]-l[34]+l[23]+l[36]-l[35]-l[38]+l[27]+l[4]-l[5]-l[41]+l[29]+l[33]+l[0]-l[37]+l[28]-l[40]-l[11]-l[12]+l[7]+l[1]+l[2]-l[26]-l[16]-l[8]+l[24]-l[25]+l[3]-l[6]-l[19]-l[39]-l[14]-l[31]+l[10]==-196
l[11]+l[13]+l[14]-l[15]-l[29]-l[2]+l[7]+l[20]+l[30]-l[36]-l[33]-l[19]+l[31]+l[0]-l[39]-l[4]-l[6]+l[38]+l[35]-l[28]+l[34]-l[9]-l[23]-l[26]+l[37]-l[8]-l[27]+l[5]-l[41]+l[3]+l[17]+l[40]-l[10]+l[25]+l[12]-l[24]+l[18]+l[32]==7
l[34]-l[37]-l[40]+l[4]-l[22]-l[31]-l[6]+l[38]+l[13]-l[28]+l[8]+l[30]-l[20]-l[7]-l[32]+l[26]+l[1]-l[18]+l[5]+l[35]-l[24]-l[41]+l[9]-l[0]-l[2]-l[15]-l[10]+l[12]-l[36]+l[33]-l[16]-l[14]-l[25]-l[29]-l[21]+l[27]+l[3]-l[17]==-945
l[12]-l[30]-l[8]+l[20]-l[2]-l[36]-l[25]-l[0]-l[19]-l[28]-l[7]-l[11]-l[33]+l[4]-l[23]+l[10]-l[41]+l[39]-l[32]+l[27]+l[18]+l[15]+l[34]+l[13]-l[40]+l[29]-l[6]+l[37]-l[14]-l[16]+l[38]-l[26]+l[17]+l[31]-l[22]-l[35]+l[5]-l[1]==-480
l[36]-l[11]-l[34]+l[8]+l[0]+l[15]+l[28]-l[39]-l[32]-l[2]-l[27]+l[22]+l[16]-l[30]-l[3]+l[31]-l[26]+l[20]+l[17]-l[29]-l[18]+l[19]-l[10]+l[6]-l[5]-l[38]-l[25]-l[24]+l[4]+l[23]+l[9]+l[14]+l[21]-l[37]+l[13]-l[41]-l[12]+l[35]==-213
l[19]-l[36]-l[12]+l[33]-l[27]-l[37]-l[25]+l[38]+l[16]-l[18]+l[22]-l[39]+l[13]-l[7]-l[31]-l[26]+l[15]-l[10]-l[9]-l[2]-l[30]-l[11]+l[41]-l[4]+l[24]+l[34]+l[5]+l[17]+l[14]+l[6]+l[8]-l[21]-l[23]+l[32]-l[1]-l[29]-l[0]+l[3]==-386
l[0]+l[7]-l[28]-l[38]+l[19]+l[31]-l[5]+l[24]-l[3]+l[33]-l[12]-l[29]+l[32]+l[1]-l[34]-l[9]-l[25]+l[26]-l[8]+l[4]-l[10]+l[40]-l[15]-l[11]-l[27]+l[36]+l[14]+l[41]-l[35]-l[13]-l[17]-l[21]-l[18]+l[39]-l[2]+l[20]-l[23]-l[22]==-349
l[10]+l[22]+l[21]-l[0]+l[15]-l[6]+l[20]-l[29]-l[30]-l[33]+l[19]+l[23]-l[28]+l[41]-l[27]-l[12]-l[37]-l[32]+l[34]-l[36]+l[3]+l[1]-l[13]+l[18]+l[14]+l[9]+l[7]-l[39]+l[8]+l[2]-l[31]-l[5]-l[40]+l[38]-l[26]-l[4]+l[16]-l[25]==98
l[28]+l[38]+l[20]+l[0]-l[5]-l[34]-l[41]+l[22]-l[26]+l[11]+l[29]+l[31]-l[3]-l[16]+l[23]+l[17]-l[18]+l[9]-l[4]-l[12]-l[19]-l[40]-l[27]+l[33]+l[8]-l[37]+l[2]+l[15]-l[24]-l[39]+l[10]+l[35]-l[1]+l[30]-l[36]-l[25]-l[14]-l[32]==-412
l[1]-l[24]-l[29]+l[39]+l[41]+l[0]+l[9]-l[19]+l[6]-l[37]-l[22]+l[32]+l[21]+l[28]+l[36]+l[4]-l[17]+l[20]-l[13]-l[35]-l[5]+l[33]-l[27]-l[30]+l[40]+l[25]-l[18]+l[34]-l[3]-l[10]-l[16]-l[23]-l[38]+l[8]-l[14]-l[11]-l[7]+l[12]==-95
l[2]-l[24]+l[31]+l[0]+l[9]-l[6]+l[7]-l[1]-l[22]+l[8]-l[23]+l[40]+l[20]-l[38]-l[11]-l[14]+l[18]-l[36]+l[15]-l[4]-l[41]-l[12]-l[34]+l[32]-l[35]+l[17]-l[21]-l[10]-l[29]+l[39]-l[16]+l[27]+l[26]-l[3]-l[5]+l[13]+l[25]-l[28]==-379
l[19]-l[17]+l[31]+l[14]+l[6]-l[12]+l[16]-l[8]+l[27]-l[13]+l[41]+l[2]-l[7]+l[32]+l[1]+l[25]-l[9]+l[37]+l[34]-l[18]-l[40]-l[11]-l[10]+l[38]+l[21]+l[3]-l[0]+l[24]+l[15]+l[23]-l[20]+l[26]+l[22]-l[4]-l[28]-l[5]+l[39]+l[35]==861
l[35]+l[36]-l[16]-l[26]-l[31]+l[0]+l[21]-l[13]+l[14]+l[39]+l[7]+l[4]+l[34]+l[38]+l[17]+l[22]+l[32]+l[5]+l[15]+l[8]-l[29]+l[40]+l[24]+l[6]+l[30]-l[2]+l[25]+l[23]+l[1]+l[12]+l[9]-l[10]-l[3]-l[19]+l[20]-l[37]-l[33]-l[18]==1169
l[13]+l[0]-l[25]-l[32]-l[21]-l[34]-l[14]-l[9]-l[8]-l[15]-l[16]+l[38]-l[35]-l[30]-l[40]-l[12]+l[3]-l[19]+l[4]-l[41]+l[2]-l[36]+l[37]+l[17]-l[1]+l[26]-l[39]-l[10]-l[33]+l[5]-l[27]-l[23]-l[24]-l[7]+l[31]-l[28]-l[18]+l[6]==-1236
l[20]+l[27]-l[29]-l[25]-l[3]+l[28]-l[32]-l[11]+l[10]+l[31]+l[16]+l[21]-l[7]+l[4]-l[24]-l[35]+l[26]+l[12]-l[37]+l[6]+l[23]+l[41]-l[39]-l[38]+l[40]-l[36]+l[8]-l[9]-l[5]-l[1]-l[13]-l[14]+l[19]+l[0]-l[34]-l[15]+l[17]+l[22]==-114
l[12]-l[28]-l[13]-l[23]-l[33]+l[18]+l[10]+l[11]+l[2]-l[36]+l[41]-l[16]+l[39]+l[34]+l[32]+l[37]-l[38]+l[20]+l[6]+l[7]+l[31]+l[5]+l[22]-l[4]-l[15]-l[24]+l[17]-l[3]+l[1]-l[35]-l[9]+l[30]+l[25]-l[0]-l[8]-l[14]+l[26]+l[21]==659
l[21]-l[3]+l[7]-l[27]+l[0]-l[32]-l[24]-l[37]+l[4]-l[22]+l[20]-l[5]-l[30]-l[31]-l[1]+l[15]+l[41]+l[12]+l[40]+l[38]-l[17]-l[39]+l[19]-l[13]+l[23]+l[18]-l[2]+l[6]-l[33]-l[9]+l[28]+l[8]-l[16]-l[10]-l[14]+l[34]+l[35]-l[11]==-430
l[11]-l[23]-l[9]-l[19]+l[17]+l[38]-l[36]-l[22]-l[10]+l[27]-l[14]-l[4]+l[5]+l[31]+l[2]+l[0]-l[16]-l[8]-l[28]+l[3]+l[40]+l[25]-l[33]+l[13]-l[32]-l[35]+l[26]-l[20]-l[41]-l[30]-l[12]-l[7]+l[37]-l[39]+l[15]+l[18]-l[29]-l[21]==-513
l[32]+l[19]+l[4]-l[13]-l[17]-l[30]+l[5]-l[33]-l[37]-l[15]-l[18]+l[7]+l[25]-l[14]+l[35]+l[40]+l[16]+l[1]+l[2]+l[26]-l[3]-l[39]-l[22]+l[23]-l[36]-l[27]-l[9]+l[6]-l[41]-l[0]-l[31]-l[20]+l[12]-l[8]+l[29]-l[11]-l[34]+l[21]==-502
l[30]-l[31]-l[36]+l[3]+l[9]-l[40]-l[33]+l[25]+l[39]-l[26]+l[23]-l[0]-l[29]-l[32]-l[4]+l[37]+l[28]+l[21]+l[17]+l[2]+l[24]+l[6]+l[5]+l[8]+l[16]+l[27]+l[19]+l[12]+l[20]+l[41]-l[22]+l[15]-l[11]+l[34]-l[18]-l[38]+l[1]-l[14]==853
l[38]-l[10]+l[16]+l[8]+l[21]-l[25]+l[36]-l[30]+l[31]-l[3]+l[5]-l[15]+l[23]-l[28]+l[7]+l[12]-l[29]+l[22]-l[0]-l[37]-l[14]-l[11]+l[32]+l[33]-l[9]+l[39]+l[41]-l[19]-l[1]+l[18]-l[4]-l[6]+l[13]+l[20]-l[2]-l[35]-l[26]+l[27]==-28
l[11]+l[18]-l[26]+l[15]-l[14]-l[33]+l[7]-l[23]-l[25]+l[0]-l[6]-l[21]-l[16]+l[17]-l[19]-l[28]-l[38]-l[37]+l[9]+l[20]-l[8]-l[3]+l[22]-l[35]-l[10]-l[31]-l[2]+l[41]-l[1]-l[4]+l[24]-l[34]+l[39]+l[40]+l[32]-l[5]+l[36]-l[27]==-529
l[38]+l[8]+l[36]+l[35]-l[23]-l[34]+l[13]-l[4]-l[27]-l[24]+l[26]+l[31]-l[30]-l[5]-l[40]+l[28]-l[11]-l[2]-l[39]+l[15]+l[10]-l[17]+l[3]+l[19]+l[22]+l[33]+l[0]+l[37]+l[16]-l[9]-l[32]+l[25]-l[21]-l[12]+l[6]-l[41]+l[20]-l[18]==-12
l[6]-l[30]-l[20]-l[27]-l[14]-l[39]+l[41]-l[33]-l[0]+l[25]-l[32]-l[3]+l[26]-l[12]+l[8]-l[35]-l[24]+l[15]+l[9]-l[4]+l[13]+l[36]+l[34]+l[1]-l[28]-l[21]+l[18]+l[23]+l[29]-l[10]-l[38]+l[22]+l[37]+l[5]+l[19]+l[7]+l[16]-l[31]==81

上z3，最后脚本如下，有点长

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
from z3 import *

l = [Int('l[%d]'%i) for i in range(42)]

s = Solver()

s.add(l[40]+l[35]+l[34]-l[0]-l[15]-l[37]+l[7]+l[6]-l[26]+l[20]+l[19]+l[8]-l[17]-l[14]-l[38]+l[1]-l[9]+l[22]+l[41]+l[3]-l[29]-l[36]-l[25]+l[5]+l[32]-l[16]+l[12]-l[24]+l[30]+l[39]+l[10]+l[2]+l[27]+l[28]+l[21]+l[33]-l[18]+l[4]==861)
s.add(l[31]+l[26]+l[11]-l[33]+l[27]-l[3]+l[12]+l[30]+l[1]+l[32]-l[16]+l[7]+l[10]-l[25]+l[38]-l[41]-l[14]-l[19]+l[29]+l[36]-l[9]-l[28]-l[6]-l[0]-l[22]-l[18]+l[20]-l[37]+l[4]-l[24]+l[34]-l[21]-l[39]-l[23]-l[8]-l[40]+l[15]-l[35]==-448)
s.add(l[26]+l[14]+l[15]+l[9]+l[13]+l[30]-l[11]+l[18]+l[23]+l[7]+l[3]+l[12]+l[25]-l[24]-l[39]-l[35]-l[20]+l[40]-l[8]+l[10]-l[5]-l[33]-l[31]+l[32]+l[19]+l[21]-l[6]+l[1]+l[16]+l[17]+l[29]+l[22]-l[4]-l[36]+l[41]+l[38]+l[2]+l[0]==1244)
s.add(l[5]+l[22]+l[15]+l[2]-l[28]-l[10]-l[3]-l[13]-l[18]+l[30]-l[9]+l[32]+l[19]+l[34]+l[23]-l[17]+l[16]-l[7]+l[24]-l[39]+l[8]-l[12]-l[40]-l[25]+l[37]-l[35]+l[11]-l[14]+l[20]-l[27]+l[4]-l[33]-l[21]+l[31]-l[6]+l[1]+l[38]-l[29]==-39)
s.add(l[41]-l[29]+l[23]-l[4]+l[20]-l[33]+l[35]+l[3]-l[19]-l[21]+l[11]+l[26]-l[24]-l[17]+l[37]+l[1]+l[16]-l[0]-l[13]+l[7]+l[10]+l[14]+l[22]+l[39]-l[40]+l[34]-l[38]+l[32]+l[25]-l[2]+l[15]+l[6]+l[28]-l[8]-l[5]-l[31]-l[30]-l[27]==485)
s.add(l[13]+l[19]+l[21]-l[2]-l[33]-l[0]+l[39]+l[31]-l[23]-l[41]+l[38]-l[29]+l[36]+l[24]-l[20]-l[9]-l[32]+l[37]-l[35]+l[40]+l[7]-l[26]+l[15]-l[10]-l[6]-l[16]-l[4]-l[5]-l[30]-l[14]-l[22]-l[25]-l[34]-l[17]-l[11]-l[27]+l[1]-l[28]==-1068)
s.add(l[32]+l[0]+l[9]+l[14]+l[11]+l[18]-l[13]+l[24]-l[2]-l[15]+l[19]-l[21]+l[1]+l[39]-l[8]-l[3]+l[33]+l[6]-l[5]-l[35]-l[28]+l[25]-l[41]+l[22]-l[17]+l[10]+l[40]+l[34]+l[27]-l[20]+l[23]+l[31]-l[16]+l[7]+l[12]-l[30]+l[29]-l[4]==939)
s.add(l[19]+l[11]+l[20]-l[16]+l[40]+l[25]+l[1]-l[31]+l[28]-l[23]+l[14]-l[9]-l[27]+l[35]+l[39]-l[37]-l[8]-l[22]+l[5]-l[6]+l[0]-l[32]+l[24]+l[33]+l[29]+l[38]+l[15]-l[2]+l[30]+l[7]+l[12]-l[3]-l[17]+l[34]+l[41]-l[4]-l[13]-l[26]==413)
s.add(l[22]+l[4]-l[9]+l[34]+l[35]+l[17]+l[3]-l[24]+l[38]-l[5]-l[41]-l[31]-l[0]-l[25]+l[33]+l[15]-l[1]-l[10]+l[16]-l[29]-l[12]+l[26]-l[39]-l[21]-l[18]-l[6]-l[40]-l[13]+l[8]+l[37]+l[19]+l[14]+l[32]+l[28]-l[11]+l[23]+l[36]+l[7]==117)
s.add(l[32]+l[16]+l[3]+l[11]+l[34]-l[31]+l[14]+l[25]+l[1]-l[30]-l[33]-l[40]-l[4]-l[29]+l[18]-l[27]+l[13]-l[19]-l[12]+l[23]-l[39]-l[41]-l[8]+l[22]-l[5]-l[38]-l[9]-l[37]+l[17]-l[36]+l[24]-l[21]+l[2]-l[26]+l[20]-l[7]+l[35]-l[0]==-313)
s.add(l[40]-l[1]+l[5]+l[7]+l[33]+l[29]+l[12]+l[38]-l[31]+l[2]+l[14]-l[35]-l[8]-l[24]-l[39]-l[9]-l[28]+l[23]-l[17]-l[22]-l[26]+l[32]-l[11]+l[4]-l[36]+l[10]+l[20]-l[18]-l[16]+l[6]-l[0]+l[3]-l[30]+l[37]-l[19]+l[21]+l[25]-l[15]==-42)
s.add(l[21]+l[26]-l[17]-l[25]+l[27]-l[22]-l[39]-l[23]-l[15]-l[20]-l[32]+l[12]+l[3]-l[6]+l[28]+l[31]+l[13]-l[16]-l[37]-l[30]-l[5]+l[41]+l[29]+l[36]+l[1]+l[11]+l[24]+l[18]-l[40]+l[19]-l[35]+l[2]-l[38]+l[14]-l[9]+l[4]+l[0]-l[33]==289)
s.add(l[29]+l[31]+l[32]-l[17]-l[7]+l[34]+l[2]+l[14]+l[23]-l[4]+l[3]+l[35]-l[33]-l[9]-l[20]-l[37]+l[24]-l[27]+l[36]+l[15]-l[18]-l[0]+l[12]+l[11]-l[38]+l[6]+l[22]+l[39]-l[25]-l[10]-l[19]-l[1]+l[13]-l[41]+l[30]-l[16]+l[28]-l[26]==-117)
s.add(l[5]+l[37]-l[39]+l[0]-l[27]+l[12]+l[41]-l[22]+l[8]-l[16]-l[38]+l[9]+l[15]-l[35]-l[29]+l[18]+l[6]-l[25]-l[28]+l[36]+l[34]+l[32]-l[14]-l[1]+l[20]+l[40]-l[19]-l[4]-l[7]+l[26]+l[30]-l[10]+l[13]-l[21]+l[2]-l[23]-l[3]-l[33]==-252)
s.add(l[29]+l[10]-l[41]-l[9]+l[12]-l[28]+l[11]+l[40]-l[27]-l[8]+l[32]-l[25]-l[23]+l[39]-l[1]-l[36]-l[15]+l[33]-l[20]+l[18]+l[22]-l[3]+l[6]-l[34]-l[21]+l[19]+l[26]+l[13]-l[4]+l[7]-l[37]+l[38]-l[2]-l[30]-l[0]-l[35]+l[5]+l[17]==-183)
s.add(l[6]-l[8]-l[20]+l[34]-l[33]-l[25]-l[4]+l[3]+l[17]-l[13]-l[15]-l[40]+l[1]-l[30]-l[14]-l[28]-l[35]+l[38]-l[22]+l[2]+l[24]-l[29]+l[5]+l[9]+l[37]+l[23]-l[18]+l[19]-l[21]+l[11]+l[36]+l[41]-l[7]-l[32]+l[10]+l[26]-l[0]+l[31]==188)
s.add(l[3]+l[6]-l[41]+l[10]+l[39]+l[37]+l[1]+l[8]+l[21]+l[24]+l[29]+l[12]+l[27]-l[38]+l[11]+l[23]+l[28]+l[33]-l[31]+l[14]-l[5]+l[32]-l[17]+l[40]-l[34]+l[20]-l[22]-l[16]+l[19]+l[2]-l[36]-l[7]+l[18]+l[15]+l[26]-l[0]-l[4]+l[35]==1036)
s.add(l[28]-l[33]+l[2]+l[37]-l[12]-l[9]-l[39]+l[16]-l[32]+l[8]-l[36]+l[31]+l[10]-l[4]+l[21]-l[25]+l[18]+l[24]-l[0]+l[29]-l[26]+l[35]-l[22]-l[41]-l[6]+l[15]+l[19]+l[40]+l[7]+l[34]+l[17]-l[3]-l[13]+l[5]+l[23]+l[11]-l[27]+l[1]==328)
s.add(l[22]-l[32]+l[17]-l[9]+l[20]-l[18]-l[34]+l[23]+l[36]-l[35]-l[38]+l[27]+l[4]-l[5]-l[41]+l[29]+l[33]+l[0]-l[37]+l[28]-l[40]-l[11]-l[12]+l[7]+l[1]+l[2]-l[26]-l[16]-l[8]+l[24]-l[25]+l[3]-l[6]-l[19]-l[39]-l[14]-l[31]+l[10]==-196)
s.add(l[11]+l[13]+l[14]-l[15]-l[29]-l[2]+l[7]+l[20]+l[30]-l[36]-l[33]-l[19]+l[31]+l[0]-l[39]-l[4]-l[6]+l[38]+l[35]-l[28]+l[34]-l[9]-l[23]-l[26]+l[37]-l[8]-l[27]+l[5]-l[41]+l[3]+l[17]+l[40]-l[10]+l[25]+l[12]-l[24]+l[18]+l[32]==7)
s.add(l[34]-l[37]-l[40]+l[4]-l[22]-l[31]-l[6]+l[38]+l[13]-l[28]+l[8]+l[30]-l[20]-l[7]-l[32]+l[26]+l[1]-l[18]+l[5]+l[35]-l[24]-l[41]+l[9]-l[0]-l[2]-l[15]-l[10]+l[12]-l[36]+l[33]-l[16]-l[14]-l[25]-l[29]-l[21]+l[27]+l[3]-l[17]==-945)
s.add(l[12]-l[30]-l[8]+l[20]-l[2]-l[36]-l[25]-l[0]-l[19]-l[28]-l[7]-l[11]-l[33]+l[4]-l[23]+l[10]-l[41]+l[39]-l[32]+l[27]+l[18]+l[15]+l[34]+l[13]-l[40]+l[29]-l[6]+l[37]-l[14]-l[16]+l[38]-l[26]+l[17]+l[31]-l[22]-l[35]+l[5]-l[1]==-480)
s.add(l[36]-l[11]-l[34]+l[8]+l[0]+l[15]+l[28]-l[39]-l[32]-l[2]-l[27]+l[22]+l[16]-l[30]-l[3]+l[31]-l[26]+l[20]+l[17]-l[29]-l[18]+l[19]-l[10]+l[6]-l[5]-l[38]-l[25]-l[24]+l[4]+l[23]+l[9]+l[14]+l[21]-l[37]+l[13]-l[41]-l[12]+l[35]==-213)
s.add(l[19]-l[36]-l[12]+l[33]-l[27]-l[37]-l[25]+l[38]+l[16]-l[18]+l[22]-l[39]+l[13]-l[7]-l[31]-l[26]+l[15]-l[10]-l[9]-l[2]-l[30]-l[11]+l[41]-l[4]+l[24]+l[34]+l[5]+l[17]+l[14]+l[6]+l[8]-l[21]-l[23]+l[32]-l[1]-l[29]-l[0]+l[3]==-386)
s.add(l[0]+l[7]-l[28]-l[38]+l[19]+l[31]-l[5]+l[24]-l[3]+l[33]-l[12]-l[29]+l[32]+l[1]-l[34]-l[9]-l[25]+l[26]-l[8]+l[4]-l[10]+l[40]-l[15]-l[11]-l[27]+l[36]+l[14]+l[41]-l[35]-l[13]-l[17]-l[21]-l[18]+l[39]-l[2]+l[20]-l[23]-l[22]==-349)
s.add(l[10]+l[22]+l[21]-l[0]+l[15]-l[6]+l[20]-l[29]-l[30]-l[33]+l[19]+l[23]-l[28]+l[41]-l[27]-l[12]-l[37]-l[32]+l[34]-l[36]+l[3]+l[1]-l[13]+l[18]+l[14]+l[9]+l[7]-l[39]+l[8]+l[2]-l[31]-l[5]-l[40]+l[38]-l[26]-l[4]+l[16]-l[25]==98)
s.add(l[28]+l[38]+l[20]+l[0]-l[5]-l[34]-l[41]+l[22]-l[26]+l[11]+l[29]+l[31]-l[3]-l[16]+l[23]+l[17]-l[18]+l[9]-l[4]-l[12]-l[19]-l[40]-l[27]+l[33]+l[8]-l[37]+l[2]+l[15]-l[24]-l[39]+l[10]+l[35]-l[1]+l[30]-l[36]-l[25]-l[14]-l[32]==-412)
s.add(l[1]-l[24]-l[29]+l[39]+l[41]+l[0]+l[9]-l[19]+l[6]-l[37]-l[22]+l[32]+l[21]+l[28]+l[36]+l[4]-l[17]+l[20]-l[13]-l[35]-l[5]+l[33]-l[27]-l[30]+l[40]+l[25]-l[18]+l[34]-l[3]-l[10]-l[16]-l[23]-l[38]+l[8]-l[14]-l[11]-l[7]+l[12]==-95)
s.add(l[2]-l[24]+l[31]+l[0]+l[9]-l[6]+l[7]-l[1]-l[22]+l[8]-l[23]+l[40]+l[20]-l[38]-l[11]-l[14]+l[18]-l[36]+l[15]-l[4]-l[41]-l[12]-l[34]+l[32]-l[35]+l[17]-l[21]-l[10]-l[29]+l[39]-l[16]+l[27]+l[26]-l[3]-l[5]+l[13]+l[25]-l[28]==-379)
s.add(l[19]-l[17]+l[31]+l[14]+l[6]-l[12]+l[16]-l[8]+l[27]-l[13]+l[41]+l[2]-l[7]+l[32]+l[1]+l[25]-l[9]+l[37]+l[34]-l[18]-l[40]-l[11]-l[10]+l[38]+l[21]+l[3]-l[0]+l[24]+l[15]+l[23]-l[20]+l[26]+l[22]-l[4]-l[28]-l[5]+l[39]+l[35]==861)
s.add(l[35]+l[36]-l[16]-l[26]-l[31]+l[0]+l[21]-l[13]+l[14]+l[39]+l[7]+l[4]+l[34]+l[38]+l[17]+l[22]+l[32]+l[5]+l[15]+l[8]-l[29]+l[40]+l[24]+l[6]+l[30]-l[2]+l[25]+l[23]+l[1]+l[12]+l[9]-l[10]-l[3]-l[19]+l[20]-l[37]-l[33]-l[18]==1169)
s.add(l[13]+l[0]-l[25]-l[32]-l[21]-l[34]-l[14]-l[9]-l[8]-l[15]-l[16]+l[38]-l[35]-l[30]-l[40]-l[12]+l[3]-l[19]+l[4]-l[41]+l[2]-l[36]+l[37]+l[17]-l[1]+l[26]-l[39]-l[10]-l[33]+l[5]-l[27]-l[23]-l[24]-l[7]+l[31]-l[28]-l[18]+l[6]==-1236)
s.add(l[20]+l[27]-l[29]-l[25]-l[3]+l[28]-l[32]-l[11]+l[10]+l[31]+l[16]+l[21]-l[7]+l[4]-l[24]-l[35]+l[26]+l[12]-l[37]+l[6]+l[23]+l[41]-l[39]-l[38]+l[40]-l[36]+l[8]-l[9]-l[5]-l[1]-l[13]-l[14]+l[19]+l[0]-l[34]-l[15]+l[17]+l[22]==-114)
s.add(l[12]-l[28]-l[13]-l[23]-l[33]+l[18]+l[10]+l[11]+l[2]-l[36]+l[41]-l[16]+l[39]+l[34]+l[32]+l[37]-l[38]+l[20]+l[6]+l[7]+l[31]+l[5]+l[22]-l[4]-l[15]-l[24]+l[17]-l[3]+l[1]-l[35]-l[9]+l[30]+l[25]-l[0]-l[8]-l[14]+l[26]+l[21]==659)
s.add(l[21]-l[3]+l[7]-l[27]+l[0]-l[32]-l[24]-l[37]+l[4]-l[22]+l[20]-l[5]-l[30]-l[31]-l[1]+l[15]+l[41]+l[12]+l[40]+l[38]-l[17]-l[39]+l[19]-l[13]+l[23]+l[18]-l[2]+l[6]-l[33]-l[9]+l[28]+l[8]-l[16]-l[10]-l[14]+l[34]+l[35]-l[11]==-430)
s.add(l[11]-l[23]-l[9]-l[19]+l[17]+l[38]-l[36]-l[22]-l[10]+l[27]-l[14]-l[4]+l[5]+l[31]+l[2]+l[0]-l[16]-l[8]-l[28]+l[3]+l[40]+l[25]-l[33]+l[13]-l[32]-l[35]+l[26]-l[20]-l[41]-l[30]-l[12]-l[7]+l[37]-l[39]+l[15]+l[18]-l[29]-l[21]==-513)
s.add(l[32]+l[19]+l[4]-l[13]-l[17]-l[30]+l[5]-l[33]-l[37]-l[15]-l[18]+l[7]+l[25]-l[14]+l[35]+l[40]+l[16]+l[1]+l[2]+l[26]-l[3]-l[39]-l[22]+l[23]-l[36]-l[27]-l[9]+l[6]-l[41]-l[0]-l[31]-l[20]+l[12]-l[8]+l[29]-l[11]-l[34]+l[21]==-502)
s.add(l[30]-l[31]-l[36]+l[3]+l[9]-l[40]-l[33]+l[25]+l[39]-l[26]+l[23]-l[0]-l[29]-l[32]-l[4]+l[37]+l[28]+l[21]+l[17]+l[2]+l[24]+l[6]+l[5]+l[8]+l[16]+l[27]+l[19]+l[12]+l[20]+l[41]-l[22]+l[15]-l[11]+l[34]-l[18]-l[38]+l[1]-l[14]==853)
s.add(l[38]-l[10]+l[16]+l[8]+l[21]-l[25]+l[36]-l[30]+l[31]-l[3]+l[5]-l[15]+l[23]-l[28]+l[7]+l[12]-l[29]+l[22]-l[0]-l[37]-l[14]-l[11]+l[32]+l[33]-l[9]+l[39]+l[41]-l[19]-l[1]+l[18]-l[4]-l[6]+l[13]+l[20]-l[2]-l[35]-l[26]+l[27]==-28)
s.add(l[11]+l[18]-l[26]+l[15]-l[14]-l[33]+l[7]-l[23]-l[25]+l[0]-l[6]-l[21]-l[16]+l[17]-l[19]-l[28]-l[38]-l[37]+l[9]+l[20]-l[8]-l[3]+l[22]-l[35]-l[10]-l[31]-l[2]+l[41]-l[1]-l[4]+l[24]-l[34]+l[39]+l[40]+l[32]-l[5]+l[36]-l[27]==-529)
s.add(l[38]+l[8]+l[36]+l[35]-l[23]-l[34]+l[13]-l[4]-l[27]-l[24]+l[26]+l[31]-l[30]-l[5]-l[40]+l[28]-l[11]-l[2]-l[39]+l[15]+l[10]-l[17]+l[3]+l[19]+l[22]+l[33]+l[0]+l[37]+l[16]-l[9]-l[32]+l[25]-l[21]-l[12]+l[6]-l[41]+l[20]-l[18]==-12)
s.add(l[6]-l[30]-l[20]-l[27]-l[14]-l[39]+l[41]-l[33]-l[0]+l[25]-l[32]-l[3]+l[26]-l[12]+l[8]-l[35]-l[24]+l[15]+l[9]-l[4]+l[13]+l[36]+l[34]+l[1]-l[28]-l[21]+l[18]+l[23]+l[29]-l[10]-l[38]+l[22]+l[37]+l[5]+l[19]+l[7]+l[16]-l[31]==81)
print(s.check())
m = s.model()
for i in range(42):
    print(chr((m[l[i]]).as_long()), end="")

最后的flag为flag{A_l0ng_10NG_eqU4Ti0n_1s_E4Sy_W1Th_z3}

GWCTF 2019 Re3

有个SMC，不过可以跟着调试一下就出来了，ida python 不会写呜呜呜，只能自己单步调试，找了个IDC脚本

1
2
3
4
5
6
7
8
9
#include <idc.idc>

static main(){
    auto addr = 0x402219;
    auto i = 0;
    for(i=0; i<=223; i++){
        PatchByte(addr+i, Byte(addr+i)^0x99);
    }
}

按shift+F12调出IDC界面跑一下就出了

patch之后进入函数，使用findcrypt找到了函数的算法大概是AES加密，密钥可以调出来

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
__int64 __fastcall sub_40221A(__int64 input)
{
  unsigned int v2; // [rsp+18h] [rbp-D8h]
  signed int i; // [rsp+1Ch] [rbp-D4h]
  char v4; // [rsp+20h] [rbp-D0h]
  unsigned __int64 v5; // [rsp+E8h] [rbp-8h]

  v5 = __readfsqword(0x28u);
  AESKeyGenerate((__int64)&v4, (__int64)&key);
  AESEncrypt((__int64)&v4, input);
  AESEncrypt((__int64)&v4, input + 16);
  v2 = 1;
  for ( i = 0; i <= 31; ++i )
  {
    if ( *(_BYTE *)(i + input) != data[i] )
      v2 = 0;
  }
  return v2;
}

key 是

1
2
3
4
5
6
7
8
9
10
11
key = [
      0xCB, 0x8D, 0x49, 0x35, 0x21, 0xB4, 0x7A, 0x4C, 0xC1, 0xAE, 
  0x7E, 0x62, 0x22, 0x92, 0x66, 0xCE
]

data = [
      0xBC, 0x0A, 0xAD, 0xC0, 0x14, 0x7C, 0x5E, 0xCC, 0xE0, 0xB1, 
  0x40, 0xBC, 0x9C, 0x51, 0xD5, 0x2B, 0x46, 0xB2, 0xB9, 0x43, 
  0x4D, 0xE5, 0x32, 0x4B, 0xAD, 0x7F, 0xB4, 0xB3, 0x9C, 0xDB, 
  0x4B, 0x5B
]

然后直接跑解密

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
import base64
from Crypto.Cipher import AES
import binascii


key = [
      0xCB, 0x8D, 0x49, 0x35, 0x21, 0xB4, 0x7A, 0x4C, 0xC1, 0xAE, 
  0x7E, 0x62, 0x22, 0x92, 0x66, 0xCE
]

data = [
      0xBC, 0x0A, 0xAD, 0xC0, 0x14, 0x7C, 0x5E, 0xCC, 0xE0, 0xB1, 
  0x40, 0xBC, 0x9C, 0x51, 0xD5, 0x2B, 0x46, 0xB2, 0xB9, 0x43, 
  0x4D, 0xE5, 0x32, 0x4B, 0xAD, 0x7F, 0xB4, 0xB3, 0x9C, 0xDB, 
  0x4B, 0x5B
]

cipher = AES.new(bytes(key))
a = cipher.decrypt(bytes(data[:16]))
a += cipher.decrypt(bytes(data[16:]))
print(a)

出了，比较简单

flag{924a9ab2163d390410d0a1f670}

[GUET-CTF] number_game

x64的ELF，main 函数还算简单

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
unsigned __int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
  _QWORD *v3; // ST08_8
  __int64 input; // [rsp+10h] [rbp-30h]
  __int16 v6; // [rsp+18h] [rbp-28h]
  __int64 v7; // [rsp+20h] [rbp-20h]
  __int16 v8; // [rsp+28h] [rbp-18h]
  char v9; // [rsp+2Ah] [rbp-16h]
  unsigned __int64 v10; // [rsp+38h] [rbp-8h]

  v10 = __readfsqword(0x28u);
  input = 0LL;
  v6 = 0;
  v7 = 0LL;
  v8 = 0;
  v9 = 0;
  __isoc99_scanf("%s", &input, a3);
  if ( (unsigned int)check1((const char *)&input) )
  {
    v3 = trans1((__int64)&input, 0, 10);
    trans2((__int64)v3, (__int64)&v7);
    v9 = 0;
    replace((char *)&v7);
    if ( (unsigned int)compare() )
    {
      puts("TQL!");
      printf("flag{", &v7);
      printf("%s", &input);
      puts("}");
    }
    else
    {
      puts("your are cxk!!");
    }
  }
  return __readfsqword(0x28u) ^ v10;
}

第一个check是看长度和格式，必须要48 <= ord(i) <= 52, 也就是0-4，长度是10，所以应该可以5 ** 10 直接爆，后面的if里面是个矩阵操作，比较横向和竖向不能相同，是个数独

1
2
3
4
5
6
7
14#23 0
30#1# 4 2
0#23# 1 4
#3##0 2 1 4
42##1 3 0


0421421430

trans1 是个递归，根据单双数来进行转存，是个二叉树，单数左边双数右边，结构为byte|odd Node|even Node，这个不关俺的事儿，只管看怎么填进去的，按照横着的顺序跑了一下，完全不是顺序，又不想逆算法，patch一下他的判定，把0-4改成0-9，然后调试一下看看

1
0x37, 0x33, 0x38, 0x31, 0x39, 0x34, 0x30, 0x35, 0x32, 0x36

输入为0123456789，结果是

1
2
3
4
5
14723
30318
01239
43050
42261

写个脚本，出了

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
m = [
    0x31, 0x34, 0x23, 0x32, 0x33, 0x33, 0x30, 0x23, 0x31, 0x23, 
  0x30, 0x23, 0x32, 0x33, 0x23, 0x23, 0x33, 0x23, 0x23, 0x30, 
  0x34, 0x32, 0x23, 0x23, 0x31
]

after = [
  0x31, 0x34, 0x37, 0x32, 0x33, 0x33, 0x30, 0x33, 0x31, 0x38, 
  0x30, 0x31, 0x32, 0x33, 0x39, 0x34, 0x33, 0x30, 0x35, 0x30, 
  0x34, 0x32, 0x32, 0x36, 0x31
]

matrix = m
transTable = [7, 3, 8, 1, 9, 4, 0, 5, 2, 6]
solve = [int(x) for x in list('0421421430')]
res = [0]*10

for i in range(len(matrix)):
  if (i+1) % 5 == 0:
    print(chr(matrix[i]))
  else:
    print(chr(matrix[i]), end='')

cnt = 0
for i in transTable:
  res[i] = solve[cnt]
  cnt += 1
print(''.join([str(x) for x in res]))

flag{1134240024}

actf oruga

迷宫题，就是走的时候是一条路走到死

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
. . . . # . . . . . . . # # # #
. . . # # . . . O O . . . . . .
. . . . . . . . O O . P P . . .
. . . L . O O . O O . P P . . .
. . . L . O O . O O . P . . . .
. . L L . O O . . . . P . . . .
. . . . . O O . . . . P . . . .
# . . . . . . . . . . . . . . .
. . . . . . . . . . . . # . . .
. . . . . . M M M . . . # . . .
. . . . . . . M M M . . . . E E
. . . 0 . M . M . M . . . . E .
. . . . . . . . . . . . . . E E
T T T I . M . M . M . . . . E .
. T . I . M . M . M . . . . E .
. T . I . M . M . M ! . . . E E

然后他的上下左右是特定的，很快就出了MEWEMEWJMEWJM

[网鼎杯2020] 青龙组 signal

是个中等难度的虚拟机，看了一下网上的WP，直接angr一把梭，太猛了

1
2
3
4
5
6
import angr
proj = angr.Project('./signal.exe',auto_load_libs = False)  #载入文件创建镜像
state = proj.factory.entry_state() # 根据镜像创建进程
simgr = proj.factory.simgr(state)  # 创建一个模拟器，用来模拟执行求解
simgr.explore(find = 0x40179E,avoid = 0x4016ed)  # 成功的地址和失败的地址
print (simgr.found[0].posix.dumps(0))  # 把要找的结果输出

757515121f3d478直接出了

[Zeropts2020] easy strcmp

看了一下main函数

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
__int64 __fastcall main(signed int a1, char **a2, char **a3)
{
  if ( a1 > 1 )
  {
    if ( !strcmp(a2[1], "zer0pts{********CENSORED********}") )
      puts("Correct!");
    else
      puts("Wrong!");
  }
  else
  {
    printf("Usage: %s <FLAG>\n", *a2, a3, a2);
  }
  return 0LL;
}

这个strcmp绝对有蹊跷，要么是被魔改过，要么是钩子函数

反正elf结构里面的函数也不多，直接翻到了类似于SMC的代码段

1
2
3
4
5
6
7
8
9
int (**sub_795())(const char *s1, const char *s2)
{
  int (**result)(const char *, const char *); // rax

  result = &strcmp;
  qword_201090 = (__int64 (__fastcall *)(_QWORD, _QWORD))&strcmp;
  off_201028 = sub_6EA;
  return result;
}

好耶，看看这个qword还有这个sub函数的调用过程就可以了

动态调试跟一下

1
2
3
4
5
6
7
8
9
10
11
12
13
__int64 __fastcall newStrCmp(__int64 input, __int64 cmpare)
{
  int len; // [rsp+18h] [rbp-8h]
  int strlen; // [rsp+18h] [rbp-8h]
  int j; // [rsp+1Ch] [rbp-4h]

  for ( i = 0; *(_BYTE *)(i + input); ++i )
    ;
  strlen = (len >> 3) + 1;
  for ( j = 0; j < strlen; ++j )
    *(_QWORD *)(8 * j + input) -= table[j];
  return OriginStrCmp(input, cmpare);
}

那不就得了么

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
censored = 'zer0pts{********CENSORED********}'

def getHexEight(s):
    chunk = 0
    for i in s:
        b = ord(i)
        chunk <<= 8
        chunk += b
    return chunk

def hexEightToStr(number:int):
    s = ''
    while number != 0:
        c = number & 0xff
        s += chr(c)
        number >>= 8
    s = list(s)
    #s.reverse()
    return ''.join(s)

table = [0, 0x410A4335494A0942, 0x0B0EF2F50BE619F0, 0x4F0A3A064A35282B]

for i in range(4):
    s = censored[i*8: (i+1)*8]
    s = s[::-1]
    s = getHexEight(s)
    #print(hex(s))
    s += table[i]
    s &= 0xffffffffffffffff
    s = hexEightToStr(s)
    print(s, end='')

值得注意的是主机中的大小端序，我们自己是大端序，但是他转化为hex来加减的时候用的是小端序

zer0pts{l3ts_m4k3_4_DETOUR_t0d4y}

[FlareOn3] Challenge1

x86的exe程序，看样子是个边表base64

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
_BYTE *__cdecl tran_func(int input, unsigned int length)
{
  unsigned int v3; // ST24_4
  int v4; // ST2C_4
  int v5; // [esp+Ch] [ebp-24h]
  int v6; // [esp+10h] [ebp-20h]
  int v7; // [esp+14h] [ebp-1Ch]
  int i; // [esp+1Ch] [ebp-14h]
  _BYTE *v9; // [esp+24h] [ebp-Ch]
  int v10; // [esp+28h] [ebp-8h]
  unsigned int v11; // [esp+2Ch] [ebp-4h]

  v9 = malloc(4 * ((length + 2) / 3) + 1);
  if ( !v9 )
    return 0;
  v11 = 0;
  v10 = 0;
  while ( v11 < length )
  {
    if ( v11 >= length )
      v7 = 0;
    else
      v7 = *(unsigned __int8 *)(v11++ + input);
    if ( v11 >= length )
      v6 = 0;
    else
      v6 = *(unsigned __int8 *)(v11++ + input);
    if ( v11 >= length )
      v5 = 0;
    else
      v5 = *(unsigned __int8 *)(v11++ + input);
    v3 = v5 + (v7 << 16) + (v6 << 8);
    v9[v10] = byte_413000[(v3 >> 18) & 0x3F];
    v4 = v10 + 1;
    v9[v4++] = byte_413000[(v3 >> 12) & 0x3F];
    v9[v4++] = byte_413000[(v3 >> 6) & 0x3F];
    v9[v4] = byte_413000[v5 & 0x3F];
    v10 = v4 + 1;
  }
  for ( i = 0; i < dword_413040[length % 3]; ++i )
    v9[4 * ((length + 2) / 3) - i - 1] = 61;
  v9[4 * ((length + 2) / 3)] = 0;
  return v9;
}

字母表是ZYXABCDEFGHIJKLMNOPQRSTUVWzyxabcdefghijklmnopqrstuvw0123456789+/

写个脚本就出来了

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
import base64
table = 'ZYXABCDEFGHIJKLMNOPQRSTUVWzyxabcdefghijklmnopqrstuvw0123456789+/'
cipher = 'x2dtJEOmyjacxDemx2eczT5cVS9fVUGvWTuZWjuexjRqy24rV29q'
ori_table = ['A', 'B', 'C', 'D', 'E', 'F', 'G', 'H',
'I', 'G', 'K', 'L', 'M', 'N', 'O', 'P',
'Q', 'R', 'S', 'T', 'U', 'V', 'W', 'X',
'Y', 'Z', 'a', 'b', 'c', 'd', 'e', 'f',
'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n',
'o', 'p', 'q', 'r', 's', 't', 'u', 'v',
'w', 'x', 'y', 'z', '0', '1', '2', '3',
'4', '5', '6', '7', '8', '9', '+', '/']
trans = ''
for i in cipher:
    idx = table.index(i)
    trans += ori_table[idx]
print(base64.b64decode(trans.encode()))

结果是sh00ting_phish_in_a_baq\xb2el@flare-on.com？？？ 特殊字符??艹了复制粘贴的表有问题，改一下就行sh00ting_phish_in_a_barrel@flare-on.com