Writeup: TokyoWesterns 2019 - Easy Crack Me

(Updated: )
writeups
, , , ,

Information

  • category : reverse
  • points : 88

Description

Cracking is easy for you.

File : easy_crack_me

Writeup

To analyze the binary I used both ghidra and cutter (radare2’s GUI).

In the binary there is only one interesting function and it’s the main. The graph overview of the main is the following :

Just seeing the graph I could tell that this crackme wasn’t easy as the title said.

The decompiler of the main function generated by ghidra is the following :

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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
undefined8 main(int param_1,long param_2)

{
  char cVar1;
  char *__s;
  int iVar2;
  undefined8 uVar3;
  size_t sVar4;
  char *pcVar5;
  long lVar6;
  undefined8 *puVar7;
  long in_FS_OFFSET;
  byte bVar8;
  int local_1b8;
  int local_1b4;
  int local_1b0;
  uint local_1ac;
  int local_1a8;
  int local_1a4;
  int local_1a0;
  uint local_19c;
  int local_198;
  int local_194;
  int local_190;
  int local_18c;
  char *local_188;
  undefined8 local_168;
  undefined8 local_160;
  undefined8 local_158;
  undefined8 local_150;
  undefined8 local_148;
  undefined8 local_140;
  undefined8 local_138;
  undefined8 local_130;
  undefined8 local_128;
  undefined8 local_120;
  undefined8 local_118;
  undefined8 local_110;
  undefined8 local_108;
  undefined8 local_100;
  undefined8 local_f8;
  undefined8 local_f0;
  undefined8 local_e8;
  undefined8 local_e0;
  undefined8 local_d8;
  undefined8 local_d0;
  undefined8 local_c8;
  undefined8 local_c0;
  undefined8 local_b8;
  undefined8 local_b0;
  undefined8 local_a8 [16];
  undefined8 local_28;
  undefined8 local_20;
  long local_10;
  
  bVar8 = 0;
  local_10 = *(long *)(in_FS_OFFSET + 0x28);
  if (param_1 == 2) {
    __s = *(char **)(param_2 + 8);
    sVar4 = strlen(__s);
    if (sVar4 != 0x27) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    iVar2 = memcmp(__s,"TWCTF{",6);
    if ((iVar2 != 0) || (__s[0x26] != '}')) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    local_e8 = 0;
    local_e0 = 0;
    local_d8 = 0;
    local_d0 = 0;
    local_c8 = 0;
    local_c0 = 0;
    local_b8 = 0;
    local_b0 = 0;
    local_28 = 0x3736353433323130;
    local_20 = 0x6665646362613938;
    local_1b8 = 0;
    while (local_188 = __s, local_1b8 < 0x10) {
      while (pcVar5 = strchr(local_188,(int)*(char *)((long)&local_28 + (long)local_1b8)),
            pcVar5 != (char *)0x0) {
        *(int *)((long)&local_e8 + (long)local_1b8 * 4) =
             *(int *)((long)&local_e8 + (long)local_1b8 * 4) + 1;
        local_188 = pcVar5 + 1;
      }
      local_1b8 = local_1b8 + 1;
    }
    iVar2 = memcmp(&local_e8,&DAT_00400f00,0x40);
    if (iVar2 != 0) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    local_168 = 0;
    local_160 = 0;
    local_158 = 0;
    local_150 = 0;
    local_148 = 0;
    local_140 = 0;
    local_138 = 0;
    local_130 = 0;
    local_1b4 = 0;
    while (local_1b4 < 8) {
      local_1b0 = 0;
      local_1ac = 0;
      local_1a8 = 0;
      while (local_1a8 < 4) {
        local_1b0 = local_1b0 + (int)__s[(long)local_1a8 + (long)(local_1b4 << 2) + 6];
        local_1ac = local_1ac ^ (int)__s[(long)local_1a8 + (long)(local_1b4 << 2) + 6];
        local_1a8 = local_1a8 + 1;
      }
      *(int *)((long)&local_168 + (long)local_1b4 * 4) = local_1b0;
      *(uint *)((long)&local_148 + (long)local_1b4 * 4) = local_1ac;
      local_1b4 = local_1b4 + 1;
    }
    local_128 = 0;
    local_120 = 0;
    local_118 = 0;
    local_110 = 0;
    local_108 = 0;
    local_100 = 0;
    local_f8 = 0;
    local_f0 = 0;
    local_1a4 = 0;
    while (local_1a4 < 8) {
      local_1a0 = 0;
      local_19c = 0;
      local_198 = 0;
      while (local_198 < 4) {
        local_1a0 = local_1a0 + (int)__s[(long)(local_198 << 3) + (long)local_1a4 + 6];
        local_19c = local_19c ^ (int)__s[(long)(local_198 << 3) + (long)local_1a4 + 6];
        local_198 = local_198 + 1;
      }
      *(int *)((long)&local_128 + (long)local_1a4 * 4) = local_1a0;
      *(uint *)((long)&local_108 + (long)local_1a4 * 4) = local_19c;
      local_1a4 = local_1a4 + 1;
    }
    iVar2 = memcmp(&local_168,&DAT_00400f40,0x20);
    if ((iVar2 != 0) || (iVar2 = memcmp(&local_148,&DAT_00400f60,0x20), iVar2 != 0)) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    iVar2 = memcmp(&local_128,&DAT_00400fa0,0x20);
    if ((iVar2 != 0) || (iVar2 = memcmp(&local_108,&DAT_00400f80,0x20), iVar2 != 0)) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    lVar6 = 0x10;
    puVar7 = local_a8;
    while (lVar6 != 0) {
      lVar6 = lVar6 + -1;
      *puVar7 = 0;
      puVar7 = puVar7 + (ulong)bVar8 * 0x1ffffffffffffffe + 1;
    }
    local_194 = 0;
    while (local_194 < 0x20) {
      cVar1 = __s[(long)local_194 + 6];
      if ((cVar1 < '0') || ('9' < cVar1)) {
        if ((cVar1 < 'a') || ('f' < cVar1)) {
          *(undefined4 *)((long)local_a8 + (long)local_194 * 4) = 0;
        }
        else {
          *(undefined4 *)((long)local_a8 + (long)local_194 * 4) = 0x80;
        }
      }
      else {
        *(undefined4 *)((long)local_a8 + (long)local_194 * 4) = 0xff;
      }
      local_194 = local_194 + 1;
    }
    iVar2 = memcmp(local_a8,&DAT_00400fc0,0x80);
    if (iVar2 != 0) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    local_190 = 0;
    local_18c = 0;
    while (local_18c < 0x10) {
      local_190 = local_190 + (int)__s[(long)((local_18c + 3) * 2)];
      local_18c = local_18c + 1;
    }
    if (local_190 != 0x488) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    if ((((__s[0x25] != '5') || (__s[7] != 'f')) || (__s[0xb] != '8')) ||
       (((__s[0xc] != '7' || (__s[0x17] != '2')) || (__s[0x1f] != '4')))) {
      puts("incorrect");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    printf("Correct: %s\n",__s);
    uVar3 = 0;
  }
  else {
    fwrite("./bin flag_is_here",1,0x12,stderr);
    uVar3 = 1;
  }
  if (local_10 == *(long *)(in_FS_OFFSET + 0x28)) {
    return uVar3;
  }
                    /* WARNING: Subroutine does not return */
  __stack_chk_fail();
}

1st constraint

Our goal is to create a flag that passed to the program prints “correct”.
From now on I will rename various variable to make easier the understanding.

Let’s check what are the initial conditions to bypass.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
if (argc == 2) {
flag = *(char **)(param_2 + 8);
len_flag = strlen(flag);
                /* 0x27 = 39d */
if (len_flag != 0x27) {
    puts("incorrect");
                /* WARNING: Subroutine does not return */
    exit(0);
}
str_equal = memcmp(flag,"TWCTF{",6);
if ((str_equal != 0) || (flag[0x26] != '}')) {
    puts("incorrect");
                /* WARNING: Subroutine does not return */
    exit(0);
}

We need to :

  1. pass to the program one argument –> flag
  2. the length of the flag must be 0x27 = 39
  3. The first 6 byte of the flag are "TWCTF{"
  4. The last byte of the flag must be "}"

2nd constraint

From now on all operations will have a + 6 to remove the first 6 bytes "TWCTF{" or the first 6 bytes are not considered, so I’ll set the flag to be 39 - 6 ("TWCTF{") - 1 ("}") = 32 bytes (Only the characters that we need to find).

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
array_e8 = 0;
local_e0 = 0;
local_d8 = 0;
local_d0 = 0;
local_c8 = 0;
local_c0 = 0;
local_b8 = 0;
                /* string = string0 + string1 */
local_b0 = 0;
                /* -->"76543210" */
string0 = 0x3736353433323130;
                /* -->"fedcba98" */
string1 = 0x6665646362613938;
                /* 0x10 = 16d */
counter = 0;
while (pointer_to_flag = flag, counter < 0x10)        
{
    /*  strchr(const char *s, int c);
        Return pointer to the first occurence of the character c in the string s */
    while (first_occurence = strchr(pointer_to_flag,(int)*(char *)((long)&string0 + (long)counter)),first_occurence != (char *)0x0
                /* local_e8 += 1 */) {
    *(int *)((long)&array_e8 + (long)counter * 4) =
            *(int *)((long)&array_e8 + (long)counter * 4) + 1;
    pointer_to_flag = first_occurence + 1;
    }
    counter = counter + 1;
}
iVar2 = memcmp(&array_e8,&DAT_00400f00,0x40);
if (iVar2 != 0) {
    puts("incorrect");
                /* WARNING: Subroutine does not return */
    exit(0);
}

What this nested while does in pseucode:

1
2
3
4
5
6
7
8
9
10
11
array_freq = [16]; // array_e8 above
characters = "0123456789abcdef"; // string0 + string1 above
for(i = 0; i < len(flag); ++i)
{
    array_freq[i] = flag.count(characters[i]);
}
freq = 0x400f00; // we'll check this in just a second
if (array_freq != *freq)
{
    error;
}

So basically it constructs an array of frequencies of each character presented in string0 + string1.

Let’s see what’s inside 0x400f00. I used cutter in this case because with ghidra I had problem converting these values in little endian automatically.

1
[0x00000003, 0x00000002, 0x00000002, 0x00000000, 0x00000003, 0x00000002, 0x00000001, 0x00000003, 0x00000003, 0x00000001, 0x00000001, 0x00000003, 0x00000001, 0x00000002, 0x00000002, 0x00000003]

So basically there are three 0, two 1,…, two e and three f. There are other constraints to check to make sure that the flag is correct. To solve each of this constraints I used z3.

Sets the frequencies count in z3py was at first a pain. Luckily I found this code and I was able to make an “efficient and readable” code to impose the characters frequencies.

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
#!/usr/bin/env python3
from z3 import *


s = solver()
charset = '0123456789abcdef'
freq = [0x00000003, 0x00000002, 0x00000002, 0x00000000, 0x00000003, 0x00000002, 0x00000001, 0x00000003,
        0x00000003, 0x00000001, 0x00000001, 0x00000003, 0x00000001, 0x00000002, 0x00000002, 0x00000003]
flag = [BitVec('{:2}'.format(i), 8) for i in range(32)]

# As @usr suggested
for i, char in enumerate(charset):
	counter = 0
	for x in flag:
		counter += If(x == ord(char), 1, 0)
	s.add(counter == freq[i])


"""
As @Zhongjun 'Mark' Jin implemented the counter.
At first I used this because I didn't understand how to code the above method.

counterTrace = [IntVector('counterTrace' + str(i), 33) for i in range (0, 16)]
# ascii of 0 --> 9 = 48 --> 57.
# ascii of a --> f = 97 --> 102.
for j in range(0, 16):
    s.add(counterTrace[j][0] == 0)
    for i in range(0, 32):
        if j <= 9:
            s.add(If(numbers[i] == j + 48, counterTrace[j][i + 1] == counterTrace[j][i] + 1, counterTrace[j][i + 1] == counterTrace[j][i]))
        else:
            s.add(If(numbers[i] == j + 87, counterTrace[j][i + 1] == counterTrace[j][i] + 1, counterTrace[j][i + 1] == counterTrace[j][i]))
    s.add(counterTrace[j][32] == freq[j])
"""

Ok so far everything is ok..

3rd and 4th constraint

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
arrx = 0;
local_160 = 0;
local_158 = 0;
local_150 = 0;
arry = 0;
local_140 = 0;
local_138 = 0;
local_130 = 0;
i = 0;
while (i < 8) {
    x = 0;
    y = 0;
    j = 0;
    while (j < 4) {
    x = x + (int)flag[(long)j + (long)(i << 2) + 6];
    y = y ^ (int)flag[(long)j + (long)(i << 2) + 6];
    j = j + 1;
    }
    *(int *)((long)&arrx + (long)i * 4) = x;
    *(uint *)((long)&arry + (long)i * 4) = y;
    i = i + 1;
}
arrx1 = 0;
local_120 = 0;
local_118 = 0;
local_110 = 0;
arry1 = 0;
local_100 = 0;
local_f8 = 0;
local_f0 = 0;
i1 = 0;
while (i1 < 8) {
    x1 = 0;
    y1 = 0;
    j1 = 0;
    while (j1 < 4) {
    x1 = x1 + (int)flag[(long)(j1 << 3) + (long)i1 + 6];
    y1 = y1 ^ (int)flag[(long)(j1 << 3) + (long)i1 + 6];
    j1 = j1 + 1;
    }
    *(int *)((long)&arrx1 + (long)i1 * 4) = x1;
    *(uint *)((long)&arry1 + (long)i1 * 4) = y1;
    i1 = i1 + 1;
}
iVar2 = memcmp(&arrx,&INT_00400f40,0x20);
if ((iVar2 != 0) || (iVar2 = memcmp(&arry,&DAT_00400f60,0x20), iVar2 != 0)) {
    puts("incorrect");
                /* WARNING: Subroutine does not return */
    exit(0);
}
iVar2 = memcmp(&arrx1,&DAT_00400fa0,0x20);
if ((iVar2 != 0) || (iVar2 = memcmp(&arry1,&DAT_00400f80,0x20), iVar2 != 0)) {
    puts("incorrect");
                /* WARNING: Subroutine does not return */
    exit(0);
}

Let’s rewrite the first nested while in pseudocode:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
i = 0;
while(i < 8)
{ 
    x = 0;
    y = 0;
    for all c in flag[i:i*4]
    {
        x = x + int(c);     // In this pseudocode int(x) returns the ascii value
        y = y ^ int(c);     // of x in decimal. int('0') = 48, int('f') = 102
                            // In python is ord()
    }
    sum[i] = x;
    xor[i] = y;
}

if(sum != *0x00400f40 || xor != *0x00400f60)
{
    error;
}

Basically it divides the flag in blocks of 4, and then it converts every characters of the block to int and sum/xor them. Then it checks if the sum and xor are equal to the values stored in 0x00400f40 and 0x00400f60.

Content of 0x00400f40 and 0x00400f60 :

1
2
[0x0000015e, 0x000000da, 0x0000012f, 0x00000131, 0x00000100, 0x00000131, 0x000000fb, 0x00000102]
[0x00000052, 0x0000000c, 0x00000001, 0x0000000f, 0x0000005c, 0x00000005, 0x00000053, 0x00000058]

Second nested while in pseudocode:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
i = 0;
while(i < 8)
{
    x = 0;
    y = 0;
    for (j = 0; j < 4; ++j) // implicit + 6
    {
        x = x + int(flag[j * 8 + i]);
        y = y ^ int(flag[j * 8 + i]);
    }
    sum[i] = x;
    xor[i] = y;
}
if (sum != *0x00400fa0 || xor != *0x00400f80)
{
    error;
}

So it sums:

1
2
3
4
5
6
sum[0] = int(flag[0]) + int(flag[8]) + int(flag[16]) + int(flag[24])
sum[1] = int(flag[1]) + int(flag[9]) + int(flag[17]) + int(flag[25])
.
.
.
sum[7] = int(flag[7]) + int(flag[15]) + int(flag[23]) + int(flag[31])

The same for the xor.

Content of 0x00400fa0 and 0x00400f80 :

1
2
[0x00000129, 0x00000103, 0x0000012b, 0x00000131, 0x00000135, 0x0000010b, 0x000000ff, 0x000000ff]
[0x00000001, 0x00000057, 0x00000007, 0x0000000d, 0x0000000d, 0x00000053, 0x00000051, 0x00000051]

z3 code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
sum_1 = [0x0000015e, 0x000000da, 0x0000012f, 0x00000131, 0x00000100, 0x00000131, 0x000000fb, 0x00000102]
xor_1 = [0x00000052, 0x0000000c, 0x00000001, 0x0000000f, 0x0000005c, 0x00000005, 0x00000053, 0x00000058]
sum_2 = [0x00000129, 0x00000103, 0x0000012b, 0x00000131, 0x00000135, 0x0000010b, 0x000000ff, 0x000000ff]
xor_2 = [0x00000001, 0x00000057, 0x00000007, 0x0000000d, 0x0000000d, 0x00000053, 0x00000051, 0x00000051]

# First nested while
for i in range(0, 8):
	s.add(flag[0 + i * 4] + flag[1 + i * 4] + flag[2 + i * 4] + flag[3 + i * 4] == sum_1[i])
	s.add(flag[0 + i * 4] ^ flag[1 + i * 4] ^ flag[2 + i * 4] ^ flag[3 + i * 4] == xor_1[i])

# Second nested while
for i in range(0, 8):    
	s.add(flag[0 + i] + flag[8 + i] + flag[16 + i] + flag[24 + i] == sum_2[i])
	s.add(flag[0 + i] ^ flag[8 + i] ^ flag[16 + i] ^ flag[24 + i] == xor_2[i])

5th constraint

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
i3 = 0;
while (i3 < 0x20) {
  char_flag = flag[(long)i3 + 6];
  if ((char_flag < '0') || ('9' < char_flag)) {
    if ((char_flag < 'a') || ('f' < char_flag)) {
      *(undefined4 *)((long)array + (long)i3 * 4) = 0;
    }
    else {
      *(undefined4 *)((long)array + (long)i3 * 4) = 0x80;
    }
  }
  else {
    *(undefined4 *)((long)array + (long)i3 * 4) = 0xff;
  }
  i3 = i3 + 1;
}
iVar1 = memcmp(array,&DAT_00400fc0,0x80);
if (iVar1 != 0) {
  puts("incorrect");
                /* WARNING: Subroutine does not return */
  exit(0);
}

Pseudocode:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
while(i < 32)
{
	char_flag = flag[i];
	if(char_flag.is_not_an_ascii_number)
	{
		if(char_flag.is_not_an_hex_value('a', 'f') //not in range between a and f
		{
			array[i] = 0;	// this shouldn't ever happen 
		}else
		{
			array[i] = 0x80;
		}
	}else
	{
		array[i] = 0xff;
	}
	++i;
}
if(array != *0x00400fc0)
{
	error;
}

So in a specific index there must be a number (0 --> 9) or a char (a --> f).

number = 0xff, char = 0x80

0x00400fc0 content:

1
[0x00000080, 0x00000080, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x00000080, 0x00000080, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x00000080, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff]

z3 code:

1
2
3
4
5
6
7
8
9
10
n_or_c = [0x00000080, 0x00000080, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x000000ff,
        0x00000080, 0x000000ff, 0x000000ff, 0x00000080, 0x00000080, 0x000000ff, 0x000000ff, 0x00000080,
        0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x00000080, 0x00000080, 0x000000ff, 0x000000ff,
        0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff]

for i in range(0, 32):
	if(n_or_c[i] == 0x80):
		s.add(And(flag[i] >= 97, flag[i] <= 102))
	else:
		s.add(And(flag[i] >= 48, flag[i] <= 57))

6th constraint

1
2
3
4
5
6
if ((((flag[0x25] != '5') || (flag[7] != 'f')) || (flag[0xb] != '8')) ||
	(((flag[0xc] != '7' || (flag[0x17] != '2')) || (flag[0x1f] != '4')))) {
	puts("incorrect");
				/* WARNING: Subroutine does not return */
	exit(0);
}

Ok no need for pseudocode because is self explanatory.

z3 code:

1
2
s.add(flag[1] == ord('f'),flag[5] == ord('8'), flag[6] == ord('7'),
      flag[17] == ord('2'), flag[25] == ord('4'), flag[31] == ord('5'))

Ok we have finished to check the bonds of the crackme. Let’s write a final exploit

Exploit

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
#!/usr/bin/env python3

from z3 import *
import sys

# Global variables
s = Solver()
charset = '0123456789abcdef'
freq = [0x00000003, 0x00000002, 0x00000002, 0x00000000, 0x00000003, 0x00000002, 0x00000001, 0x00000003,
        0x00000003, 0x00000001, 0x00000001, 0x00000003, 0x00000001, 0x00000002, 0x00000002, 0x00000003]
sum_1 = [0x0000015e, 0x000000da, 0x0000012f, 0x00000131, 0x00000100, 0x00000131, 0x000000fb, 0x00000102]
xor_1 = [0x00000052, 0x0000000c, 0x00000001, 0x0000000f, 0x0000005c, 0x00000005, 0x00000053, 0x00000058]
sum_2 = [0x00000129, 0x00000103, 0x0000012b, 0x00000131, 0x00000135, 0x0000010b, 0x000000ff, 0x000000ff]
xor_2 = [0x00000001, 0x00000057, 0x00000007, 0x0000000d, 0x0000000d, 0x00000053, 0x00000051, 0x00000051]
n_or_c = [0x00000080, 0x00000080, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x000000ff,
          0x00000080, 0x000000ff, 0x000000ff, 0x00000080, 0x00000080, 0x000000ff, 0x000000ff, 0x00000080,
          0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x00000080, 0x00000080, 0x000000ff, 0x000000ff,
          0x000000ff, 0x000000ff, 0x00000080, 0x000000ff, 0x000000ff, 0x000000ff, 0x00000080, 0x000000ff]
flag = [BitVec('{:2}'.format(i), 8) for i in range(32)]

def chars_limit():
    for i in range(0, 32):
        s.add(And(Or(And(flag[i] >= 48, flag[i] <= 57), And(flag[i] >= 97, flag[i] <= 102)), flag[i] != 51))

def frequencies():
    for i, char in enumerate(charset):
        counter = 0
        for x in flag:
            counter += If(x == ord(char), 1, 0)
        s.add(counter == freq[i])

def sumxor1():
    for i in range(0, 8):
        s.add(flag[0 + i * 4] + flag[1 + i * 4] + flag[2 + i * 4] + flag[3 + i * 4] == sum_1[i])
        s.add(flag[0 + i * 4] ^ flag[1 + i * 4] ^ flag[2 + i * 4] ^ flag[3 + i * 4] == xor_1[i])

def sumxor2():
    for i in range(0, 8):   
        s.add(flag[0 + i] + flag[8 + i] + flag[16 + i] + flag[24 + i] == sum_2[i])
        s.add(flag[0 + i] ^ flag[8 + i] ^ flag[16 + i] ^ flag[24 + i] == xor_2[i])

def index_values():
    for i in range(0, 32):
        if(n_or_c[i] == 0x80):
            s.add(And(flag[i] >= 97, flag[i] <= 102))
        else:
            s.add(And(flag[i] >= 48, flag[i] <= 57))

def known_chars():
    s.add(flag[1] == ord('f'),flag[5] == ord('8'), flag[6] == ord('7'),
          flag[17] == ord('2'), flag[25] == ord('4'), flag[31] == ord('5'))

def main(): 
    # Constraint 2
    chars_limit()
    frequencies()
    # Constraint 3/4
    sumxor1()
    sumxor2()
    # Constraint 5
    index_values()
    # Contraint 6
    known_chars()

    # Solve
    if str(s.check()) == 'sat':
        m = s.model()
        model = sorted([(d, m[d]) for d in m], key = lambda x: str(x[0]))
        print("sat\n" + str(model))
    else:
        print(s.check())
        exit(1)

    sys.stdout.write("TWCTF{")
    for m in model:
        sys.stdout.write(chr(m[1].as_long()))
    sys.stdout.write("}\n")

if __name__ == '__main__':
    main()

Flag

TWCTF{df2b4877e71bd91c02f8ef6004b584a5}