2020第十三届全国大学生信息安全创新实践大赛 z3

http://ethereal.prohitime.top/demo/


其实根据题目名字的提示（直接百度这道题的题目，会发现z3是一种解方程的工具）

// local variable allocation has failed, the output may be wrong!
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int v4; // [rsp+20h] [rbp-60h]
  int v5; // [rsp+24h] [rbp-5Ch]
  int v6; // [rsp+28h] [rbp-58h]
  int v7; // [rsp+2Ch] [rbp-54h]
  int v8; // [rsp+30h] [rbp-50h]
  int v9; // [rsp+34h] [rbp-4Ch]
  int v10; // [rsp+38h] [rbp-48h]
  int v11; // [rsp+3Ch] [rbp-44h]
  int v12; // [rsp+40h] [rbp-40h]
  int v13; // [rsp+44h] [rbp-3Ch]
  int v14; // [rsp+48h] [rbp-38h]
  int v15; // [rsp+4Ch] [rbp-34h]
  int v16; // [rsp+50h] [rbp-30h]
  int v17; // [rsp+54h] [rbp-2Ch]
  int v18; // [rsp+58h] [rbp-28h]
  int v19; // [rsp+5Ch] [rbp-24h]
  int v20; // [rsp+60h] [rbp-20h]
  int v21; // [rsp+64h] [rbp-1Ch]
  int v22; // [rsp+68h] [rbp-18h]
  int v23; // [rsp+6Ch] [rbp-14h]
  int v24; // [rsp+70h] [rbp-10h]
  int v25; // [rsp+74h] [rbp-Ch]
  int v26; // [rsp+78h] [rbp-8h]
  int v27; // [rsp+7Ch] [rbp-4h]
  int v28; // [rsp+80h] [rbp+0h]
  int v29; // [rsp+84h] [rbp+4h]
  int v30; // [rsp+88h] [rbp+8h]
  int v31; // [rsp+8Ch] [rbp+Ch]
  int v32; // [rsp+90h] [rbp+10h]
  int v33; // [rsp+94h] [rbp+14h]
  int v34; // [rsp+98h] [rbp+18h]
  int v35; // [rsp+9Ch] [rbp+1Ch]
  int v36; // [rsp+A0h] [rbp+20h]
  int v37; // [rsp+A4h] [rbp+24h]
  int v38; // [rsp+A8h] [rbp+28h]
  int v39; // [rsp+ACh] [rbp+2Ch]
  int v40; // [rsp+B0h] [rbp+30h]
  int v41; // [rsp+B4h] [rbp+34h]
  int v42; // [rsp+B8h] [rbp+38h]
  int v43; // [rsp+BCh] [rbp+3Ch]
  int v44; // [rsp+C0h] [rbp+40h]
  int v45; // [rsp+C4h] [rbp+44h]
  unsigned __int8 v46; // [rsp+D0h] [rbp+50h]
  unsigned __int8 v47; // [rsp+D1h] [rbp+51h]
  unsigned __int8 v48; // [rsp+D2h] [rbp+52h]
  unsigned __int8 v49; // [rsp+D3h] [rbp+53h]
  unsigned __int8 v50; // [rsp+D4h] [rbp+54h]
  unsigned __int8 v51; // [rsp+D5h] [rbp+55h]
  unsigned __int8 v52; // [rsp+D6h] [rbp+56h]
  unsigned __int8 v53; // [rsp+D7h] [rbp+57h]
  unsigned __int8 v54; // [rsp+D8h] [rbp+58h]
  unsigned __int8 v55; // [rsp+D9h] [rbp+59h]
  unsigned __int8 v56; // [rsp+DAh] [rbp+5Ah]
  unsigned __int8 v57; // [rsp+DBh] [rbp+5Bh]
  unsigned __int8 v58; // [rsp+DCh] [rbp+5Ch]
  unsigned __int8 v59; // [rsp+DDh] [rbp+5Dh]
  unsigned __int8 v60; // [rsp+DEh] [rbp+5Eh]
  unsigned __int8 v61; // [rsp+DFh] [rbp+5Fh]
  unsigned __int8 v62; // [rsp+E0h] [rbp+60h]
  unsigned __int8 v63; // [rsp+E1h] [rbp+61h]
  unsigned __int8 v64; // [rsp+E2h] [rbp+62h]
  unsigned __int8 v65; // [rsp+E3h] [rbp+63h]
  unsigned __int8 v66; // [rsp+E4h] [rbp+64h]
  unsigned __int8 v67; // [rsp+E5h] [rbp+65h]
  unsigned __int8 v68; // [rsp+E6h] [rbp+66h]
  unsigned __int8 v69; // [rsp+E7h] [rbp+67h]
  unsigned __int8 v70; // [rsp+E8h] [rbp+68h]
  unsigned __int8 v71; // [rsp+E9h] [rbp+69h]
  unsigned __int8 v72; // [rsp+EAh] [rbp+6Ah]
  unsigned __int8 v73; // [rsp+EBh] [rbp+6Bh]
  unsigned __int8 v74; // [rsp+ECh] [rbp+6Ch]
  unsigned __int8 v75; // [rsp+EDh] [rbp+6Dh]
  unsigned __int8 v76; // [rsp+EEh] [rbp+6Eh]
  unsigned __int8 v77; // [rsp+EFh] [rbp+6Fh]
  unsigned __int8 v78; // [rsp+F0h] [rbp+70h]
  unsigned __int8 v79; // [rsp+F1h] [rbp+71h]
  unsigned __int8 v80; // [rsp+F2h] [rbp+72h]
  unsigned __int8 v81; // [rsp+F3h] [rbp+73h]
  unsigned __int8 v82; // [rsp+F4h] [rbp+74h]
  unsigned __int8 v83; // [rsp+F5h] [rbp+75h]
  unsigned __int8 v84; // [rsp+F6h] [rbp+76h]
  unsigned __int8 v85; // [rsp+F7h] [rbp+77h]
  unsigned __int8 v86; // [rsp+F8h] [rbp+78h]
  unsigned __int8 v87; // [rsp+F9h] [rbp+79h]
  int Dst[43]; // [rsp+110h] [rbp+90h]
  int i; // [rsp+1BCh] [rbp+13Ch]

  _main(*(_QWORD *)&argc, argv, envp);
  memcpy(Dst, &unk_404020, 0xA8ui64);
  printf("plz input your flag:");
  scanf("%42s", &v46);
  v4 = 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52;
  v5 = 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52;
  v6 = 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52;
  v7 = 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52;
  v8 = 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52;
  v9 = 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52;
  v10 = 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52;
  v11 = 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59;
  v12 = 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59;
  v13 = 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59;
  v14 = 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59;
  v15 = 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59;
  v16 = 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59;
  v17 = 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59;
  v18 = 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66;
  v19 = 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66;
  v20 = 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66;
  v21 = 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66;
  v22 = 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66;
  v23 = 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66;
  v24 = 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66;
  v25 = 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73;
  v26 = 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73;
  v27 = 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73;
  v28 = 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73;
  v29 = 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73;
  v30 = 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73;
  v31 = 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73;
  v32 = 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80;
  v33 = 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80;
  v34 = 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80;
  v35 = 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80;
  v36 = 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80;
  v37 = 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80;
  v38 = 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80;
  v39 = 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87;
  v40 = 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87;
  v41 = 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87;
  v42 = 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87;
  v43 = 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87;
  v44 = 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87;
  v45 = 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87;
  for ( i = 0; i <= 41; ++i )
  {
    if ( *(&v4 + i) != Dst[i] )
    {
      printf("error");
      exit(0);
    }
  }
  printf("win");
  return 0;
}

