Ce billet constitue le troisième d'une série portant sur l'analyse a postériori de l'étape 2 du challenge SSTIC 2013. Si vous n'avez pas lu le premier de cette série et que vous souhaitez suivre mes diverses expériences correctement je vous conseille vivement de commencer par lui; et si, au contraire, vous voulez simplement connaitre le fin mot de l'histoire je vous recommande de sauter au dernier billet de la série :)

Boostons l'analyse fréquentielle

En terminant le billet précédent par la comparaison de fréquences entre l'un des buckets chiffrés et un lorem ipsum encodé en base64 j'avais conclu que le clair original, bien que probablement ascii, n'était pas de l'anglais (ni probablement du français ou un autre dérivé de langue latine d'ailleurs). Pour autant, l'analyse fréquentielle est-elle totalement hors course ? Peut-être pas ! En effet, je sais que le clair original n'était pas similaire à du lorem ipsum, mais peut-être est il similaire à du code en C, ou à du HTML, ou à un autre truc potentiellement aussi exotique que du brainfuck. Pour identifier ça j'ai eu une idée toute bête : trouver pleins de textes variés et comparer leur analyse fréquentielle à celle de data. En pratique ça a donné un petit script python qui dumpait en boucle les dernier pastie de pastebin, les encodait en base64 et faisait l'analyse fréquentiel du blob base64 ainsi obtenu. Au bout d'environ 12h je me suis retrouvé avec 9322 textes différents et j'ai élu comme mon "champion" celui qui donnait l'erreur quadratique la plus faible quand il était comparé à data.

Pour les curieux voici à quoi il ressemble (il a déjà été supprimé de pastebin, il serait donc inutile de vous mettre le lien) :

RemoveBuildingForPlayer(playerid, 4024, 1479.8672, -1790.3984, 56.0234, 0.25);
RemoveBuildingForPlayer(playerid, 4044, 1481.1875, -1785.0703, 22.3828, 0.25);
RemoveBuildingForPlayer(playerid, 4045, 1479.3359, -1802.2891, 12.5469, 0.25);
RemoveBuildingForPlayer(playerid, 4046, 1479.5234, -1852.6406, 24.5156, 0.25);
RemoveBuildingForPlayer(playerid, 4047, 1531.6328, -1852.6406, 24.5156, 0.25);
...
CreateObject(1231, 1399.14575, -1845.25000, 15.20500,   356.85840, 0.00000, 3.14160);
CreateObject(1231, 1399.15137, -1838.06458, 15.20500,   356.85840, 0.00000, 3.14160);
CreateObject(1231, 1478.45117, -1862.11169, 15.20500,   356.85840, 0.00000, 3.14160);
CreateObject(1231, 1486.32324, -1862.03967, 15.20500,   356.85840, 0.00000, 3.14160);

Etant donné que nous sommes à posteriori et que nous "trichons" donc j'ai tracé l'analyse fréquentielle des buckets de mon "champion" et je l'ai comparé avec celle de la solution. Force est de constater que, contre toute attente, on trouve des éléments assez proche de la solution ! Les octets significatifs (i.e. apparaissant souvent) sont assez cohérents entre la solution du challenge et mon "champion" (bien qu'il y ait tout de même des différences). Les octets apparaissant peu sont, eux, complètement mélangés (mais ça, on pouvait s'y attendre). L'analyse complète prend plusieurs pages, mais voici un extrait de l'analyse du bucket 15 pour vous donner une idée de ce à quoi ça ressemble :

+++ data - bucket 15 +++
t [0xb] (0.04)  
L [0x17] (0.04) 
e [0x83] (0.04) 
o [0xd3] (0.04) 
K [0xf7] (0.04) 
...
z [0x7b] (3.67) =======================
j [0x73] (4.58) =============================
Z [0x7f] (4.76) ==============================
Y [0xbf] (5.01) ================================
T [0xf] (5.23)  =================================
D [0x7] (5.74)  ====================================
N [0x57] (6.76)===========================================
M [0x97] (9.37)============================================================

== Champion.txt - bucket 15 ===
q [0x71] (0.05) 
e [0x65] (0.10) 
n [0x6e] (0.15) =
7 [0x37] (0.20) =
B [0x42] (0.20) =
...
j [0x6a] (3.64) ===========================
N [0x4e] (3.89) =============================
L [0x4c] (4.53) ==================================
C [0x43] (5.37) ========================================
D [0x44] (5.47)=========================================
A [0x41] (6.79) ===================================================
M [0x4d] (7.53)=========================================================
w [0x77] (7.88)============================================================

Il y a donc des similitudes assez flagrandes, mais pas assez pour que je puisse résoudre le challenge en identifiants uniquement les chiffrés à des clairs en fonction de leur similitude de fréquence avec mon champion. L'attaque fréquentielle se rapproche donc de la solution, mais n'y arrive pas tout à fait...

La génétique à la rescousse

Je me retrouve donc à ce point avec une approche en force brute trop longue, et une approche en analyse fréquentielle trop approximative. J'ai alors eu l'idée de tenter une méthode d'optimisation numérique issue du champs d'étude de l'intelligence artificielle : un algorithme génétique :)

Je ne vais pas rentrer dans les détails mais l'idée centrale c'est de simuler les phénomènes d'évolution naturelles des organismes sexués. Dans mon cas :

• un individu était caractérisé par l'ensemble des relations chiffré=>clair
• les mutations consistaient à changer le clair associé à un chiffré en le remplaçant par un autre chiffré possible pour ce clair
• les croisements consistaient à prendre la moitié des association en provenance d'un parent et l'autre moitié de l'autre (sans déc ;) !)
• la fonction de notation consistait à compter le nombre de caractères ascii "improbable" obtenus dans le clair décodé. Les caractères ascii "improbables" étant, en gros, l'ensemble des caractères de controles (tabulation VERTICALE, bip, etc.)

Le programme a tourné une petite après-midi, mais sans grand succès. La convergence ne semblait pas vraiment au rendez-vous et, surtout, je me suis rappelé d'une bonne résolution qui m'a semblé plus prometteuse, donc j'ai abandonné l'approche génétique.

Une bonne résolution refait surface

Ma bonne résolution c'était d'utiliser un solver SAT la prochaine fois que je n'aurai pas de meilleure idée qu'une approche en force brute ! En plus, je savais que ce type d'approche pouvait donner de bon résultats dans l'attaque de chiffrements faibles, donc je me suis dit qu'il fallait absolument que je tente le coup !

La traduction de mon problème au format SAT a d'ailleurs été plus facile que ce à quoi je m'attendais. En effet, ce que je cherche à trouver c'est : pour chaque valeurs d'octets chiffrés de chacun de mes 16 buckets je veux retrouver la valeurs des 6 bits qu'encode le caractère base64 clair correspondant. J'ai donc créé un petit dictionnaire python qui m'a permi de faire rapidement les conversiont entre "bucket, valeur d'octet, bit" et "numéro de variable booléenne pour le solveur SAT" :

runner = 0
for bucket_id in range(16):
    for octet in range(255):
        for bit in range(8):
            correspondance['%d_%d_%d'] = runner
            runner+=1

Je me retrouve donc avec un peu plus de 5000 variables utiles (chaque bucket ne contient qu'environ 54 valeurs d'octets chiffrés différents; donc avec mon range(255) j'en fais plus que nécessaire). Maintenant il va falloir écrire les règles à respecter... La première est évidente : je vais exprimer la contrainte des bits nuls causées par la nature ascii du texte clair original (cf billet précédent). Au format dimacs ça s'exprime très simplement -XXX 0 (où XXX est le numéro de la variable booléenne correspondant au bit forcé à nul).

Je lance minisat sur ce problème et il me trouve une solution en un rien de temps :) ! Malheureusement ce n'est, évidemment, pas la bonne solution :-/ Le texte obtenu contient, après décodage base64, beaucoup de caractères non-imprimables dont je parlais dans mon approche génétique. Qu'à cela ne tienne, l'approche SAT permet de rajouter allègrement des contraintes, en effet je voudrai exprimer que chaque octet décodé n'a pas le droit d'être l'un des caractères non-imprimables. En pseudo-logique ça va donner quelque chose comme ça : "(octetX n'a pas la valeur ascii du charactère de controle 1) et (octetX n'a pas la valeur ascii du charactère de controle 2) et (octetX n'a pas la valeur ascii du charactère de controle 3) ..." donc je n'ai qu'à réussir à traduire un "octetX n'a pas la valeur ascii BBBBBBBB" sous la forme d'une suite de "ou" logiques et ça ira bien. Ca tombe bien, la loi de de morgan me dit que : "non (bit1=1 et bit2=0 et bit3=1, ...)" est identique à "bit1=0 ou bit2=1 ou bit3=0...".

Bref : interdire à un octet de prendre une valeur donnée est trivial en dimacs. Aussitôt dit aussitôt fait, j'interdit l'apparition de caractères non imprimables et je relance minisat. En un clin d'oeil j'ai une solution...qui n'est toujours pas la bonne -_-

Je commence à être ennuyé mais je me dit que je vais profiter de la facilité qu'il y a à interdire que certains octets prennent certaines valeurs en clair pour m'aiguiller dans la bonne direction. Je ressort donc mon "champion" de l'analyse fréquentielle, dont je parle en début de billet, et j'interdit à chacun de mes octets apparaissant significativement dans data d'être traduit en clair par l'un des octets apparaissant moins de 1% du temps dans mon champion. Je relance minisat et j'obtient une nouvelle solution....toujours pas bonne -_-

L'anneau unique

C'est là que je réalise que j'ai oublié une contrainte essentielle : l'algorithme de chiffrement peut être vu comme 16 bijections indépendantes, or moi je n'ai imposé nulle part qu'un clair ne pouvait correspondre qu'à une seule valeur chiffrée. Pour preuve j'en veux la solution que minisat me donne quand je lui donne peu de contraintes : AAAAAAAAA....AAA Il faut donc que je trouve un moyen d'exprimer, en dimacs, le fait que chaque octets clair ne peut pas apparaitre plus d'une fois dans chaque bucket. Pas simple à réaliser à partir de simples ET et OU... Après réflexion je me suis dit qu'il me suffirait de dire que, pour chaque bucket, le XOR de chaque octets clair est non-null avec n'importe quelle autre octet clair du même bucket. La solution est dans l'esprit et fonctionne : ce sont des simples propositions logiques, et elles imposent qu'aucun clair n'apparaisse plus d'une fois dans chaque bucket. Sauf que voilà, bien que certains solveurs permettent d'utiliser des XOR sur des vecteurs de bits, la syntaxe dimacs "pure" ne permet d'utiliser que des OR et des AND sur de simples bits... Enfer et damnation, ne parviendrais-je pas à exprimer cette contrainte pourtant simple et essentielle ???

Et bien si ;) ! Il se trouve qu'on peut exprimer des XOR sur des vecteurs de bits avec de simples OR et AND sur des bits. L'explication est un peu longue donc je vous invite à aller la lire directement sur cette page web, là où je l'ai trouvé. On y apprend par contre un énorme inconvénient des XOR : un simple XOR entre deux vecteurs de X bits implique 2 puissance (X-1) clauses dimacs ! Un XOR entre deux octets implique donc 128 clauses dimacs différentes...Heureusement je travaille en base64 et je n'ai donc à faire des XOR qu'entre des vecteurs de 6 bits, ce qui n'induit que 32 clauses à chaque fois et qui reste donc gérable. Arrivé là je me suis même demandé si ça n'avais pas été fait exprès par les concepteurs du challenge¹... Quoiqu'il en soit j'exprime mes (environ) 555516 xor qui se traduisent en (environ) 1,5 millions d'expressions dimacs. Je donne mon nouveau fichier à manger à minisat et....j'attend.

