Le FCSC sans se fatiguer

C'est le printemps, la saison du France Cybersecurity Challenge et donc de mon billet de blog annuel, apparemment. Organisé par l'ANSSI, l'agence de cybersécurité française, le FCSC est l'occasion de sélectionner les membres de l'équipe de France pour l'ECSC, le challenge européen. Le challenge est généreusement aussi ouvert aux vieux comme moi qui ne sont pas éligibles pour raisons d'âge¹.

La diversité et l'originalité des épreuves en font facilement l'un de mes concours préférés. Je m'étais beaucoup amusé avec les épreuves hardware l'année dernière, et cette année j'ai eu à nouveau beaucoup de plaisir dans de multiples catégories d'épreuves, mais surtout en crypto.

Comme c'est de tradition, je prolonge le plaisir en me prêtant au jeu des writeups pour quelques unes des épreuves que j'ai le plus appréciées.

Hardware

Mommy Morse (77 résolutions)

Il est demandé de transmettre un signal en morse, où les points et les traits sont représentés par une « porteuse pure à une fréquence de 5 kHz », et les espacements par une fréquence de 1 kHz. Un signal d'exemple est fourni, et comme j'aime bien visualiser, j'ai fait un graphe:

Comme d'habitude, je trouve que tracer l'argument complexe du signal aide bien, parce que dans ce cas il évolue de manière linéaire (modulo le modulo $2\pi$), avec une pente qui dépend de la fréquence de la porteuse. C'est exactement la manière dont je m'y suis pris pour créer le signal dont j'avais besoin : j'ai créé l'argument qu'il fallait, que j'ai mis dans une exponentielle complexe et c'est passé.

Crypto

Hash-ish (71 résolutions) et Khal Hash (10 résolutions)

Sûrement mes deux épreuves préférées :)

Hash-ish donne un entier H et demande de trouver deux entiers a et b tels que la valeur de hash((a, b)) soit H (hash étant la fonction de hachage par défaut de Python).

Mais comment ça fonctionne, hash, d'abord ? Pour les tuples, son code est là ou bien simplifié² ici en Python (PH1, PH2 et PH5 sont des constantes définies dans le code de CPython, et MOD vaut $2^{64}$) :

def myhash(integer_tuple: Tuple[int, ...]):
    acc = PH5
    for element in integer_tuple:
        acc = (acc + element * PH2) % MOD
        acc = ((acc << 31) | (acc >> 33)) % MOD
        acc = (acc * PH1) % MOD
    acc = (acc + len(t) ^ (PH5 ^ 3527539)) % MOD
    return acc

C'est donc cette fonction qu'il faut inverser (on sait ce qu'elle doit retourner, et on veut savoir quel argument lui donner pour qu'elle fasse ça).

Entre Z3, un « prouveur de théorèmes » développé par Microsoft Research. Plus précisément, c'est un solveur SMT. Sans rentrer dans les détails, un solveur SMT est une généralisation d'un solveur SAT. Alors qu'un solveur SAT détermine la satisfiabilité de formules logiques (avec des portes logiques et des booléens), un solveur SMT détermine la satisfiabilité de formules impliquant des objets plus complexes, comme des nombres ou des structures de données. Ici, c'est exactement ce qu'il faut : on a une formule mathématique à résoudre sur les entiers modulo $2^{64}$.

Z3 possède des variables de type entier, mais vu qu'ici on a des opérations sur des bits, j'ai préféré utiliser les BitVecs, qui sont comme leur nom l'indique des tableaux de bits de taille fixée, et sur lesequels on peut quand même faire des opérations arithmétiques facilement.

