Write-Up Moth ECW 2023

Description

Find the correct entry.

Write-Up

To solve this reverse challenge, let’s open our favorite reverse engineering tool : for me it is IDA.

The first step is to find the main function to get an overview of the binary.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


__int64 __fastcall main(int a1, char **a2, char **a3)
{
  if ( a1 != 2 )
    return 1LL;
  if ( strlen(a2[1]) == 81 && (unsigned int)sub_11CD(a2[1]) )
  {
    puts("Well done, flag is ECW{md5(input)}");
    return 0LL;
  }
  else
  {
    puts("Nope");
    return 1LL;
  }
}

As you can see, main is quite simple: there are checks on the input passed as a binary argument. Now, we rename variables, set types and add comments.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


__int64 __fastcall main(int nb_args, char **input_args, int a3)
{
  if ( nb_args != 2 )
    return 1LL;
  if ( strlen(input_args[1]) == 81 && (unsigned int)check_func(input_args[1]) )
  {
    puts("Well done, flag is ECW{md5(input)}"); // here is the flag
    return 0LL;
  }
  else
  {
    puts("Nope");                               // wrong input 
    return 1LL;
  }
}

So, the input must be size 81 and the check_func function must not return 0. Let’s take a look at the check_func().

 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


_BOOL8 __fastcall check_func()(__int64 a1)
{
  char v2; // [rsp+12h] [rbp-2Eh]
  char v3; // [rsp+13h] [rbp-2Dh]
  int v4; // [rsp+14h] [rbp-2Ch]
  int i; // [rsp+18h] [rbp-28h]
  int j; // [rsp+1Ch] [rbp-24h]
  int k; // [rsp+20h] [rbp-20h]
  int m; // [rsp+24h] [rbp-1Ch]
  int n; // [rsp+28h] [rbp-18h]
  int ii; // [rsp+2Ch] [rbp-14h]
  int v11; // [rsp+30h] [rbp-10h]
  int jj; // [rsp+34h] [rbp-Ch]

  v4 = 0;
  for ( i = 0; i <= 8; ++i )
  {
    for ( j = 0; j <= 8; ++j )
    {
      v2 = *(_BYTE *)(9 * i + j + a1);
      if ( v2 <= 96 || v2 > 101 )
        return 0LL;
      v3 = byte_2020[9 * i + j];
      if ( v2 - 96 > (int)sub_1169((unsigned int)v3) )
        v4 |= 1u;
      for ( k = 0; k <= 8; ++k )
      {
        for ( m = 0; m <= 8; ++m )
        {
          if ( (m != j || k != i) && v3 == byte_2020[9 * k + m] && v2 == *(_BYTE *)(9 * k + m + a1) )
            v4 |= 2u;
        }
      }
      for ( n = -1; n <= 1; ++n )
      {
        for ( ii = -1; ii <= 1; ++ii )
        {
          if ( j + ii >= 0
            && i + n >= 0
            && j + ii <= 8
            && i + n <= 8
            && (ii || n)
            && v2 == *(_BYTE *)(9 * (n + i) + j + ii + a1) )
          {
            v4 |= 4u;
          }
        }
      }
    }
  }
  v11 = 0;
  for ( jj = 0; jj <= 2; ++jj )
    v11 += (v4 >> jj) & 1;
  return v11 == 0;
}

The function is not that long but we can see many loop and verification. Let’s rename variables and split the code.

First, there is an important buffer byte_2020 :

1
2
3
4
5
6
7
8
9


01 01 01 01 02 03 03 04 05 
06 01 07 02 02 03 04 04 05 
06 07 07 07 02 02 08 04 05 
06 07 09 09 09 09 08 04 05 
06 0A 09 0B 0B 08 08 08 0D 
0A 0A 0A 0C 0B 0B 0E 0D 0D 
0A 0F 0F 0C 0B 0E 0E 0E 0D 
10 0F 0F 0F 12 13 13 13 0D 
10 10 11 12 12 12 12 13 13

And the first part of the code :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


