Ce challenge très simple de reverse est issu du CTF interIUT. Il m’a semblé intéressant d’en faire le write-up car il permet de faire une petite introduction au module Python intitulé z3, qui va ici nous aider à résoudre un système d’équations.
Description du challenge
Arriverez-vous à trouver le flag qui répond à ce Théorème ?
Auteur : @Masterfox
Fichier du challenge
Le binaire à reverse pour ce challenge est disponible ici : bithagore.
Première approche
Comme d’habitude on commence par faire un file sur le binaire pour avoir une première idée d’à quoi s’attendre.
$ file bithagore
bithagore: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-, for GNU/Linux 3.2.0, BuildID[sha1]=bca6f2fa1ddcb0503f230aa80864d7bea6db79f9, not strippedOk on a donc ici un ELF x86_64 (32 bits) non strippé, linké dynamiquement mais cela ne va pas nous servir ici
On peut donc ensuite ouvrir le main du programme et le flowchart nous saute aux yeux.
On voit donc ici qu’il va sans doute nous falloir valider un grand nombre de conditions pour avoir un flag correct…
Reverse
Début du main : arguments
On va quand même faire les choses dans l’ordre et observer le fonctionnement général du programme. On commence donc en haut du main.
Dans ce premier bloc (on passera ici le détail du call à __x86_get_pc_thunk_bx pour ne pas se perdre, ce n’est pas nécessaire de savoir ce qu’il se passe avec cette fonction), on voit globalement que si ECX est plus petit ou égal à 1 alors le programme jump à la fin du programme (on y reviendra plus tard).
Il nous faut donc ECX supérieur ou égal à 2 ! Mais qu’est-ce que c’est ?
Et bien si on remonte dans ce premier bloc du main on voit qu’ECX va pointer vers ESP+4, c’est-à-dire argc ! Un argc égal à 1 signifie qu’aucun argument n’a été passé au programme lors de l’appel. Il va donc ici nous falloir avoir argc >= 1 soit au moins un argument 🙂
Fin du main : 3 possibilités
Pour confirmer notre hypothèse, on peut ensuite jump à la fin du main.
On remarque ici 3 terminaisons différentes du main qui convergent ensuite vers un même bloc destiné à vérifier la présence de buffer overflow (utilisant le principe de la stack canary mais ceci fera l’objet d’un prochain article).
Dans le cas où nous n’avons pas entré un argument au moins avec le programme, on jump sur le bloc que j’ai appelé BAD_USAGE qui va juste afficher “%s <flag>” (avec %s qui sera remplacé par le nom du programme) pour indiquer l’usage du programme : il faut donc bien un argument qui sera le flag !
Dans les deux autres cas, une chaine différente nous est affichée : unk_804A008 ou unk_804A030.
On voit ici que les buffer sont en fait des chaines de caractères que l’on peut reconstituer en appuyant sur la touche “A” sur IDA après avoir sélectionné la première lettre de la chaine.
On a donc quelque chose de plus lisible.
Pseudo code FTW
OK ! Bon c’est bien gentil tout ça mais maintenant on veut le flag ! Alors pour ça bah pas de grande surprise… Il va falloir analyser le code et plus spécifiquement les différentes conditions nécessaires à ce que notre flag entré en argument soit le bon (malinx).
Pour cela on peut regarder chaque condition dans l’assembleur mais ce serait une perte de temps face à la puissance du pseudo-code généré par IDA (Cutter, Ghidra ou encore Binary Ninja peuvent aussi générer un pseudo code).
On génère donc le pseudo code du main et on obtient ceci.
int __cdecl main(int argc, const char **argv, const char **envp)
{
const char *v3; // edx
char v4; // si
char v6; // cl
__int16 v7; // ax
int v8; // esi
char v9; // [esp+1h] [ebp-39h]
int v10; // [esp+6h] [ebp-34h]
int v11; // [esp+Ah] [ebp-30h]
char v12; // [esp+Ah] [ebp-30h]
char v13; // [esp+Eh] [ebp-2Ch]
char v14; // [esp+Fh] [ebp-2Bh]
char v15; // [esp+Fh] [ebp-2Bh]
char v16; // [esp+10h] [ebp-2Ah]
char v17; // [esp+10h] [ebp-2Ah]
char v18; // [esp+11h] [ebp-29h]
if ( argc <= 1 )
{
((void (__cdecl *)(signed int, const char *, const char *))__printf_chk)(1, "%s <flag>\n", *argv);
}
else
{
v3 = argv[1];
v4 = v3[12];
if ( v3[12] < 0 )
goto LABEL_50;
if ( v3[10] != 103 )
goto LABEL_50;
v6 = v3[19];
v18 = v3[23];
if ( v18 + v6 != 244 )
goto LABEL_50;
if ( v3[2] != 71 )
goto LABEL_50;
v16 = v3[20];
v12 = v3[21];
if ( ((unsigned __int8)v16 ^ 0x42) != v12 )
goto LABEL_50;
if ( v3[15] != 116 )
goto LABEL_50;
if ( v6 >> 5 != 3 )
goto LABEL_50;
if ( v6 != 119 )
goto LABEL_50;
if ( v12 >> 3 != 14 )
goto LABEL_50;
LOBYTE(v10) = v3[11];
if ( (char)v10 >> 1 != 24 )
goto LABEL_50;
if ( v3[1] != 50 )
goto LABEL_50;
v13 = v3[17];
v14 = v3[8];
if ( v13 >> v14 % 8 != 51 )
goto LABEL_50;
if ( v13 != 51 )
goto LABEL_50;
if ( v3[6] != 49 )
goto LABEL_50;
if ( v16 != 49 )
goto LABEL_50;
if ( v3[5] != 98 )
goto LABEL_50;
v17 = v3[13];
if ( (unsigned __int8)v17 << 24 != 855638016 )
goto LABEL_50;
if ( v12 == 115
&& v18 << 6 == 8000
&& (LOBYTE(v11) = v3[4], v4 >> (char)v11 % 8 == 14)
&& v4 == 114
&& v14 == 104
&& (LOBYTE(v7) = *v3 / 8, HIBYTE(v7) = *v3 % 8, !(v7 & 0xFF00))
&& (v9 = v3[14], v3[16] << v9 % 8 == 13312)
&& v3[9] == 52
&& (v15 = v3[18], v15 % 8 == 7)
&& v3[3] == 50
&& v11 << 24 == 2063597568
&& (v8 = v3[7], v10 = (char)v10, v8 + (char)v10 == 164)
&& v18 % 8 == 5
&& v3[16] == 104
&& 2 * v8 == 232
&& 119 >> v3[7] % 8 == 7
&& v3[22] == 51
&& v9 == 95
&& *v3 == 72
&& v17 >> 5 == 1
&& (_BYTE)v11 == 123
&& v15 >= 0
&& v18 == 125
&& v10 == 48
&& v15 == 95
&& v8 << 7 == 14848
&& v17 == 51 )
{
puts("Bien joué, tu peux soumettre ce flag !");
}
else
{
LABEL_50:
puts("C'est loupé !");
}
}
return 0;
}On voit ici ligne 28 que la variable v3 correspond à argv[1] c’es à dire au flag que l’on entre en paramètre. Ensuite, tout un tas de checks sont effectués sur les différents caractères du flag et si toutes ces conditions passent alors le flag est validé.
Python & z3 FTW
Récupérer ce flag revient donc à résoudre un système d’équations ! Lors du CTF je l’ai résolu à la main mais en y réfléchissant c’est une bonne opportunité pour s’introduire à z3.
Bon dans notre cas c’est un petit peu overkill dans le sens où nous avons presque la totalité des caractères directement : exemple ligne 32-33.
if ( v3[10] != 103 )
goto LABEL_50;Il faut ici que v3 (qui est donc notre flag) aie en onzième caractère (ne pas oublier que l’on commence à l’indice 0) le caractère correspondant à la valeur 103 en décimal, sans quoi le programme va jump sur le bloc indiquant que ce n’est pas le bon flag.
Python 3.9.0 (default, Nov 21 2020, 14:01:55)
[Clang 11.0.0 (clang-1100.0.33.17)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> chr(103)
'g'Le onzième caractère du flag est donc un ‘g’, et ainsi de suite…
On va donc réunir toutes ces conditions dans un script python en utilisant le solver z3.
from z3 import *
flag = [BitVec(f"flag[{i}]", 8) for i in range(24)]
s = Solver()
s.add(flag[0] == 72)
s.add(flag[1] == 50)
s.add(flag[2] == 71)
s.add(flag[3] == 50)
s.add(flag[4] == ord('{')) # GUESSING car les flags commencent par "H2G2{"
s.add(flag[5] == 98)
s.add(flag[6] == 49)
s.add(0x30 + flag[7] == 164)
s.add(flag[8] == 104)
s.add(flag[9] == 52)
s.add(flag[10] == 103)
s.add(flag[11] >> 1 == 24)
s.add(flag[12] == 114)
s.add(flag[13] == 51)
s.add(flag[14] == 95)
s.add(flag[15] == 116)
s.add(flag[16] == 104)
s.add(flag[17] == 51)
s.add(flag[18] == 95)
s.add(flag[19] == 119)
s.add(flag[20] == 49)
s.add(flag[21] == 115)
s.add(flag[22] == 51)
s.add(flag[23] == 125)
print(s.check())
if(str(s.check()) == "sat"):
print(s.model())Le s.check() va nous afficher au choix “sat” ou “unsat” si z3 trouve ou non une solution à notre sytème d’équations. Dans le cas où une solution est bien trouvée, on affiche cette solution.
$ python3 bithagore_z3.py
sat
[flag[11] = 48,
flag[23] = 125,
flag[22] = 51,
flag[21] = 115,
flag[20] = 49,
flag[19] = 119,
flag[18] = 95,
flag[17] = 51,
flag[16] = 104,
flag[15] = 116,
flag[14] = 95,
flag[13] = 51,
flag[12] = 114,
flag[10] = 103,
flag[9] = 52,
flag[8] = 104,
flag[7] = 116,
flag[6] = 49,
flag[5] = 98,
flag[4] = 123,
flag[3] = 50,
flag[2] = 71,
flag[1] = 50,
flag[0] = 72]Super ! On a donc une belle solution contenant la valeur en décimal de chaque caractère du flag 😀
Il n’y a plus qu’à tout remettre dans l’ordre à la main et à tout décoder encore à la main….. BAHAHAHAHAH très bonne blague Michel.
Hop hop hop ni une ni deux on automatise ça ! On veut un joli script qui nous affiche un joli flag ! On ajoute donc cette portion de code à notre script.
if(str(s.check()) == "sat"):
final_flag = ""
flag = str(s.model()).replace(',', '').split('\n')
flag[0] = flag[0][1:] # Enlève '[' au début
flag[23] = flag[23][:-1] # Enlève ']' à la fin
flag.insert(13, flag[0]) # Met flag[11] à la bonne place (en premier à la base)
flag.pop(0) # Supp flag[11] en première position (déjà copié à la bonne place)
flag.reverse() # inverse l'ordre de la liste
for line in flag:
final_flag += chr(int(line.split('=')[1]))
print(f'\n[+] FLAG : {final_flag}\n')Il n’y a plus qu’à lancer le script et récupérer le flag !
$ python3 bithagore_z3.py
[+] FLAG : H2G2{b1th4g0r3_th3_w1s3}