def solve(h):
    N = 64
    s = z3.Solver()
    # a and b are the integers that we are looking for
    a = z3.BitVec('a', N)
    b = z3.BitVec('b', N)
    # they need to be less than 2**60, or they don't hash to themselves
    # ULT = Unsigned Less Than: `a < 2**60` doesn't work unless we also add `0 <= a`
    s.add(z3.ULT(a, 2**60))
    s.add(z3.ULT(b, 2**60))
    # hashing the first integer
    acc0 = z3.BitVec('acc0', N)
    s.add(acc0 == PH5 + a * PH2)
    acc1 = z3.BitVec('acc1', N)
    # LShR stands for Logical Shift Right, >> being the arithmetic one
    s.add(acc1 == (acc0 << 31) | z3.LShR(acc0, 33))
    acc2 = z3.BitVec('acc2', N)
    s.add(acc2 == acc1 * PH1)
    # hashing the second integer
    acc3 = z3.BitVec('acc3', N)
    s.add(acc3 == acc2 + b * PH2)
    acc4 = z3.BitVec('acc4', N)
    s.add(acc4 == (acc3 << 31) | z3.LShR(acc3, 33))
    acc5 = z3.BitVec('acc5', N)
    s.add(acc5 == acc4 * PH1)
    # the final hash value should be the one specified
    s.add(h == acc5 + (2 ^ (PH5 ^ 3527539)))
    # calling the solver
    sol = s.check()
    if str(sol) == 'sat':
        # a solution was found: return it
        model = s.model()
        return (model.evaluate(a).as_long(), model.evaluate(b).as_long())

Appelée avec h = 42 (au hasard), la fonction retourne le tuple suivant: (471024597674449489, 129304832457527322). On vérifie :

>>> hash((471024597674449489, 129304832457527322))
42

Ça suffisait pour passer Hash-ish. En revanche, le grand frère Khal Hash est plus coriace. En effet, il demande toujours de trouver un tuple d'entiers dont le hash est une valeur donnée, mais avec la contrainte que les entiers doivent être des caractères ascii (compris entre 0 et 127). Or, deux entiers ne suffisent plus : en effet, le hash étant une valeur de 64 bits, il faut environ le même nombre de paramètres pour avoir une chance, soit environ 9 ou 10 entiers (puisque chacun a 7 bits utilisables et que $64 / 7 \approx 9$). Z3 est malheureusement dépassé par ces contraintes (le problème est beaucoup plus profond : non seulement il y a plus de variables intermédiaires, mais aussi le chemin est plus long entre le hash final et l'entrée à trouver).

J'ai donc écrit une version optimisée de la fonction hash en Rust, qui tourne en une poignée de nanosecondes pour une entrée de 10 entiers. C'est rapide ! Il ne reste plus qu'à essayer des tuples au hasard jusqu'à tomber sur la valeur qu'on voulait. Pas vrai ? Pas vrai ?

On peut essayer d'estimer combien de temps ça peut prendre : la probabilité de tomber sur la valeur qu'on veut en hachant un tuple est environ $2^{-64}$. Donc la probabilité de ne pas tomber dessus est de $1-2^{-64}$. La probabilité de ne jamais être tombé dessus après avoir haché $n$ tuples est donc $(1-2^{-64})^n$. Quelle valeur doit avoir $n$ pour que cette probabilité soit assez basse, disons à $1/2$ ? La réponse est $n \approx 2^{64}$, à peu de choses près. Même avec la fonction optimisée, ça prendrait plus de 2000 ans de hacher ce nombre de tuples³. Le FCSC ne durant que 10 jours, il faut trouver une autre technique.

La clé ici était de se rendre compte que les opérations de la fonction de hash sont toutes inversibles. En effet, reprenons la fonction ligne par ligne:

acc = (acc + element * PH2) % MOD

Pour inverser cette addition, il suffit de retirer element * PH2 modulo MOD à acc.

acc = ((acc << 31) | (acc >> 33)) % MOD

Cette ligne réalise en fait une rotation des bits de acc, de 33 bits vers la droite (ou 31 vers la gauche). Pour l'inverser, il suffit donc de faire la même rotation à l'envers.

acc = (acc * PH1) % MOD

Pour inverser cette multiplication, on multiplie acc par l'inverse modulaire de PH1 modulo MOD. On peut calculer facilement cet inverse en python avec la fonction pow du langage: pow(PH1, -1, MOD).

acc = (acc + len(t) ^ (PH5 ^ 3527539)) % MOD

La dernière ligne est également facile à inverser puisqu'il s'agit encore juste d'une addition.

