Learning z3!

I learn something about py z3 from this challenge today.

signed __int64 __fastcall main(int a1, char **a2, char **a3)
{
  signed __int64 result; // rax
  char *j; // rax
  char v5; // ST1F_1
  char v6; // ST1E_1
  char v7; // [rsp+1Dh] [rbp-1B3h]
  signed int i; // [rsp+20h] [rbp-1B0h]
  signed int k; // [rsp+24h] [rbp-1ACh]
  int v10; // [rsp+28h] [rbp-1A8h]
  int v11; // [rsp+2Ch] [rbp-1A4h]
  signed int l; // [rsp+30h] [rbp-1A0h]
  signed int m; // [rsp+34h] [rbp-19Ch]
  int v14; // [rsp+38h] [rbp-198h]
  int v15; // [rsp+3Ch] [rbp-194h]
  signed int n; // [rsp+40h] [rbp-190h]
  signed int ii; // [rsp+44h] [rbp-18Ch]
  int v18; // [rsp+48h] [rbp-188h]
  signed int jj; // [rsp+4Ch] [rbp-184h]
  char *s; // [rsp+58h] [rbp-178h]
  __int64 v21; // [rsp+70h] [rbp-160h]
  __int64 v22; // [rsp+78h] [rbp-158h]
  __int64 v23; // [rsp+80h] [rbp-150h]
  __int64 v24; // [rsp+88h] [rbp-148h]
  __int64 v25; // [rsp+90h] [rbp-140h]
  __int64 v26; // [rsp+98h] [rbp-138h]
  __int64 v27; // [rsp+A0h] [rbp-130h]
  __int64 v28; // [rsp+A8h] [rbp-128h]
  __int64 v29; // [rsp+B0h] [rbp-120h]
  __int64 v30; // [rsp+B8h] [rbp-118h]
  __int64 v31; // [rsp+C0h] [rbp-110h]
  __int64 v32; // [rsp+C8h] [rbp-108h]
  __int64 v33; // [rsp+D0h] [rbp-100h]
  __int64 v34; // [rsp+D8h] [rbp-F8h]
  __int64 v35; // [rsp+E0h] [rbp-F0h]
  __int64 v36; // [rsp+E8h] [rbp-E8h]
  __int64 s1; // [rsp+F0h] [rbp-E0h]
  __int64 v38; // [rsp+F8h] [rbp-D8h]
  __int64 v39; // [rsp+100h] [rbp-D0h]
  __int64 v40; // [rsp+108h] [rbp-C8h]
  __int64 v41; // [rsp+110h] [rbp-C0h]
  __int64 v42; // [rsp+118h] [rbp-B8h]
  __int64 v43; // [rsp+120h] [rbp-B0h]
  __int64 v44; // [rsp+128h] [rbp-A8h]
  int v45[32]; // [rsp+130h] [rbp-A0h]
  __int64 v46; // [rsp+1B0h] [rbp-20h]
  __int64 v47; // [rsp+1B8h] [rbp-18h]
  unsigned __int64 v48; // [rsp+1C8h] [rbp-8h]

  v48 = __readfsqword(0x28u);
  if ( a1 == 2 )
  {
    s = a2[1];
    if ( strlen(a2[1]) != 39 )
    {
      puts("incorrect");
      exit(0);
    }
    if ( memcmp(s, "TWCTF{", 6uLL) || s[38] != 125 )
    {
      puts("incorrect");
      exit(0);
    }
    s1 = 0LL;
    v38 = 0LL;
    v39 = 0LL;
    v40 = 0LL;
    v41 = 0LL;
    v42 = 0LL;
    v43 = 0LL;
    v44 = 0LL;
    v46 = '76543210';
    v47 = 'fedcba98';
    for ( i = 0; i <= 15; ++i )
    {
      for ( j = strchr(s, *((char *)&v46 + i)); j; j = strchr(j + 1, *((char *)&v46 + i)) )
        ++*((_DWORD *)&s1 + i);
    }
    if ( memcmp(&s1, &dword_400F00, 0x40uLL) )
    {
      puts("incorrect");
      exit(0);
    }
    v21 = 0LL;
    v22 = 0LL;
    v23 = 0LL;
    v24 = 0LL;
    v25 = 0LL;
    v26 = 0LL;
    v27 = 0LL;
    v28 = 0LL;
    for ( k = 0; k <= 7; ++k )
    {
      v10 = 0;
      v11 = 0;
      for ( l = 0; l <= 3; ++l )
      {
        v5 = s[4 * k + 6 + l];
        v10 += v5;
        v11 ^= v5;
      }
      *((_DWORD *)&v21 + k) = v10;
      *((_DWORD *)&v25 + k) = v11;
    }
    v29 = 0LL;
    v30 = 0LL;
    v31 = 0LL;
    v32 = 0LL;
    v33 = 0LL;
    v34 = 0LL;
    v35 = 0LL;
    v36 = 0LL;
    for ( m = 0; m <= 7; ++m )
    {
      v14 = 0;
      v15 = 0;
      for ( n = 0; n <= 3; ++n )
      {
        v6 = s[8 * n + 6 + m];
        v14 += v6;
        v15 ^= v6;
      }
      *((_DWORD *)&v29 + m) = v14;
      *((_DWORD *)&v33 + m) = v15;
    }
    if ( memcmp(&v21, &dword_400F40, 0x20uLL) || memcmp(&v25, &dword_400F60, 0x20uLL) )
    {
      puts("incorrect");
      exit(0);
    }
    if ( memcmp(&v29, &dword_400FA0, 0x20uLL) || memcmp(&v33, &dword_400F80, 0x20uLL) )
    {
      puts("incorrect");
      exit(0);
    }
    memset(v45, 0, sizeof(v45));
    for ( ii = 0; ii <= 31; ++ii )
    {
      v7 = s[ii + 6];
      if ( v7 <= 47 || v7 > 57 )
      {
        if ( v7 <= 96 || v7 > 102 )
          v45[ii] = 0;
        else
          v45[ii] = 128;
      }
      else
      {
        v45[ii] = 255;
      }
    }
    if ( memcmp(v45, &dword_400FC0, 0x80uLL) )
    {
      puts("incorrect");
      exit(0);
    }
    v18 = 0;
    for ( jj = 0; jj <= 15; ++jj )
      v18 += s[2 * (jj + 3)];
    if ( v18 != 0x488 )
    {
      puts("incorrect");
      exit(0);
    }
    if ( s[37] != 53 || s[7] != 102 || s[11] != 56 || s[12] != 55 || s[23] != 50 || s[31] != 52 )
    {
      puts("incorrect");
      exit(0);
    }
    printf("Correct: %s\n", s, a2);
    result = 0LL;
  }
  else
  {
    fwrite("./bin flag_is_here", 1uLL, 0x12uLL, stderr);
    result = 1LL;
  }
  return result;
}

