[CTF GEMA] TSTM3
CTF GEMA Groupe 2025
Niveau de Difficulté : Hard
Catégorie du Challenge : Reverse
Description :
run!
Steps to Solve
Exécution de la question et test
Utilisation de l'outil ltrace
On observe que le programme prend une entrée et vérifie si elle respecte certaines conditions.
Analyse avec Ghidra
En analysant le fichier exécutable avec Ghidra, nous avons trouvé une fonction Check().
Voyons ce qu'elle contient :
Il semble que nous ayons besoin d'un solveur SAT ici...
Débogage avec GDB
En travaillant sur l'index des valeurs et en traçant la sortie avec l'outil GDB,
nous avons maintenant une idée de comment voir le flag.
📌 (Lire plus sur les solveurs SAT pour approfondir)
Code pour récupérer le flag
Exécution du code
Ok, lançons-le ! 🚀
solve code:
from z3 import *
FLAGLEN = 38
flag = [Int(f'flag_{i}') for i in range(FLAGLEN)]
solver = Solver()
solver.add(flag[2] + flag[6] + flag[27] + flag[25] + flag[30] + flag[33] + flag[13] == 421)
solver.add(flag[25] + flag[9] + flag[8] + flag[36] + flag[6] + flag[31] + flag[25] + flag[9] == 506)
solver.add(flag[35] + flag[20] + flag[3] + flag[7] + flag[3] + flag[28] + flag[31] + flag[23] + flag[15] + flag[19] + flag[35] + flag[34] + flag[29] + flag[22] + flag[32] + flag[18] + flag[24] + flag[22] + flag[10] == 1367)
solver.add(flag[34] + flag[18] + flag[32] + flag[11] + flag[26] + flag[31] + flag[37] + flag[35] == 631)
solver.add(flag[24] + flag[1] + flag[15] + flag[25] + flag[26] + flag[20] + flag[22] == 442)
solver.add(flag[19] + flag[3] + flag[31] + flag[9] + flag[6] + flag[9] + flag[15] + flag[9] + flag[2] + flag[6] + flag[37] + flag[16] + flag[30] + flag[12] == 1017)
solver.add(flag[26] + flag[6] + flag[27] + flag[25] + flag[8] + flag[1] + flag[16] + flag[35] + flag[2] + flag[22] + flag[27] + flag[28] + flag[13] + flag[17] + flag[15] == 1050)
solver.add(flag[34] + flag[22] + flag[31] + flag[32] + flag[28] + flag[15] + flag[0] + flag[14] + flag[9] + flag[10] + flag[22] + flag[28] + flag[26] + flag[21] + flag[19] + flag[32] == 1194)
solver.add(flag[3] + flag[16] + flag[9] == 220)
solver.add(flag[14] + flag[3] + flag[7] + flag[21] + flag[25] + flag[10] + flag[23] + flag[3] + flag[7] + flag[37] + flag[13] + flag[24] + flag[14] + flag[37] + flag[4] + flag[13] + flag[37] + flag[37] + flag[31] + flag[36] == 1781)
solver.add(flag[22] + flag[9] + flag[1] + flag[13] + flag[8] + flag[20] + flag[21] + flag[1] + flag[27] + flag[9] + flag[8] + flag[27] + flag[22] + flag[37] + flag[9] + flag[11] + flag[37] + flag[9] + flag[20] == 1234)
solver.add(flag[16] + flag[5] + flag[26] + flag[11] == 253)
solver.add(flag[5] + flag[0] + flag[15] + flag[2] + flag[26] + flag[9] == 388)
solver.add(flag[20] + flag[4] + flag[8] + flag[20] + flag[5] + flag[28] + flag[11] + flag[3] + flag[10] + flag[7] + flag[34] == 800)
solver.add(flag[35] + flag[0] + flag[35] + flag[25] + flag[5] + flag[25] + flag[3] + flag[8] + flag[14] + flag[7] == 596)
solver.add(flag[27] + flag[5] + flag[25] + flag[24] + flag[10] + flag[18] + flag[8] == 455)
solver.add(flag[18] + flag[16] + flag[30] + flag[11] == 298)
solver.add(flag[4] + flag[28] + flag[37] + flag[16] + flag[1] + flag[23] + flag[16] == 672)
solver.add(flag[29] + flag[1] + flag[0] + flag[9] + flag[28] + flag[20] + flag[9] + flag[32] + flag[11] + flag[8] + flag[21] + flag[14] + flag[33] + flag[12] + flag[11] + flag[27] + flag[14] == 1079)
solver.add(flag[13] + flag[2] + flag[6] + flag[11] + flag[33] + flag[17] + flag[14] + flag[23] + flag[5] + flag[8] + flag[17] + flag[5] + flag[15] + flag[16] == 983)
solver.add(flag[3] + flag[25] + flag[36] + flag[11] + flag[37] + flag[3] + flag[4] + flag[1] + flag[14] + flag[2] == 788)
solver.add(flag[31] + flag[27] + flag[33] + flag[27] + flag[18] + flag[5] + flag[15] + flag[5] + flag[31] + flag[17] + flag[15] + flag[25] + flag[20] + flag[29] + flag[28] + flag[24] + flag[7] + flag[29] + flag[16] == 1405)
solver.add(flag[10] + flag[15] + flag[33] + flag[23] + flag[36] + flag[7] + flag[23] + flag[25] + flag[3] + flag[35] + flag[0] + flag[32] + flag[15] + flag[32] + flag[35] + flag[14] == 1205)
solver.add(flag[19] + flag[34] + flag[0] + flag[14] + flag[1] + flag[36] + flag[35] == 452)
solver.add(flag[31] + flag[21] + flag[6] + flag[16] + flag[0] + flag[30] + flag[10] + flag[6] + flag[27] + flag[33] == 676)
solver.add(flag[2] + flag[33] + flag[20] + flag[23] + flag[4] + flag[33] + flag[2] + flag[4] + flag[1] + flag[25] + flag[22] + flag[17] + flag[20] + flag[12] + flag[35] + flag[14] + flag[11] + flag[5] == 1231)
solver.add(flag[27] + flag[29] + flag[32] + flag[20] + flag[1] + flag[13] + flag[2] + flag[26] + flag[12] + flag[21] + flag[19] + flag[8] + flag[30] + flag[1] + flag[10] + flag[1] + flag[22] == 1167)
solver.add(flag[20] + flag[2] + flag[36] + flag[22] + flag[6] + flag[8] == 375)
solver.add(flag[25] + flag[10] + flag[33] + flag[35] + flag[27] + flag[7] + flag[25] + flag[7] + flag[10] + flag[5] + flag[6] + flag[23] + flag[28] + flag[26] + flag[32] + flag[32] + flag[36] + flag[11] == 1312)
solver.add(flag[9] + flag[28] + flag[18] + flag[4] + flag[32] + flag[25] + flag[11] + flag[15] + flag[27] + flag[10] + flag[25] + flag[23] + flag[20] == 983)
solver.add(flag[3] + flag[8] + flag[19] + flag[13] + flag[9] + flag[6] + flag[19] + flag[5] + flag[34] + flag[10] + flag[18] + flag[6] + flag[22] == 836)
solver.add(flag[34] + flag[14] + flag[23] + flag[0] + flag[9] + flag[21] + flag[4] + flag[27] + flag[18] + flag[21] + flag[30] + flag[20] + flag[12] + flag[5] + flag[14] == 970)
solver.add(flag[0] + flag[33] + flag[9] + flag[33] + flag[33] + flag[27] + flag[19] + flag[23] + flag[4] + flag[15] + flag[2] + flag[15] + flag[22] + flag[13] + flag[36] + flag[7] == 1166)
solver.add(flag[10] + flag[14] + flag[2] + flag[31] + flag[16] + flag[1] + flag[8] + flag[9] + flag[20] + flag[28] + flag[1] + flag[19] + flag[20] + flag[12] + flag[29] + flag[19] == 1128)
solver.add(flag[21] + flag[2] + flag[21] + flag[36] + flag[30] + flag[37] + flag[21] + flag[28] + flag[25] + flag[1] == 723)
solver.add(flag[8] + flag[36] + flag[9] + flag[30] + flag[30] + flag[33] + flag[2] + flag[10] + flag[23] + flag[3] == 646)
solver.add(flag[30] + flag[32] + flag[12] + flag[15] + flag[35] + flag[15] + flag[6] + flag[7] + flag[27] + flag[32] + flag[5] + flag[37] + flag[6] + flag[32] + flag[6] + flag[1] + flag[24] + flag[17] + flag[12] + flag[21] == 1571)
solver.add(flag[24] + flag[30] + flag[2] + flag[10] + flag[9] + flag[0] + flag[35] + flag[19] + flag[17] + flag[22] + flag[5] + flag[25] + flag[11] + flag[25] + flag[25] + flag[21] + flag[29] + flag[10] + flag[29] + flag[6] == 1226)
for i in range(FLAGLEN):
solver.add(flag[i] >= 32, flag[i] <= 126)
if solver.check() == sat:
model = solver.model()
flag_str = ''.join([chr(model[flag[i]].as_long()) for i in range(FLAGLEN)])
print(f"Flag: {flag_str}")
else:
print("No solution found.")
Flag
FLAG{25a34d5dd7bafa245888352b83bf352b}