Tout cela signifie qu'en partant de la valeur finale connue du hash, on peut prendre les éléments du tuple à l'envers et revenir à la valeur initiale de l'accumulateur acc (PH5). Mais chercher dans un sens ou dans l'autre ne change rien en termes de temps de calcul. L'astuce est de chercher par les deux bouts et de faire se retrouver la recherche au milieu.

Imaginons qu'on commence par le faisceau de droite, et qu'on enregistre tous ses points d'arrivée. Maintenant, le faisceau de gauche peut se raccorder non plus juste au point final, mais à chacun des $n$ points du faisceau de droite. On arrive ainsi à $n \approx 2^{32}$ au lieu des $2^{64}$ de la première méthode, pour la même probabilité de succès. C'est un sacré progrès, et ça se calcule à présent en quelques secondes ou minutes au lieu de miliers d'années⁴.

En pratique, j'ai calculé tous les tuples de taille 4 en partant d'un côté, et cherché les tuples de taille 6 en partant de l'autre côté, et je suis tombé sur une solution en une ou deux minutes.

T-Rex (67 résolutions)

Je passe des détails, mais en gros on nous donnait le résultat de $F^{31337}(k)$ où $F$ est l'application $x \mapsto (2x+1)x$ modulo $2^{128}$, et on veut remonter à $k$ qui est la clé de chiffrement du message. Après m'être rendu compte que $F$ était bijective, j'ai passé un bon moment à essayer de l'inverser à la main sans succès, avant de réaliser que je pouvais utiliser là aussi Z3 (31337 fois de suite).

Gaston La Paffe (29 résolutions)

