Ce mois-ci je suis tombé, en moins de 24h, sur deux articles traitant de l'utilisation des SAT solvers dans un contexte de sécurité informatique. La (re)découverte de ces outils dans ce domaine m'a donné envie de partager l'expérience et je fais donc, via ce petit billet, un peu plus de "bruit google" autour des SAT solvers en espérant qu'ainsi quelqu'un d'autre passe un bon moment à (re)découvrir les possibilités de ces outils :)

Un "problème SAT" c'est un problème de décision visant à savoir s'il existe une solution à une série d'équations logiques données¹. Résoudre un problème SAT revient donc à décider s'il existe, ou non, une configuration d'affectation "VRAI/FAUX" à des variables d'entrées qui permette de satisfaire une expression logique du type : "(condition1 OU condition2 OU ... OU conditionX) ET (conditionY OU...OU condition Y++) ET ... ET (...)". Par exemple si on considère deux variables de bool "A" et "B" on peut évaluer le problème SAT suivant "(A) ET (nonA)" qui n'a, évidemment, pas de solution et qui est donc "UNSATIFIABLE"; en revanche le problème SAT "(A ou B) ET (nonA ou B)" est SATISFIABLE avec, par exemple, les affectations : B=VRAI, A=VRAI. Un solveur SAT est un programme informatique dont la tache est de décider automatiquement si un problème SAT et UNSATISFIABLE ou SATISFIABLE (et de donner une solution exemple dans ce dernier cas de figure).

On trouve aujourd'hui beaucoup de logiciels de résolution SAT plutôt très efficace² et on peut donc considérer que la technologie est assez mature pour jouer avec sans avoir à ramer dès l'installation ;) Par exemple "Minisat" est packagé dans toutes les bonne distributions Linux³ et vous n'aurez donc aucun souci à vous en procurer une version en état de marche.

Une fois un solveur SAT fonctionnel installé il faut apprendre quelques rudiments du langage "DIMACS". C'est un formalisme qui est utilisé pour représenter les problèmes SAT de façon compréhensible par 99% des solveurs publiques et qui, coup de chance, est basé sur du texte brute et reste super simple à apprendre :

• Toute ligne commençant par un "c" sera considérée comme du commentaire
• En début de fichier on doit renseigner le nombre de clauses (i.e. nombre de : "condition1 OU condition2 OU ...OU ... conditionX" ) ainsi que le nombre de variables que l'on va utiliser. Pour celà on écrit une ligne commençant par "p cnf" puis contenant les informations demandées. Au final la ligne ressemble à ça : "p cnf NOMBRE_DE_CLAUSE NOMBRE_DE_VARIABLES"
• Ensuite on écrit, sur chaque ligne, une clause du problème dans laquelle on remplace : les variables par un numéro d'indice l'identifiant uniquement, les mots "OU" par des espaces, et les les "non" par des moins. On termine chaque ligne de clause par un "0" Ainsi notre problème SAT d'exemple UNSATISFIABLE ((A) ET (nonA)) devient⁴ :

p cnf 1 2
1 0
-1 0

De même notre second problème SAT d'exemple ((A OU B) ET (nonA OU B)) devient :

p cnf 2 2
1 2 0
-1 2 0

Quand on donne à manger le premier fichier texte à minisat on obtient bien UNSATISFIABLE, et quand on lui donne à manger le second on obtient SATISFIABLE sur la sortie standard et la solution exemple -1 2 0 dans le fichier de résultat⁵

Bon c'est bien joli, mais on ne va pas très loin avec ça me direz-vous ! Et bien si, justement :) ! Là où ça devient intéressant c'est qu'on peut faire beaucoup plus que mes mini problèmes d'exemple. Parmi les fichiers cnf mis à dispositions ici on en trouve un qui compte 1040 variables et 3668 clauses que Minisat résoud (comme "UNSATISFIABLE") en...0m0.013s ! Dans la même catégorie on trouve un autre fichier de test contenant 1501 variables et 3575 clauses que Minisat résoud (en "SATISFIABLE" avec une solution exemple) en 0m0.008s.

Avec une telle puissance de résolution que peut-on faire ? On peut, par exemple, attaquer des algorithmes de hachage faibles, comme l'indique l'un des deux articles déclencheur de ce billet. On peut également aller beaucoup plus loin et se mettre à taquiner la recherche de vulnérabilité ou la génération de code d'exploitation comme le montre le second lien initiateur de ce billet. De plus, j'ai en mémoire d'avoir vu quelque part des outils de fuzzing qui utilisaient des SAT solver pour augmenter leur couverture de test, mais je ne parviens plus à retrouver de liens pertinents :( ...Enfin, pour ma part, je vais probablement tenter d'insérer une intervention de SAT solver dans mon analyseur de code PHP afin de décider plus précisément si un bout de code est accessible ou pas; ou encore tenter de transcrire au formalisme SAT le prochain problème que je rencontrerai et pour lequel je n'aurai pas de meilleure idée qu'un brute-forceur :)

Et vous, qu'en ferez-vous ;) ?

1. Merci Wikipédia ↩
2. En tout cas beaucoup plus efficace qu'un être humain devant réaliser la même tâche ↩
3. Minisat est masqué sous gentoo par ~x86, mais il est tout de même packagé ↩
4. Vous devinerez que j'ai affecté 1 à la variable A, et 2 à la variable B ↩
5. On remarque au passage que Minisat nous propose la solution A=Faux, B=Vrai alors qu'en exemple moi j'avais donné A=Vrai, B=Vrai. Les deux solutions sont valides pour ce problème. ↩