这道题对我来说有两个问题：
一个是当时我不知道z3是什么东西
第二个是我没看懂这段到底什么意思
现在分析一下，这42个方程的未知数是以v46开始的，而scanf("%42s", &v46)，自己输入的就是v46,所以相当于v46,v47，就是自己输入的字符串的每一位
然后用z3解这个方程，但是安装z3其实挺麻烦，我在windows上没装好，然后到了kali上装的
提供一个解方程的网址： https://www.buildenvi.com/gongju/formula/3lck4
正规方法：z3
这个其实很好用，但是不知道为什么我比赛的时候总是报错

root@kali:~/z3/build/python# python z3.py
[v85 = 52,
 v65 = 52,
 v63 = 57,
 v74 = 45,
 v47 = 108,
 v62 = 98,
 v81 = 97,
 v64 = 45,
 v48 = 97,
 v51 = 55,
 v58 = 51,
 v53 = 49,
 v49 = 103,
 v55 = 49,
 v57 = 52,
 v67 = 49,
 v54 = 55,
 v70 = 57,
 v69 = 45,
 v56 = 100,
 v86 = 56,
 v72 = 48,
 v60 = 54,
 v78 = 52,
 v68 = 56,
 v79 = 99,
 v75 = 54,
 v46 = 102,
 v77 = 49,
 v76 = 101,
 v50 = 123,
 v61 = 51,
 v71 = 57,
 v82 = 102,
 v83 = 101,
 v84 = 54,
 v87 = 125,
 v80 = 50,
 v73 = 101,
 v66 = 101,
 v59 = 45,
 v52 = 101]
# 转成字符
v84 = 54
v65 = 52
v63 = 57
v74 = 45
v47 = 108
v62 = 98
v81 = 97
v64 = 45
v48 = 97
v51 = 55
v58 = 51
v53 = 49
v49 = 103
v55 = 49
v57 = 52
v67 = 49
v54 = 55
v70 = 57
v69 = 45
v56 = 100
v86 = 56
v72 = 48
v60 = 54
v78 = 52
v68 = 56
v79 = 99
v75 = 54
v46 = 102
v77 = 49
v76 = 101
v50 = 123
v61 = 51
v71 = 57
v82 = 102
v83 = 101
v85 = 52
v87 = 125
v80 = 50
v73 = 101
v66 = 101
v59 = 45
v52 = 101
 
print(chr(v46)+
      chr(v47)+
      chr(v48)+
      chr(v49)+
      chr(v50)+
      chr(v51)+
      chr(v52)+
      chr(v53)+
      chr(v54)+
      chr(v55)+
      chr(v56)+
      chr(v57)+
      chr(v58)+
      chr(v59)+
      chr(v60)+
      chr(v61)+
      chr(v62)+
      chr(v63)+
      chr(v64)+
      chr(v65)+
      chr(v66)+
      chr(v67)+
      chr(v68)+
      chr(v69)+
      chr(v70)+
      chr(v71)+
      chr(v72)+
      chr(v73)+
      chr(v74)+
      chr(v75)+
      chr(v76)+
      chr(v77)+
      chr(v78)+
      chr(v79)+
      chr(v80)+
      chr(v81)+
      chr(v82)+
      chr(v83)+
      chr(v84)+
      chr(v85)+
      chr(v86)+
      chr(v87))

flag{7e171d43-63b9-4e18-990e-6e14c2afe648}
http://ethereal.prohitime.top/demo/