z3 solver est un outil pour résoudre des contraintes logiques et arithmétiques. Ici, j'utilise une librairie différente nommée permettant également de résoudre des CSP (). 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}