v4 = 0;
  for ( i = 0; i <= 8; ++i )
  {
    for ( j = 0; j <= 8; ++j )
    {
      current_char = input[9 * i + j];                                          // we iterate over all the 9x9 input matrice
      if ( current_char <= 96 || current_char > 101 )                           // eache char must be between 'a' and 'e'
        return 0LL;
      buffer_current_char = strange_buffer[9 * i + j];                          // take the buffer char at the same position as the input
      if ( current_char - 96 > (int)count_itteration(buffer_current_char) )     // we check that the index of the current character is greater than the iterations of the current buffer character in the buffer
        v4 |= 1u;

There is some condition to check that each character of the input is between ‘a’ and ’e’ and that the index of the current character is greater than the number of iterations of the current buffer character in the buffer

Next part :

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


for ( k = 0; k <= 8; ++k )
      {
        for ( m = 0; m <= 8; ++m )
        {
          if ( (m != j || k != i)
            && buffer_current_char == strange_buffer[9 * k + m]                 
            && current_char == input[9 * k + m] )                               
          {
            v4 |= 2u;
          }
        }
      }

This part is quiet complexe : this code is used to check a special condition similar to Sudoku: characters cannot appear twice in the same group: they must be unique in each group (a group represents all the cells with the same value in the buffer seen above).

And finally the last part :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


for ( n = -1; n <= 1; ++n )
      {
        for ( ii = -1; ii <= 1; ++ii )
        {
          if ( j + ii >= 0
            && i + n >= 0
            && j + ii <= 8
            && i + n <= 8
            && (ii || n)
            && current_char == input[9 * n + 9 * i + j + ii] )
          {
            v4 |= 4u;
          }
        }
      }

This condition verifies that two characters are not identical if they are neighbors in the matrix (including the diagonals).

Looking at the composition of the groups, we notice that group 0x11 is made up of just one square. So, according to the condition `if ( current_char - 96 > (int)count_itteration(buffer_current_char) )``, this cell must contain the character ‘a’.

We therefore have a list of conditions that our input must meet to validate the challenge:

The character at index [8][2] is a ‘a’
Each character must be between ‘a’ and ’e’
Neighboring characters must not be identical
Characters in the same group must not be identical

We can now write a z3 script to find the perfect input that match all the conditions.

 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


from z3 import *

# 9x9 z3 matrice
matrice = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(9)] for i in range(9)]
s = Solver()

# groups from buffer
groupes = [
    [1, 1, 1, 1, 2, 3, 3, 4, 5],
    [6, 1, 7, 2, 2, 3, 4, 4, 5],
    [6, 7, 7, 7, 2, 2, 8, 4, 5],
    [6, 7, 9, 9, 9, 9, 8, 4, 5],
    [6, 10, 9, 11, 11, 8, 8, 8, 13],
    [10, 10, 10, 12, 11, 11, 14, 13, 13],
    [10, 15, 15, 12, 11, 14, 14, 14, 13],
    [16, 15, 15, 15, 18, 19, 19, 19, 13],
    [16, 16, 17, 18, 18, 18, 18, 19, 19]
]

# Each character must be between 'a' and 'e'
for i in range(9):
    for j in range(9):
        s.add(And(1 <= matrice[i][j], matrice[i][j] <= 5))

# The character at index [8][2] is a 'a'
s.add(matrice[8][2] == 1)

# Characters in the same group must not be identical
for k in range(1, 20):  # Il y a 19 groupes
    cells = [(i, j) for i in range(9) for j in range(9) if groupes[i][j] == k]
    s.add(Distinct([matrice[i][j] for i, j in cells]))

for i in range(9):
    for j in range(9):
        groupe_courant = groupes[i][j]
        count = sum(1 for x in range(9) for y in range(9) if groupes[x][y] == groupe_courant)
        s.add(matrice[i][j] <= count)

# Neighboring characters must not be identical
for i in range(9):
    for j in range(9):
        for dx in [-1, 0, 1]:
            for dy in [-1, 0, 1]:
                if 0 <= i + dx < 9 and 0 <= j + dy < 9 and (dx != 0 or dy != 0):
                    s.add(matrice[i][j] != matrice[i + dx][j + dy])

# Solve the chall
if s.check() == sat:
    m = s.model()
    solution = [[m.evaluate(matrice[i][j]).as_long() for j in range(9)] for i in range(9)]
    # Convert decimal into chars
    for i in range(9):
        for j in range(9):
            solution[i][j] = chr(96 + solution[i][j])  # Convert 1 to 'a', 2 to 'b', etc.
    
    # Convert the matrice into a string
    solution_str = ''.join(''.join(row) for row in solution)
    print(solution_str)
else:
    print("Pas de solution!")

Let’s execute the script :

1
2


(.venv) ➜  Rev python3 reverse.py                             
bcaedbabaadbcacdcdbcadbebabdebecaceccadadedabdbebcbcedcacaedababebdbcedcacacedaba

The flag is the md5 of this input.

Flag

ECW{5e438f1fd92d68afe17d89f8004b8ea7}