TokyoWesterns CTF 2019 - Easy Crack Me

Bypass constraints in binary using z3.

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 :

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.

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 :

pass to the program one argument –> flag
the length of the flag must be 0x27 = 39
The first 6 byte of the flag are "TWCTF{"
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).

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:

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.

[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.

#!/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

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:

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 :

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

Second nested while in pseudocode:

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:

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 :

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

z3 code :

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

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:

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:

[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:

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

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:

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

#!/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}

@PatchFriday meme