This exp can’t get right flag.

from z3 import *

#sol:
def sum_exp(li):
    result = 0
    for i in li[::2]:
        result += i
    return result


def count_cipin(li):
    result = [0 for _ in range(0,16)]
    F = '0123456789abcdef'
    for l in F:
        for m in li:
            if m == ord(l):
                result[int(l)] +=1
    return result


def count_add21(li):
    result = []
    F = 0
    for m in range(0,8):
        for n in range(0,4):
            F += li[4*m+n]
        result.append(F)
    return result

def count_xor25(li):
    result = []
    F = 0
    for m in range(0,8):
        for n in range(0,4):
            F ^= li[4*m+n]
        result.append(F)
    return result


def count_add29(li):
    result = []
    F = 0
    for m in range(0,8):
        for n in range(0,4):
            F += li[8*n+m]
        result.append(F)
    return result

def count_xor33(li):
    result = []
    F = 0
    for m in range(0,8):
        for n in range(0,4):
            F ^= li[8*n+m]
        result.append(F)
    return result





#          0 1 2 3 4 5 6 7 8 9 a b c d e f 
# cipin = [3,2,2,0,3,2,1,3,3,1,1,3,1,2,2,3] sum_it = 2246
# 


v21 = [0x15E,0x0DA,0x12F,0x131,0x100,0x131,0x0FB,0x102]                
v25 = [0x52,0x0C,0x1,0x0F,0x5C,0x5,0x53,0x58]
v29 = [0x129,0x103,0x12B,0x131,0x135,0x10B,0x0FF,0x0FF]
v33 = [0x1,0x57,0x7,0x0D,0x0D,0x53,0x51,0x51]
v45 = [0x80,0x80,0x0FF,0x80,0x0FF,0x0FF,0x0FF,0x0FF,0x80,0x0FF,0x0FF,0x80,0x80,0x0FF,0x0FF,0x80,0x0FF,0x0FF,0x80,0x0FF,0x80,0x80,0x0FF,0x0FF,0x0FF,0x0FF,0x80,0x0FF,0x0FF,0x0FF,0x80,0x0FF]



