Rev0x02

Flag: StarHack{G00d_J0B_78e8ezrzr9}

Challenge

4KB

rev0x02.zip

archive

Description

---

Il faut un clé de licence pour activer le programme!

nc 35.180.44.229 1234

Ce challenge tourne sur un docker et n'est pas disponible

Solution

Commençons par la décompilation de la fonction main, voici le pseudo code sortie par Ghidra avec quelques modifications :

int main() {
  char *licence;
  bool check1_success;
  unsigned int n1;
  unsigned int n2;
  unsigned int n3;
  unsigned int n4;
  unsigned int sum;
  unsigned int licence_part;
  bool check2_success;
  bool check3_success;
  
  licence = (char *)malloc(0x18);
  printf("Bonjour Bonjour reverseur.\n Bienvenue dans m...");
  scanf("%s",licence);
  
  check1_success = check1(licence);
  if (check1_success == 0) {
    puts("Vous essayez d\'utiliser mon programme gratuitement. Allez acheter une licence.");
  } else {
    licence_part = cut(licence,0x4);
    n1 = licence_part;
    licence_part = cut(licence + 0x5,0x4);
    n2 = licence_part;
    licence_part = cut(licence + 0xa,0x4);
    n3 = licence_part;
    licence_part = cut(licence + 0xf,0x4);
    n4 = licence_part;
    licence_part = cut(licence + 0x14,0x4);
    sum = checksum(n1,n2,n3,n4);
    if (licence_part == sum) {
      check2_success = check2(n1,n2,n3,n4);
      if (check2_success == 0) {
        puts("Vous essayez d\'utiliser mon programme gratuitement. Allez acheter une licence.");
      } else {
        check3_success = check3(n1 << 0x10 | n2, licence_part * 0xc0de, n3 << 0x10 | n4);
        if (check3_success == 0) {
          puts("Vous essayez d\'utiliser mon programme gratuitement. Allez acheter une licence.");
        } else {
          puts("Bon travail, mais je pense qu'il n'y a rien...");
          win();
        }
      }
    } else {
      puts("Vous essayez d\'utiliser mon programme gratuitement. Allez acheter une licence.");
    }
  }
  return 0x0;
}

L'objectif est de passer les 3 fonctions check. Commençons par la première :

Check1

Elle vérifie que notre licence à le format XXXX-XXXX-XXXX-XXXX-XXXX où les X sont un caractère dans [0-9A-F] (hexa en majuscule).

bool check1(char *licence) {
  size_t size;
  bool success;
  int i;
  
  size = strlen(licence);
  if ((((size == 24) && (licence[0x4] == '-')) && (licence[0x9] == '-')) && ((licence[0xe] == '-' && (licence[0x13] == '-')))) {
    for (i = 0x0; i < size; i = i + 0x1) {
      if ((licence[i] < '0') || ('F' < licence[i])) {
        if (licence[i] != '-') {
          return 0x0;
        }
      }
      else if ((licence[i] < 'A') && ('9' < licence[i])) {
        return 0x0;
      }
    }
    success= 0x1;
  }
  else {
    success= 0x0;
  }
  return success;
}

Checksum

Ensuite, notre licence est découpée en fonction des blocs qu'elle forme, puis l'hexa décimal est interprété en tant que nombre, on a donc 5 entiers. Par exemple si notre licence est DEAD-BEAF-C0FE-BABE-1337, cela correspond à [57005, 48815, 49406, 47806, 4919].

Les 4 premiers nombres servent à calculer le 5ᵉ. C'est la fonction checksum qui permet cela.

unsigned int checksum(unsigned int n1, unsigned int n2, unsigned int n3, unsigned int n4) {
  return n2 * 0x2 & n1 >> 0x1 ^ n3 ^ n4;
}

Check3

On passe directement au 3ᵉ check pour s'éviter des problèmes. Elle prend trois paramètres notés p1, p2 et p3 et qui sont calculés comme suit :

p1 = n1 << 0x10 | n2
p2 = checksum * 0xc0de
p3 = n3 << 0x10 | n4

bool check3(unsigned int p1, unsigned int p2, unsigned int p3) {
  return p3 == (~p2 | p1) + (~p1 | p2) + ~(p1 | p2) * -0x2 + (p1 & p2) * -0x2;
}

Résolution avec z3

Maintenant que l'on connaît les conditions, on va créer des contraintes pour réduire le nombre de licences possibles, puis les tester une à une. Pour ça, on utilise z3.

• n1 jusqu'à n5 représente nos blocs

• p1, p2 et p3 sont les paramètres passés à check3

from z3 import *
import subprocess

s = Solver()
n1 = BitVec('n1', 32)
n2 = BitVec('n2', 32)
n3 = BitVec('n3', 32)
n4 = BitVec('n4', 32)
n5 = BitVec('n5', 32)
p1 = BitVec('p1', 32)
p2 = BitVec('p2', 32)
p3 = BitVec('p3', 32)

# Les blocs font 2 octets, donc n1-5 peuvent aller jusque 2**16, soit 65536
s.add(n1 >= 0, n1 < 65536)
s.add(n2 >= 0, n2 < 65536)
s.add(n3 >= 0, n3 < 65536)
s.add(n4 >= 0, n4 < 65536)
s.add(n5 >= 0, n5 < 65536)

# Ici on ajoute la formule du checksum, pour forcer n5 à être bon
s.add(n5 == n2 * 0x2 & n1 >> 0x1 ^ n3 ^ n4)

# On définit les paramètres de check3
s.add(p1 == n2 | (n1 << 16))
s.add(p2 == 0xC0DE * n5)
s.add(p3 == n4 | (n3 << 16))

# On applique check3
s.add(p3 == (p2 | ~p1) + (p1 | ~p2) - 2 * ~(p2 | p1) - 2 * (p2 & p1))

# Tant qu'une solution existe, on affiche
while s.check() == sat:
  model = s.model()
  licence = '-'.join([f'{model[n].as_long():0>4X}' for n in [n1, n2, n3, n4, n5]])

  # Test en direct la licence
  out = subprocess.run(f'echo {licence} | ./task', shell=True, capture_output=True).stdout.decode()
  if 'Allez acheter une licence' not in out:
    print(licence)
  
  # Sert à trouver une nouvelle solution
  s.add(Or(n1 != model[n1], n2 != model[n2], n3 != model[n3], n4 != model[n4]))

Unintended way

La clé 0000-0000-0000-0000-0000 fonctionnait.