samedi, août 11 2012

SAT solvers

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 :)

Puzzle - Creative Common from a work by "INTVGene" on Flickr
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[1]. 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[2] 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[3] 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[4] :

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[5]

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 ;) ?

Notes

[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.

samedi, octobre 22 2011

Brèves du jour

Un mini billet pour deux petites brèves : une astuce python (déjà bien connue, mais plus on réplique ce genre d'info moins on a de mal à la retrouver quand on l'a oublié), et un pointeur sur un jouet sympa.

Tools - Creative Common by mtneer_man on Flickr
Tout d'abord l'astuce python : comment changer son user-agent quand on utilise la librairie urllib. C'est un problème ultra-classique puisque pas mal de sites font du filtrage sur ce user-agent et refusent de répondre quand ils repèrent un script python[1]. En fouillant sur le net on trouve pleins de méthodes plus ou moins bidons (certaines se contentent carrément de rajouter un second header "user-agent", ce qui n'est évidemment pas ce que l'on cherche à faire), et après en avoir testé au moins une demi-douzaine voici celle que j'utilise à présent (et qui marche :D) :

import urllib
# ============ USER AGENT MAGIC ===========
class UAOpener(urllib.FancyURLopener):
        version = 'Mozilla/5.0 (Windows; U; Windows NT 5.1; it; rv:1.8.1.11) Gecko/20071127 Firefox/2.0.0.11'
urllib._urlopener = UAOpener()
# =========================================

Et voilà :) Comme pour le passage via TOR c'est tout ce qu'il y a à faire. Accessoirement j'ai réalisé récemment que le dernier paramètre de "setdefaultproxy" que j'utilise pour passer par TOR souffre un bug ennuyeux : il est ignoré :-D Donc que vous mettiez à "True" ou à "False" les résolutions DNS ne passeront JAMAIS par votre proxy socks (et donc par TOR)...ennuyeux n'est-ce-pas ? En tout cas maintenant vous êtes prévenus :)

Le petit jouet maintenant : ça n'a rien de nouveau non plus, mais c'est tout de même un jouet rigolo. Il s'agit du WOrdnet Libre du Français[2]. Pour ceux qui connaissent Wordnet : c'est Wordnet pour le Français ;) Pour ceux qui ignorent ce qu'est Wordnet c'est une base de donnée concernant le sens des mots et leurs relations les uns avec les autres. Un usage immédiat de Wordnet c'est de trouver des synonymes (dans la langue française avec WOLF, dans la langue anglaise avec le Wordnet original), un autre usage consiste à mesurer la proximité de sens entre deux mots par exemple. Les possibilités sont vraiment nombreuses, notamment en data-mining. Bref vous pouvez le télécharger ici au format XML, et ces trois mini remarques pourraient vous êtes utiles si vous voulez travailler avec :

  • Le document ne contient pas de balise racine, ajoutez donc en une si vous voulez que xmllint --format ou xml.dom.minidom.Parse ne vous insulte pas. Par exemple un petit <wolf> en début de document et un petit </wolf> en fin de document feront parfaitement l'affaire.
  • Les '&' ont tendance à faire crier le module python xml.dom.minidom. Pour ma part je les ai donc purement et simplement supprimés grâce à un petit sed.
  • Le XML pèse 38Mo sur disque, une fois parsé par xml.dom.minidom mon interpréteur Python prend plus de 1Go ;-) Veillez donc à avoir de la RAM disponible.

Notes

[1] Par exemple wikipedia.

[2] WOLF