Solution de mk_4362 pour Mikado

Table des matières

On a quoi ?

Un énoncé un peu cryptique, si quelqu’un a la référence je suis preneur … je ne vois toujours pas le rapport avec la suite du challenge …

un fichier : binaire
un service en ligne : nc localhost 4000

Si on teste les deux dès le début :

$ ./mikado
[+] Username: toto
[+] Serial:   1def3
[!] Incorrect serial.
 
$ nc localhost 4000
What is a valid serial for username: Hello World
>>> oups
Sorry, that is not a valid serial.
Please check your inputs.

Et on se rend vite compte que le binaire fournit n’est pas directement le service exposé.

On comprend quoi ?

Dans un premier temps le mieux c’est de regarder un peu ce que fait ce binaire … naire et voir que tout est dans la fonction main() :


int main(void)

{
  int iVar1;
  size_t l;
  long in_FS_OFFSET;
  char name [32];
  char serial [40];
  long canary;
  
  canary = *(long *)(in_FS_OFFSET + 0x28);
  setup();
  printf("[+] Username: ");
  fgets(name,0x20,stdin);
  l = strcspn(name,"\n");
  name[l] = '\0';
  printf("[+] Serial:   ");
  fgets(serial,0x20,stdin);
  l = strcspn(serial,"\n");
  serial[l] = '\0';
  iVar1 = check_serial(name,serial);
  if (iVar1 == 0) {
    puts("[!] Incorrect serial.");
  }
  else {
    puts("[>] Valid serial!");
    puts("[>] Now connect to the remote server and generate serials for the given usernames.");
  }
  if (canary != *(long *)(in_FS_OFFSET + 0x28)) {
                    /* WARNING: Subroutine does not return */
    __stack_chk_fail();
  }
  return 0;
}

Le programme :

lit le nom de l’utilisateur (0x20 octets pour un buffer de 32 octets) et le tronque au premier \n trouvé (remplace par un \0)
lit un numéro de série (0x20 octets pour un buffer de 40 octets, on a un peu de marge) et le tronque au premier \n trouvé (remplace par un \0)
efféctue des vérifications sur le numéro de série
si c’est bon on peut aller essayer sur le serveur distant (given usernames … il y en aura plusieurs !! )

Maintenant faut aller voir la fonction check_serial() :


long check_serial(char *name,char *serial)

{
  long canary;
  int x1, x2
  long result;
  long l;
  int *piVar2;
  long in_FS_OFFSET;
  byte bVar3;
  int i, j, k, t, m, n, count, p;
  int A [12];
  int B [12];
  int C [12];
  int buff [9];
  bool test;
  
  bVar3 = 0;
  canary = *(long *)(in_FS_OFFSET + 0x28);
  x1 = scramble(name);
  // le 1er caractère vaut x1
  x2 = ascii_to_ints(*serial);
  if (x1 == x2) {
    // le 10e caractère vaut x1 aussi
    x2 = ascii_to_ints(serial[9]);
    if (x1 == x2) {
      // initialisation à 0 des matrices
      A[0] = 0; A[1] = 0; A[2] = 0; A[3] = 0; A[4] = 0; A[5] = 0; A[6] = 0; A[7] = 0; A[8] = 0;
      B[0] = 0; B[1] = 0; B[2] = 0; B[3] = 0; B[4] = 0; B[5] = 0; B[6] = 0; B[7] = 0; B[8] = 0;
      C[0] = 0; C[1] = 0; C[2] = 0; C[3] = 0; C[4] = 0; C[5] = 0; C[6] = 0; C[7] = 0; C[8] = 0;

      // répartit le serial en deux matrices
      // serial[0:8] -> A
      // serial[9:18] -> B
      for (i = 0; i < 9; i = i + 1) {
        x1 = ascii_to_ints(serial[i]);
        x2 = ascii_to_ints(serial[i + 9]);
        if ((x1 < 0) || (x2 < 0)) {
          result = 0;
          goto LAB_001017d7;
        }
        A[(i / 3) * 3 + (i % 3)] = x1;
        B[(i / 3) * 3 + (i % 3)] = x2;
      }
      // calcul de C = B * A
      for (j = 0; j < 3; j = j + 1) {
        for (k = 0; k < 3; k = k + 1) {
          C[j * 3 + k] = 0;
          for (t = 0; t < 3; t = t + 1) {
            C[j * 3 + k] = C[j * 3 + k] + B[t * 3 + k] * A[j * 3 + t];
          }
        }
      }
      // ça je ne sais pas trop ce que ça fait
      piVar2 = buff;
      for (l = 0x80; l != 0; l = l + -1) {
        piVar2[0] = 0;
        piVar2[1] = 0;
        piVar2 = piVar2 + (ulong)bVar3 * -4 + 2;
      }
      // test sur C : unicité des valeurs c00, c01, c02, c10, c11, c12 ... c22 
      test = true;
      for (m = 0; m < 3; m = m + 1) {
        for (n = 0; n < 3; n = n + 1) {
          buff[C[m * 3 + n]] = buff[C[m * 3 + n]] + 1;
          test = (test & C[m * 3 + n] == (B[m * 3 + n] | A[m * 3 + n] << 4));
        }
      }
      count = 9;
      for (p = 0; p < 0x100; p = p + 1) {
        count = count - (buff[p] != 0);
      }
      if ((count == 0) && (test)) {
        result = 1;
      }
      else {
        result = 0;
      }
      goto LAB_001017d7;
    }
  }
  result = 0;
LAB_001017d7:
  if (canary != *(long *)(in_FS_OFFSET + 0x28)) {

    __stack_chk_fail();
  }
  return result;
}

