[Sthack][Writeup – Reverse] Sharko’s specials

Introduction

Quand on clique sur le lien du challenge, on reçoit un binaire, ainsi qu’un lien vers un site web nous demandant de rentrer 10 nombres (Le site étant down, et n’ayant pas pris de capture d’écran pendant le CTF, vous allez bien devoir me croire !)
Quand on lance le binaire, on se retrouve face à dix inputs, et un check de fin qui nous dit si nos nombres sont corrects ou pas.

$> ./challenge
#########THE#######ZIG######&####SHARKO##LOTERY#########
Enter number 0 : 0
Enter number 1 : 1
Enter number 2 : 2
Enter number 3 : 3
Enter number 4 : 4
Enter number 5 : 5
Enter number 6 : 6
Enter number 7 : 7
Enter number 8 : 8
Enter number 9 : 9
Your code is : Time to check if it’s good…Nop you failed

Bref on comprend assez vite qu’il faudra envoyer ces nombres dans le site web pour valider le challenge final.

Investigation

$> file challenge
challenge: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, with debug_info, not stripped

OK cool, c’est du elf pas strippé avec les debug infos, ça devrait être super facile ! (spoiler: non)
Un petit call à strings ne donne rien de très probant, dommage 😉
Dès qu’on ouvre avec ghidra (NSA > 1600$/an), on check la petite partie fonctions, mais on comprend pas grand chose…

Liste des fonctions

Où est mon main ?? Oo
Je n’ai que des fonctions std.XXXX :/
Bon on a une fonction start qui appelle tout de même std.start.posixCallMainAndExit();, ça sent le bon main, on va checker ce qui se trame la dedans :

Fonction main

OK c’est le bazar, ça ressemble pas à un main normal, j’ai bien l’impression qu’il va falloir un peu se casser la tête finalement :/ (même si on reconnait les petits argc/argv classiques)

Détails d’une fonction

Etrange ces trucs qui se baladent…
En googlant un peu sur ces std.io.writer.Writer.CaNenFinitJamais, on tombe assez vite sur des issues d’un langage de programmation appelé Zig, basé sur le C : https://github.com/ziglang/zig
Et ce truc, en le compilant, nous donne ces lignes assez affreuses.

Le décompilo de ghidra comprend que dalle :/
Va falloir passer par l’asm, finalement j’aurais peut-être préféré un binaire stripped…

Bon en fouillant un peu dans l’asm, et avec quelques guess (On nous demande 10 nombres, et ça calcule une solution avec, ça ressemble pas mal à un keygen), j’arrive à trouver un cmp suivi de deux jump vers des prints différents, ça sent quand même bien la fonction de verif finale !

Forrest Jump

Ici le mov esi unnamed_XX correspond au chargement de la string Nice you win ou Nop you failed.
On teste avec gdb en posant un breakpoint sur la comparaison, puis on va rentrer n’importe quels nombres et essayer de set le fameux dl à 0x10.

Et tu breakes, et tu breakes, et tu breakes

set dl

Impec, on a bien le « You Win » qui s’affiche. Bon ça nous permet pas de valider le flag vu qu’on a rentré n’importe quoi (pour devenir n’importe qui), mais au moins on est plus perdu dans le code et on a un point de départ !
En remontant un peu plus haut dans l’asm, on trouve toute une série de récupération de data depuis la st(h)ack, avec des opérations sur les différentes valeurs, suivies d’une petite comparaison ensuite.

Opérations sur les valeurs

Bon on dirait bien qu’il va falloir passer toutes les comparaisons, et que chacune d’entre elle nous permettra d’incrémenter le fameux registre dl jusqu’à 0x10.
On va mixer un peu dynamique et statique pour regarder les différentes valeurs qu’on compare.

Vérification de RAX