Au bout d'une heure et demi de calcul minisat ne s'en sortait toujours pas. J'ai donc téléchargé, compilé, et testé cryptominisat. Pas de chance : au bout d'une heure cryptominisat n'avait toujours pas terminé lui non plus. J'ai donc cherché ailleurs et j'ai testé lingeling et, miracle, il m'a trouvé la solution en à peine une minute :-D !...Enfin...il m'a trouvé une solution, mais ça n'était toujours pas celle du challenge. Visiblement, je manquais de contraintes...

Markov à la rescousse

J'ai continué de jouer un petit peu avec lingeling en lui fournissant des dimacs un peu différents, basés sur diverses contraintes issues de l'analyse fréquentielle de mon champion (exemple : tous les octets chiffré apparaissant plus de 1% du temps dans data doivent forcément avoir leur clair présent dans le champion, etc.), mais sans succès. En effet, chaque nouvelle solution trouvée par lingelin n'était "visiblement" pas la bonne. Et c'est en réalisant ce que je venait de me dire que j'ai eu une idée : l'analyse fréquentielle du champion ne sera pas suffisante, il faut aussi que j'interdise les traductions "visiblement" improbables. En termes de techniques je me suis donc dit : j'identifie les suites de trois caractères les plus improbables (selon une mesure de markov) et je les interdit également ! Dans les faits j'ai plutôt implémenté un "pseudo-markov" capable de s'en sortir avec un échantillon de base aussi petit que mon texte "champion", mais l'idée reste la même et j'ai introduit des interdictions de plus dans mon dimacs : interdiction aux triplettes étrange ^^ !...Sauf qu'au bout d'une heure de calcul mon PC était encore en train de générer les règles d'interdiction :-/ Il y avait trop de triplettes improbables à interdire. J'ai donc opté pour un compromis en n'interdisant que certaines triplettes pour ne pas dépasser les 3 millions de règles dimacs et j'ai lancé lingeling. Quelques minutes de calcul ont suffit pour obtenir une solution...qui n'était toujours pas la bonne :-(

Destination finale ?

Bien...je commence à me dire que je suis dans une impasse et les tests prennent de plus en plus de temps (la moindre résolution demandée à lingeling prend environ 5mn, or avec la météo qu'on a en ce moment² 5mn avec le processeur qui chauffe à fond c'est presque une nouvelle forme de torture). Du coup j'ai décidé d'adopter une nouvelle approche : l'approche des autres (dont je vous parlerai dans le prochain billet).

1. D'ailleurs si l'un d'entre eux voit ce blog je veux bien une réponse en commentaire et/ou par mail :) ↩
2. Je rédige cette ligne fin juillet 2013 ↩