On avait ici un algorithme de signature à base de polynomes, qui fonctionnait de la manière suivante (là aussi, j'omets des détails) :

• s1 et s2 des polynomes choisis au hasard, constituent la clé privée ;
• On nous donne a et t, polynomes tels que t = a*s1 + s2 ;
• Pour signer un message m, y1 et y2 sont d'abord générés aléatoirement. Puis on calcule c = H(a*y1 + y2, m) où H est une fonction à sens unique. Enfin, on retourne z1 = s1*c + y1 et z2 = s2*c + y2, ainsi que y1 « par erreur ».

Quelques calculs permettent de se rendre compte que connaître y1 permet de trouver aussi y2:

y2 = a*(z1 - y1) + z2 - t*c

et qu'à partir de là, on a les équations

s1 * c = z1 - y1
s2 * c = z2 - y2

dans lesquelles on connaît toutes les variables à part les secrets s1 et s2.

Pour trouver les coefficients des secrets, j'ai choisi d'utiliser ortools, une suite de solveurs développée par Google. Z3 aurait peut-être pu aussi fonctionner, mais il s'agissait ici en fait d'un problème de programmation linéaire sur les entiers, ce sur quoi ortools est plus efficace.

Side Channels and Fault Attacks

Never Skip Class Nor Multiplication (85 résolutions)

On avait accès à un oracle RSA chiffrant des messages choisis, à l'aide d'une fonction d'exponentiation modulaire « buguée » de manière à ce qu'on puisse choisir quelle multiplication elle allait sauter. L'objectif était de déterminer la clé privée $d$ (l'exposant de l'opération $c = m^d \mod n$).

La question à se poser est la suivante : Si je saute la multiplication du bit $k$ de la clé $d$, quel est l'exposant $d'$ qui a alors été utilisé ?

    Exposant d initial                       Exposant d' réel
N-1          K            0    skip K    N-1          K            0
[    dH    ] 0 [    dL    ]    ----->    [    dH    ] 0 [    dL    ]

N-1          K            0    skip K    N-1          K            0
[    dH    ] 1 [    dL    ]    ----->    [    dH    ] 0 [    dL    ]

On remarque facilement que sauter un bit nul ne modifie pas l'exposant, alors que sauter un bit non-nul le change. Il suffit alors de demander à chiffrer le même message en sautant tous les bits un par un, et de comparer ces résultats à la situation où on ne saute aucun bit. On a alors une correspondance directe entre les résultats et la clé.

Never Skip Class Nor Squaring (70 résolutions)

Même principe, mais la fonction est buguée de manière à sauter l'étape de mise au carré. La question est la même : si on saute le bit $K$ de l'exposant $d$, quel exposant $d'$ a-t-on alors vraiment utilisé ?

    Exposant d initial                       Exposant d' réel
N-1          K            0    skip K    N-2        K            0
[    dH    ] 0 [    dL    ]    ----->    [    dH    ] [    dL    ]

N-1          K            0    skip K    N-2        K            0
[    dH    ] 1 [    dL    ]    ----->    [  dH + 1  ] [    dL    ]

Grâce à quelques dessins dans ce genre, on se rend compte que peu importe la valeur du bit $K$, on a toujours $d - d' = d_H \cdot 2^K$. Cette observation permet de déterminer $d$ bit par bit. En effet, si on appelle $c$ la vraie valeur de $m^d \mod n$, en sautant le bit $N-2$ on obtient pour $m^{d'}$ deux valeurs possibles selon que le bit $N-1$ est nul ou non : soit $c$ (s'il est nul), soit $c\cdot m^{-2^{N-2}}$ (s'il ne l'est pas). Armé de cette information, on saute alors le bit $N-3$ pour déterminer la valeur du bit $N-2$, etc.

Misc

Guess Me Too (68 résolutions)

Un nombre de 128 bits est tiré au hasard et il faut le deviner. On ne peut poser que 136 questions de la forme « Parmi les bits numéros $x_0$, $x_1$, $x_2$, etc. du nombre secret, quelle est la parité du nombre de bits non nuls ? » (en choisissant les $x_i$). De plus, on sait qu'une des réponses sera fausse mais on ne sait pas laquelle.

Il semble logique de commencer par demander les 128 bits un à un. On a déjà presque 6% de chance d'avoir deviné le nombre (si la réponse incorrecte tombe dans les 8 autres questions), donc on pourrait déjà s'arrêter là et faire plusieurs tentatives jusqu'à ce que ça marche (17 fois en moyenne).

Pour deviner le nombre à coup sûr, il faut faire de la correction d'erreur.

On commence par demander la parité de la somme de tous les bits, et on compare avec le résultat des 128 premières questions. Si les résultats concordent, on sait qu'on n'est pas encore tombé sur la réponse incorrecte. Sinon, c'est qu'il y a une erreur soit dans les questions individuelles, soit dans la question de contrôle. Pour la déterminer, on demande alors la parité de la somme de tous les bits impairs, que l'on compare à nouveau au résultat des questions individuelles. On sait que le résultat de cette question sera correct, puisqu'on a déjà détecté une erreur et qu'il ne peut y en avoir qu'une seule. Si les résultats concordent, on sait que l'erreur est dans les bits pairs, sinon c'est qu'elle est dans les bits impairs. On peut alors continuer à préciser la position de l'erreur en demandant la parité de la somme des bits impairs des bits suspects d'être erronés, jusqu'à ce qu'il n'y ait plus qu'une seule possibilité.

En pratique, toutes les questions doivent être posées en même temps au début. Qu'à cela ne tienne, les huit questions supplémentaires à poser qui fonctionnent dans tous les cas sont les suivantes :

11111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111
10101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010
11001100110011001100110011001100110011001100110011001100110011001100110011001100110011001100110011001100110011001100110011001100
11110000111100001111000011110000111100001111000011110000111100001111000011110000111100001111000011110000111100001111000011110000
11111111000000001111111100000000111111110000000011111111000000001111111100000000111111110000000011111111000000001111111100000000
11111111111111110000000000000000111111111111111100000000000000001111111111111111000000000000000011111111111111110000000000000000
11111111111111111111111111111111000000000000000000000000000000001111111111111111111111111111111100000000000000000000000000000000
11111111111111111111111111111111111111111111111111111111111111110000000000000000000000000000000000000000000000000000000000000000

Si on regarde par exemple la ligne 11001100..., elle contient bien tous les bits impairs des bits impairs, ainsi que tous les bits impairs des bits pairs, et ainsi de suite.

Coda

Z3 et ortools se sont avérés être un arsenal efficace cette année, me permettant de résoudre 5 challenges (dont 4 de crypto) sans trop d'effort. Ils rendent aussi service en dehors du FCSC : ce sont des outils à connaître.

---