test_li = [49 for _ in range(0,32)]
print(sum_exp(test_li)
,count_cipin(test_li)
,count_add21(test_li)
,count_xor25(test_li)
,count_add29(test_li)
,count_xor33(test_li)
)

k = [BitVec('k'+str(i),8) for i in range(0,32)]
sol = Solver()
#sol.add(count_cipin(k) == cipin)

fake_flag1 = [100,102,50,98,52,56,55,55,97,55,50,101,101,57,48,99,48,50,102,56,100,102,55,48,52,52,97,50,56,52,97,53]
#sol.add(k!=fake_flag1)




#sol.add(count_add21(k) == v21)
sol.add(
k[0]+k[1]+k[2]+k[3] == v21[0], 
k[4]+k[5]+k[6]+k[7] == v21[1],
k[8]+k[9]+k[10]+k[11] == v21[2],
k[12]+k[13]+k[14]+k[15] == v21[3],
k[16]+k[17]+k[18]+k[19] == v21[4],
k[20]+k[21]+k[22]+k[23] == v21[5],
k[24]+k[25]+k[26]+k[27] == v21[6],
k[28]+k[29]+k[30]+k[31] == v21[7]
)
#sol.add(count_xor25(k) == v25)
sol.add(
k[0]^k[1]^k[2]^k[3] == v25[0],
k[4]^k[5]^k[6]^k[7] == v25[1],
k[8]^k[9]^k[10]^k[11] == v25[2],
k[12]^k[13]^k[14]^k[15] == v25[3],
k[16]^k[17]^k[18]^k[19] == v25[4],
k[20]^k[21]^k[22]^k[23] == v25[5],
k[24]^k[25]^k[26]^k[27] == v25[6],
k[28]^k[29]^k[30]^k[31] == v25[7]
)

#sol.add(count_add29(k) == v29)
sol.add(
k[0]+k[8]+k[16]+k[24] == v29[0],
k[1]+k[9]+k[17]+k[25] == v29[1],
k[2]+k[10]+k[18]+k[26] == v29[2],
k[3]+k[11]+k[19]+k[27] == v29[3],
k[4]+k[12]+k[20]+k[28] == v29[4],
k[5]+k[13]+k[21]+k[29] == v29[5],
k[6]+k[14]+k[22]+k[30] == v29[6],
k[7]+k[15]+k[23]+k[31] == v29[7]
)

#sol.add(count_xor33(k) == v33)
sol.add(
k[0]^k[8]^k[16]^k[24] == v33[0],
k[1]^k[9]^k[17]^k[25] == v33[1],
k[2]^k[10]^k[18]^k[26] == v33[2],
k[3]^k[11]^k[19]^k[27] == v33[3],
k[4]^k[12]^k[20]^k[28] == v33[4],
k[5]^k[13]^k[21]^k[29] == v33[5],   
k[6]^k[14]^k[22]^k[30] == v33[6],
k[7]^k[15]^k[23]^k[31] == v33[7]
)

point = 0
for i in v45:
    if(i == 0xff):
        sol.add(k[point]>=48,k[point]<=57)
    elif(i== 0x80):
        sol.add(k[point]>96,k[point]<=102)
    point += 1


sol.add(
sum(k)==2246,  
k[0]+k[2]+k[4]+k[6]+k[8]+k[10]+k[12]+k[14]+k[16]+k[18]+k[20]+k[22]+k[24]+k[26]+k[28]+k[30] == 0x488,
k[31] == 53 , 
k[1] == 102 , 
k[5] == 56 , 
k[6] == 55,
k[17] == 50, 
k[25] == 52
)

print(sol.check())
m = sol.model()
dic = {}
flag = 'TWCTF{'
for d in m.decls():
    dic[d.name()] = m[d].as_long()

for i in range(32):
    point = 'k'+str(i)
    flag += chr(dic.get(point))

flag += '}'
print(flag)
#print(dic)
#print(sol.model())
#print(sol.model())



Nice Z3!🐕