Avant de détailler, deux autres fonctions sont appelées :

scramble() : effectue une opération en prenant en entrée une chaîne de carctères (le username) et retourne un entier (comme un code correcteur d’erreur par exemple)
ascci_to_ints() : prend en entier un caractère [0-9][a-z][A-F] et retourne sa valeur hexadécimale (ie un nombre [0-15])

Ca donne :

int ascii_to_ints(char param_1)
{
  int resutl;
  
  if ((param_1 < '0') || ('9' < param_1)) {
    if ((param_1 < 'a') || ('f' < param_1)) {
      if ((param_1 < 'A') || ('F' < param_1)) {
        resutl = -1;
      }
      else {
        resutl = param_1 + -0x37;
      }
    }
    else {
      resutl = param_1 + -0x57;
    }
  }
  else {
    resutl = param_1 + -0x30;
  }
  return resutl;
}

int scramble(char *param_1)
{
  size_t l;
  uint t;
  ulong i;
  
  l = strlen(param_1);
  t = 0;
  for (i = 0; i < l; i = i + 1) {
    t = t ^ ((param_1[i] & 7) << 5) ^ (param_1[i] >> 3) ^ 0x44;
  }
  return t % 0xe + 1;
}

Du coup que fait check_serial():

vérifie que le premier caractère du serial (en hexa) vaut le scramble de username
idem pour le 10e caractère
si c’est bon, prend le serial et en ordonne les caractères en deux matrices 3 x 3 (A et B)

==> donc : serial fait 18 caractères hexadécimaux, le 1er et le 10e caractère valent le scramble de username

Ensuite :

calcul de C = B * A

Puis deux tests sur C :

les 9 veleurs de la matrice doivent être uniques (comme un sudoku)
chacune doit vérifier : cij = bij | aij << 4

Que faire ?

Une fois que l’on a compris tout ça … on va utiliser z3 encore une fois, pour lui donner ces contraintes et voir s’il nous trouve des matrices qui correspondent (et si on a A et B on a notre serial)

La partie intéressante du code :

def find_serial(name):

    # déclaration des 3 matrices
    A = [ [ BitVec( "ax%dy%d" % (x, y), 8) for y in range(3) ] for x in range(3) ]
    B = [ [ BitVec( "bx%dy%d" % (x, y), 8) for y in range(3) ] for x in range(3) ]
    C = [ [ BitVec( "cx%dy%d" % (x, y), 8) for y in range(3) ] for x in range(3) ]

    # contrainte sur les valeurs [0-15]
    cells_a  = [ And(1 <= A[i][j], A[i][j] <= 15) for i in range(3) for j in range(3) ]
    cells_b  = [ And(1 <= B[i][j], B[i][j] <= 15) for i in range(3) for j in range(3) ]

    # les éléments de C sont distincts
    sq_c     = [ Distinct([ C[i][j] for i in range(3) for j in range(3) ]) ]

    # relation entre les cij, aij et bij
    eq_c = [ And( C[i][j] == B[i][j] | A[i][j] << 4) for i in range(3) for j in range(3) ] 

    # valeurs connues de a00 et b00
    start_a = [ And(A[0][0] == scramble(name)) ]
    start_b = [ And(B[0][0] == scramble(name)) ]

    # C = A x B
    mult = [ And( C[i][j] == B[i][0]*A[0][j] + B[i][1]*A[1][j] + B[i][2]*A[2][j]) for k in range(3) for i in range(3) for j in range(3)] 

    s = Solver()
    s.add(sq_c + eq_c + start_a + start_b + cells_a + cells_b + mult)

    s.check()
    m = s.model()
    m = str(m)

    # là encore désolé c'est moche
    # je ne sais toujours pas comment récupérer les solutions du solver
    m = m[1:-1].split(',\n ')

    M = {}
    for expr in m:
        k, v = expr.split(' = ')
        M.update({k: int(v)})

    a = [M["ax%sy%d" % (x, y)] for y in range(3) for x in range(3) ]
    b = [M["bx%sy%d" % (x, y)] for y in range(3) for x in range(3) ]
    c = [M["cx%sy%d" % (x, y)] for y in range(3) for x in range(3) ]

    # met en forme le serial et le retourne
    result = ''.join(str(hex(_))[-1] for _ in a) + ''.join(str(hex(_))[-1] for _ in b)

    return result

