Presque chaque fois que vous ouvrez un navigateur Google Chrome sécurisé, un nouveau système cryptographique développé par le MIT aide à mieux protéger vos données.

Dans un article présenté au récent Symposium de l'IEEE sur la sécurité et la confidentialité, Les chercheurs du MIT détaillent un système qui, pour la première fois, génère automatiquement un code de cryptographie optimisé qui est généralement écrit à la main. Déployé début 2018, le système est maintenant largement utilisé par Google et d'autres entreprises technologiques.

L'article montre maintenant à d'autres chercheurs dans le domaine comment des méthodes automatisées peuvent être mises en œuvre pour éviter les erreurs humaines lors de la génération de cryptocode, et comment les ajustements clés des composants du système peuvent aider à obtenir des performances plus élevées.

Pour sécuriser les communications en ligne, les protocoles cryptographiques exécutent des algorithmes mathématiques complexes qui effectuent des opérations arithmétiques complexes sur de grands nombres. Dans les coulisses, cependant, un petit groupe d'experts écrivent et réécrivent ces algorithmes à la main. Pour chaque algorithme, ils doivent peser diverses techniques mathématiques et architectures de puces pour optimiser les performances. Lorsque les mathématiques ou l'architecture sous-jacentes changent, ils recommencent essentiellement à partir de zéro. En plus d'être laborieux, ce processus manuel peut produire des algorithmes non optimaux et introduit souvent des bogues qui sont ensuite détectés et corrigés.

Des chercheurs du Laboratoire d'informatique et d'intelligence artificielle (CSAIL) ont plutôt conçu "Fiat Cryptography, " un système qui génère automatiquement et vérifie simultanément des algorithmes cryptographiques optimisés pour toutes les plates-formes matérielles. Dans les tests, les chercheurs ont découvert que leur système peut générer des algorithmes qui correspondent aux performances du meilleur code manuscrit, mais beaucoup plus rapide.

Le code généré automatiquement par les chercheurs a rempli BoringSSL de Google, une bibliothèque cryptographique open source. Google Chrome, Applications Android, et d'autres programmes utilisent BoringSSL pour générer les différentes clés et certificats utilisés pour crypter et décrypter les données. Selon les chercheurs, environ 90 % des communications Chrome sécurisées exécutent actuellement leur code.

"La cryptographie est implémentée en faisant de l'arithmétique sur de grands nombres. [Fiat Cryptography] rend plus simple la mise en œuvre des algorithmes mathématiques … parce que nous automatisons la construction du code et fournissons des preuves que le code est correct, " déclare Adam Chlipala, co-auteur de l'article, chercheur au CSAIL et professeur agrégé en génie électrique et informatique et responsable du groupe Langages de programmation et vérification. "C'est essentiellement comme prendre un processus qui s'est déroulé dans le cerveau humain et le comprendre suffisamment bien pour écrire un code qui imite ce processus."

Jonathan Protzenko de Microsoft Research, un expert en cryptographie qui n'a pas été impliqué dans cette recherche, voit le travail comme représentant un changement dans la pensée de l'industrie.

"La cryptographie Fiat utilisée dans BoringSSL profite à l'ensemble de la communauté [cryptographique], " dit-il. " [C'est] un signe que les temps changent et que les grands projets logiciels se rendent compte que la cryptographie non sécurisée est un handicap, [et montre] que le logiciel vérifié est suffisamment mature pour entrer dans le courant dominant. J'espère que de plus en plus de projets logiciels établis passeront à la cryptographie vérifiée. Peut-être dans les prochaines années, le logiciel vérifié deviendra utilisable non seulement pour les algorithmes cryptographiques, mais aussi pour d'autres domaines d'application."

Rejoindre Chlipala sur le papier sont :le premier auteur Andres Erbsen et les co-auteurs Jade Philipoom et Jason Gross, qui sont tous des étudiants diplômés du CSAIL ; ainsi que Robert Sloan MEng '17.

