Un classique des compétitions de sécurité: on vous donne un algorithme de hashage (de manière plus ou moins directe), une valeur hachée, et il faut trouver le mot de passe qui a mené à cette valeur hachée.
On va voir dans ce post comment résoudre ce type de problèmes avec z3, un solveur SMT (Satisfiability Modulo Theories) dont j’ai déjà parlé. En gros on lui donne des contraintes, et il trouve un ensemble de valeurs qui satisfait ces contraintes.
Pour l’algo de hashage à casser, j’ai porté en Python l’exercice de cette fin de vidéo :
# Example adapted from:
# https://youtu.be/0DJZ2Bt5eyE?t=2022
def hash(s:str) -> int:
n = 7
for c in s:
n = n*31+ord(c)
return n%(2**32)
def check_hash(s:str) -> bool:
TARGET_HASH=593779930
return hash(s) == TARGET_HASH
if __name__=="__main__":
import sys
print(sys.argv[1])
print(check_hash(sys.ARGV[1]))
On est donc face à un bout de code qui hashe un mot de passe, et renvoie un entier.
On a besoin de la librairie python z3:
pip install z3-solver
Ensuite, on va bruteforcer la longueur, créer un solveur pour chaque longueur, et tenter de trouver une solution. Une fois qu’on en a trouvée une (solver.check() == sat), on reconstruit le mot de passe.
from z3 import *
TARGET_HASH=593779930
def hash(s) -> int:
n = 7
for c in s:
n = n*31+c
return n%(2**32)
def break_at_length(target_length: int) -> Solver:
"""Coeur de la résolution:
on crée un solveur, on ajoute nos contraintes:
- une longueur fixée
- des lettres entre a et z
- le hash de cette entrée doit valoir le hash cible
"""
s = Solver()
# Le mot de passe
chars = [Int(f"c_{i}") for i in range(target_length)]
# Chaque élément du mot de passe doit être une lettre en minuscule
for c in chars:
s.add(And(c >= ord('a'), c <= ord('z')))
# On veut que le hash obtenu avec ce mot de passe soit celui de la cible
s.add(hash(chars)==TARGET_HASH)
return s, chars
if __name__ == "__main__":
# comme on ne connait pas la longueur du mode de passe,
# une option c’est de bruteforcer: tant qu’on a pas trouvé
# une solution valide, on teste une longueur plus grande
length = 1
while True:
s, chars = break_at_length(length)
if s.check() != sat:
print(f"Nothing found at length {length}")
length+=1
else:
break
m = s.model()
print(f"password length: {length}")
# On transforme notre modèle z3 en une string
print("".join([chr(m[c].as_long()) for c in chars]))
On teste:
$ python solve-cyberseed.py
Nothing found at length 1
Nothing found at length 2
Nothing found at length 3
Nothing found at length 4
Nothing found at length 5
password length: 6
dragon
On a trouvé le mot de passe (dragon), trop cool !