Finalement

On vérifie que tout ça marche pour le Hello World puis ensuite il suffit d’instrumenter le dialogue avec le serveur.

Le code complet ci-après

$ python3 solve.py
[+] Opening connection to localhost on port 4000: Done
b'Hello World'
b'ANSSI'
b'Team France'
#// je passe ... y'en a beaucoup //
b'VZQfsyMMROOJwb4qf0U'
b'SAOjV0nUKiMcXEI1'
b'g2BLZ4HM3srESZdBRKec'
[+] Receiving all data: Done (99B)
[*] Closed connection to localhost port 4000
b'Well done! Here is the flag\nFCSC{057c45885a3bc012c17738e47ead376dfc33789591b6fb8ed0d38451ab7e6c3f}\n'

solve.py

from z3 import *
from pwn import *
from time import sleep

HOST = "localhost"
PORT = 4000

def scramble(msg):
    l = len(msg)
    t = 0
    for i in range(l):
        c = msg[i]
        t ^= ((c & 7) << 5) ^ (c >> 3) ^ 0x44
    return t % 0xe + 1

def find_serial(name):

    # déclaration des 3 matrices
    A = [ [ BitVec( "ax%dy%d" % (x, y), 8) for y in range(3) ] for x in range(3) ]
    B = [ [ BitVec( "bx%dy%d" % (x, y), 8) for y in range(3) ] for x in range(3) ]
    C = [ [ BitVec( "cx%dy%d" % (x, y), 8) for y in range(3) ] for x in range(3) ]

    # contrainte sur les valeurs [0-15]
    cells_a  = [ And(1 <= A[i][j], A[i][j] <= 15) for i in range(3) for j in range(3) ]
    cells_b  = [ And(1 <= B[i][j], B[i][j] <= 15) for i in range(3) for j in range(3) ]

    # les éléments de C sont distincts
    sq_c     = [ Distinct([ C[i][j] for i in range(3) for j in range(3) ]) ]

    # relation entre les cij, aij et bij
    eq_c = [ And( C[i][j] == B[i][j] | A[i][j] << 4) for i in range(3) for j in range(3) ] 

    # valeurs connues de a00 et b00
    start_a = [ And(A[0][0] == scramble(name)) ]
    start_b = [ And(B[0][0] == scramble(name)) ]

    # C = A x B
    mult = [ And( C[i][j] == B[i][0]*A[0][j] + B[i][1]*A[1][j] + B[i][2]*A[2][j]) for k in range(3) for i in range(3) for j in range(3)] 

    s = Solver()
    s.add(sq_c + eq_c + start_a + start_b + cells_a + cells_b + mult)

    s.check()
    m = s.model()
    m = str(m)

    # là encore désolé c'est moche
    # je ne sais toujours pas comment récupérer les solutions du solver
    m = m[1:-1].split(',\n ')

    M = {}
    for expr in m:
        k, v = expr.split(' = ')
        M.update({k: int(v)})

    a = [M["ax%sy%d" % (x, y)] for y in range(3) for x in range(3) ]
    b = [M["bx%sy%d" % (x, y)] for y in range(3) for x in range(3) ]
    c = [M["cx%sy%d" % (x, y)] for y in range(3) for x in range(3) ]

    # met en forme le serial et le retourne
    result = ''.join(str(hex(_))[-1] for _ in a) + ''.join(str(hex(_))[-1] for _ in b)

    return result


s = remote(HOST, PORT)

while(1):
    try:
        name = s.recvuntil(b'>>> ')
        name = name.split(b'\n')[0].split(b': ')[1]
        print(name)
        s.sendline(find_serial(name).encode())
        sleep(0.2)
    except:
        print(s.recvall())
        break