Diviser les bits

Les protocoles de cryptographie utilisent des algorithmes mathématiques pour générer des clés publiques et privées, qui sont essentiellement une longue chaîne de bits. Les algorithmes utilisent ces clés pour fournir des canaux de communication sécurisés entre un navigateur et un serveur. L'une des familles d'algorithmes cryptographiques efficaces et sécurisées les plus populaires est appelée cryptographie à courbe elliptique (ECC). Essentiellement, il génère des clés de différentes tailles pour les utilisateurs en choisissant des points numériques au hasard le long d'une ligne courbe numérotée sur un graphique.

La plupart des puces ne peuvent pas stocker de si grands nombres au même endroit, ils les divisent donc brièvement en chiffres plus petits qui sont stockés dans des unités appelées registres. Mais le nombre de registres et la quantité de stockage qu'ils fournissent varient d'une puce à l'autre. "Vous devez diviser les morceaux à travers un tas d'endroits différents, mais il s'avère que la façon dont vous divisez les bits a des conséquences différentes sur les performances, " dit Chlipala.

Traditionnellement, les experts qui écrivent des algorithmes ECC implémentent manuellement ces décisions de fractionnement de bits dans leur code. Dans leur travail, les chercheurs du MIT ont tiré parti de ces décisions humaines pour générer automatiquement une bibliothèque d'algorithmes ECC optimisés pour tout matériel.

Leurs chercheurs ont d'abord exploré les implémentations existantes d'algorithmes ECC manuscrits, dans les langages de programmation C et assembleur, et transféré ces techniques dans leur bibliothèque de code. Cela génère une liste des algorithmes les plus performants pour chaque architecture. Puis, il utilise un compilateur - un programme qui convertit les langages de programmation en code que les ordinateurs comprennent - qui s'est avéré correct avec un outil de vérification, appelé Coq. Essentiellement, tout le code produit par ce compilateur sera toujours vérifié mathématiquement. Il simule ensuite chaque algorithme et sélectionne le plus performant pour chaque architecture de puce.

Prochain, les chercheurs travaillent sur des moyens de rendre leur compilateur encore plus rapide dans la recherche d'algorithmes optimisés.

Compilation optimisée

Il existe une innovation supplémentaire qui garantit que le système sélectionne rapidement les meilleures implémentations de fractionnement de bits. Les chercheurs ont équipé leur compilateur basé sur Coq d'une technique d'optimisation, appelé « évaluation partielle, " qui précalcule essentiellement certaines variables pour accélérer les choses pendant le calcul.

Dans le système des chercheurs, il précalcule toutes les méthodes de fractionnement de bits. En les associant à une architecture de puce donnée, il rejette immédiatement tous les algorithmes qui ne fonctionneront tout simplement pas pour cette architecture. Cela réduit considérablement le temps nécessaire pour rechercher dans la bibliothèque. Une fois que le système s'est concentré sur l'algorithme optimal, il finalise la compilation du code.

À partir de ce, les chercheurs ont ensuite rassemblé une bibliothèque des meilleures façons de diviser les algorithmes ECC pour une variété d'architectures de puces. Il est maintenant implémenté dans BoringSSL, les utilisateurs puisent donc principalement dans le code des chercheurs. La bibliothèque peut être automatiquement mise à jour de la même manière pour les nouvelles architectures et les nouveaux types de mathématiques.

"Nous avons essentiellement écrit une bibliothèque qui, une fois pour toutes, est correct pour toutes les façons dont vous pouvez éventuellement diviser les nombres, " dit Chlipala. " Vous pouvez explorer automatiquement l'espace des représentations possibles des grands nombres, compiler chaque représentation pour mesurer la performance, et prenez celui qui court le plus vite pour un scénario donné."

Cette histoire est republiée avec l'aimable autorisation de MIT News (web.mit.edu/newsoffice/), un site populaire qui couvre l'actualité de la recherche du MIT, innovation et enseignement.