J’ai choisi les valeurs 00 11 22 33 44 55 66 77 88 99 pour les nombres afin de bien les reconnaître pendant l’analyse dynamique.
Ici après un break sur le premier mov AL,byte ptr [rsp + local_120+0x3] , on a RAX à 0x21 (33).
La première comparaison va donc récupérer le nombre n°3, le multiplier par 2 ( ADD AL,AL ), et le comparer avec byte ptr [RSP +local_118+0x1].
Je n’ai pas la valeur de la local_118, du coup je stepi dans gdb jusqu’à la comparaison et j’affiche sa valeur, ce qui nous donne 0x63 (99).

stepi

Ok, ici on se rend compte qu’on a une première règle, 2 * le nombre n°3 doit être égal au nombre n°9.

Ca va probablement continuer comme ça, il va donc falloir écrire des contraintes.
Pour ça, y’a un super tool: z3 (https://github.com/Z3Prover/z3) seulement pas de z3 avec moi sur le pc, et impossible de l’installer pour une erreur stupide de python, du coup on va se taper les contraintes àla main 🙁 (ça va elles n’ont pas l’air si complexes).

Petit bonus, en rentrant des nombres supérieurs à 0x32 dans les inputs, le programme tente de nous afficher une chaine de caractère construite à partir des nombres qu’on lui donne, on sait donc qu’il faut lui filer de l’ascii printable. C’est cool, ça réduit pas mal le champ des possibles, notamment au niveau de la première contrainte.

#########THE#######ZIG######&####SHARKO##LOTERY#########
Enter number 0 : 69
Enter number 1 : 23
Enter number 2 : 76
Enter number 3 : 68
Enter number 4 : 98
Enter number 5 : 45
Enter number 6 : 76
Enter number 7 : 23
Enter number 8 : 79
Enter number 9 : 76
Your code is : ELDb-LOL
Time to check if it’s good…Nop you failed

Je ne vais pas vous imposer le reverse de chacune des contraintes (déja que vous avez lu jusque là, c’est plutôt pas mal), mais après quelques bricolages on se retrouve avec ces contraintes (simplifiées ici).

n°9 == (n°3 * 2)
n°8 == (n°4 + 1)
n°5 == (n°7 + 3)
n°0 == (n°7 + 20)
n°6 == (n°0 + 13)
n°0 == 69
n°1 % 15 == 7
n°2 == (n°8 + 1)

Bien qu’il nous en manque encore pas mal, sachant que certains des nombres nous sont directement donnés, on peut commencer à écrire quelques nombres qui  fonctionnent (ou qui ont l’air), on lance gdb, on pose un breakpoint sur le check du registre dl, on voit sa valeur et ça nous indiquera si on a progressé ou pas dans l’analyse !

On breake sur dl

Ok on a déja une miniphrase un peu plus intelligible, et on avance dans les contraintes, seulement 4 sont fausses ici !
(rassurez-vous ça a mis beaucoup plus de temps en vrai, ces foutues contraintes sont pas si évidentes)
On est sur la bonne voie, reste plus qu’à trouver les dernières !

Solution

Après plusieurs cheveux en moins sur la tête, de nouvelles comparaisons retournées dans tous les sens, et quelques tentatives (infructueuses 🙁 ) de bruteforce de la dernière contrainte qu’il me manquait (pas moyen de la trouver dans ce binaire), je finis par me rendre compte que j’ai mis un +1 à un endroit qui n’en méritait pas !
On arrive à ce tableau de nombres :

• 69
• 97
• 116
• 52
• 109
• 52
• 82
• 49
• 110
• 104

#########THE#######ZIG######&####SHARKO##LOTERY#########
Enter number 0 : 69
Enter number 1 : 97
Enter number 2 : 116
Enter number 3 : 52
Enter number 4 : 109
Enter number 5 : 52
Enter number 6 : 82
Enter number 7 : 49
Enter number 8 : 110
Enter number 9 : 104
Your code is : Eat4m4R1nh
Time to check if it’s good…Nice, you win.

ET BIM !
Plus qu’a aller valider sur la page web fournie avec les bons nombres, et c’est bon à nous les puntos !
Un challenge qui m’a donné du fil à retordre, mais heureusement le registre dl permet, en analysant sa  valeur à la fin de la primitive, de se rendre compte si l’on est en train d’écraser des contraintes, ainsi que de valider celles qui ont été reverse.