ZZZ

Catégorie: Reverse Difficulté: - Flag: CTFREI{1_h0p3_u_us3d_Z3_lol}

Challenge

808B

zzz.zip

archive

Description

---

Sauras-tu trouver le bon flag à rentrer ?

Le flag est sous le format : CTFREI{flag_trouvé}

Solution

z3 solver est un outil pour résoudre des contraintes logiques et arithmétiques. Ici, j'utilise une librairie différente nommée pyton-constraint permettant également de résoudre des CSP (Constraint Satisfaction Problems). Elle est sans doute beaucoup moins performante, mais plus facile à appréhender.

On commence par créer un problème, on définit ensuite les variables que l'on va utiliser (je les ai nommées comme dans zzz.py a[0], a[1], etc. pour simplifier le parsing). Et enfin, on ajoute les contraintes. La librairie va ensuite optimiser les relations pour trouver une solution.

from constraint import Problem
import string
import re

# Création du problème à résoudre par contraintes
problem = Problem()

# Ajout des variables utilisées, on les nomme quand dans zzz.py
problem.addVariables([f'a[{i}]' for i in range(20)], [ord(c) for c in string.printable])

# Parsing du fichier zzz.py pour récupérer les conditions
with open('zzz.py', 'r') as f:
  zzz = f.read().splitlines()
  if_lines = zzz[4:47:2]    # Les conditions sont toutes les 2 lignes à partir de la n°5

for line in if_lines:
  # On skip les conditions sum() car inutiles et complique le parsing
  if 'sum' in line:
    continue
  
  line = line.strip()[3:-1]               # Retire le "if " au début de la ligne et ":" à la fin
  calcul, result = line.split(' != ')     # Sépare le calcul du résultat attendu
  
  variables_used = list(set(re.findall('(a\[\d+\])', calcul)))   # Récupère les variables utilisées dans le calcul
  replace_variables_by = [(variables_used[i], 'abcdefg'[i]) for i in range(len(variables_used))] # Map chaque variable à une nouvelle lettre
  for variable, new in replace_variables_by:
    calcul = calcul.replace(variable, new)  # Remplace dans le calcul les variables par leur nouvelle lettre
  
  parameters = ', '.join([new for _, new in replace_variables_by])  # Les paramètres de la fonction lambda sont l'ensemble des lettres utilisées dans le calcul
  constraint = f'lambda {parameters}: {calcul} == {result}'
  variables = tuple([variable for variable, _ in replace_variables_by])
  eval(f'problem.addConstraint({constraint}, {variables})')  # On ajoute la contrainte qu'on vient de créer

# Calcul d'une solution (y en a qu'une seule de toutes façons)
solution = problem.getSolution()
# Les valeurs des variables sont l'ascii des caractères du flag
flag = ''.join([chr(solution[f'a[{i}]']) for i in range(20)])
print(f'CTFREI{{{flag}}}')
# CTFREI{1_h0p3_u_us3d_Z3_lol}