La mauvaise cryptographie est malheureusement omniprésente. Les chances d’avoir une mise en œuvre cryptographique correctement faite sont très souvent inférieures à celles d’en avoir une mal faite à cause des bogues de programmation laissés par les développeurs. Mais ces genres de failles qui rendent la cryptographie exploitable par des individus malveillants sont en train d’être solutionnés. En effet, selon un rapport de Quanta Magazine publié le mardi, des chercheurs viennent de mettre au point une suite d’outils de cryptographie numérique à l’épreuve des pirates informatiques, des programmes ayant le même niveau d’invincibilité qu’une preuve mathématique.
Une preuve mathématique conduisant toujours à une conclusion attendue, ces outils de cryptographie publiés par ces chercheurs sont exempts des erreurs de programmation – des bogues – qui peuvent ouvrir des portes aux pirates informatiques et révéler des secrets numériques, c’est ce qu’espèrent une équipe d’informaticiens en publiant EverCrypt le mardi.
EverCrypt est un ensemble d’outils de cryptographie numérique. Les travaux sur EverCrypt ont commencé en 2016 dans le cadre du projet Everest, une initiative menée par Microsoft Research pour tenter de pallier les insuffisances des bibliothèques cryptographiques dans de nombreuses applications logicielles à l’époque et même aujourd’hui. Les bibliothèques étaient lentes à exécuter, ce qui réduisait la performance globale des applications dont elles faisaient partie, et elles étaient pleines de bogues.
Selon le rapport de Quanta Magazine, les chercheurs ont pu prouver mathématiquement comme ont peut le faire avec, par exemple, le théorème de Pythagore que leur nouvelle approche de la sécurité en ligne est complètement invulnérable aux principaux types d’attaques de piratage qui ont touché d’autres programmes dans le passé. « Quand nous disons preuve, nous voulons dire que nous prouvons que notre code ne peut pas subir ce genre d’attaques », a déclaré Karthik Bhargavan, un informaticien de l’Inria à Paris qui a participé aux travaux sur EverCrypt.
En effet, selon les chercheurs, EverCrypt n’a pas été écrit de la même façon que la plupart des codes. D’après le rapport, normalement, une équipe de programmeurs crée des logiciels en espérant qu’ils satisferont certains objectifs. Et une fois qu’ils ont terminé le programme, ils le testent. S’il atteint les objectifs sans montrer aucun comportement indésirable, les programmeurs concluent que le logiciel fait ce qu’il est censé faire. Pourtant, les erreurs de programmation ne se manifestent souvent que dans des « cas extrêmes », c’est-à-dire un ensemble d’événements improbables qui révèle les failles des logiciels qui sont exploitées par les pirates informatiques à l’origine des dégâts de plus en plus importants en nombre comme en ampleur.
« Il s’agit d’un échec en cascade, et c’est difficile à trouver systématiquement parce que les événements qui y ont mené sont tous très improbables individuellement », a déclaré Bryan Parno, informaticien à l’Université Carnegie Mellon qui a également travaillé sur EverCrypt.
Mais Bryan Parno et ses collègues ont introduit une tout autre méthode qui, selon eux, rend leur suite d’outils de cryptographie numérique invincible comme une preuve mathématique. Ils ont précisé exactement, selon le rapport, ce que leur code est censé faire et ont ensuite prouvé qu’il le fait et seulement cela, excluant la possibilité que le code puisse s’écarter de manière inattendue dans des circonstances inhabituelles. La stratégie générale est appelée « vérification formelle ».
« Vous pouvez réduire la question de savoir comment le code se comporte dans une formule mathématique, et ensuite vous pouvez vérifier si la formule tient. Si c’est le cas, vous savez que votre code a cette propriété, » a dit Parno.
« Je pense que les développeurs d’applications se sont rendu compte qu’un désastre est imminent », a déclaré Jonathan Protzenko, informaticien chez Microsoft Research qui a travaillé sur EverCrypt. « Le monde du logiciel est mûr pour quelque chose de nouveau qui offre des garanties », a-t-il ajouté en faisant référence à EverCrypt.
L’environnement de développement d’EverCrypt
EverCrypt est une bibliothèque de logiciels qui gère la cryptographie, ou l’encodage et le décodage d’informations privées. Ces bibliothèques cryptographiques sont naturellement mathématiques, d’après les informaticiens. Elles impliquent l’arithmétique avec des nombres premiers et des opérations sur des objets géométriques canoniques comme des courbes elliptiques. Définir ce que font les bibliothèques cryptographiques en termes formels n’est pas une mince affaire.
Dans la mise au point de cette bibliothèque, le plus grand challenge auquel ont face les informaticiens a été de développer une plateforme de programmation unique capable d’exprimer tous les différents attributs que les chercheurs recherchaient dans une bibliothèque cryptographique vérifiée. Et une telle plateforme n’existait pas encore lorsque les chercheurs ont commencé à travailler sur EverCrypt. Il a fallu en développer une. La plateforme dont ils avaient besoin devait être dotée de la capacité d’un langage logiciel traditionnel comme le C++, de la syntaxe logique et de la structure des programmes d’aide à la preuve comme Isabelle et Coq, que les mathématiciens utilisent depuis des années. Ce qui a conduit à un langage de programmation appelé F* qui a mis les mathématiques et le logiciel sur un pied d’égalité.
« Nous avons unifié ces éléments en un seul cadre cohérent de sorte que la distinction entre les programmes d’écriture et les épreuves soit vraiment réduite », a déclaré Bhargavan. « Vous pouvez écrire un logiciel comme si vous étiez un développeur de logiciel, mais en même temps vous pouvez écrire une preuve comme si vous étiez un théoricien. »
Les garanties apportées par EverCrypt
Comme première garantie qu’apporte EverCrypt, les chercheurs ont prouvé que la bibliothèque est exempte d’erreurs de programmation, comme les dépassements de tampon, qui peuvent permettre des attaques de pirates informatiques. Ils ont également prouvé qu’EverCrypt réussit à chaque fois les calculs cryptographiques, il n’effectue jamais le mauvais calcul, selon les informaticiens qui ont travaillé sur le projet.
Toutefois, selon les chercheurs, la garantie la plus importante d’EverCrypt est liée à une tout autre classe de faiblesses de sécurité qui a existé par le passé et jusqu’aujourd’hui. Celle-ci se produit lorsqu’un acteur malveillant déduit le contenu d’un message chiffré simplement en observant le fonctionnement d’un programme. Ce type d’attaques peut se produire lorsque le programme divulgue des informations à partir des erreurs de programmation.
« Quelque part au fond de votre algorithme ou de la façon dont vous implémentez votre algorithme, vous divulguez des informations, ce qui peut complètement aller à l’encontre de l’objectif de l’ensemble du chiffrement, » a déclaré Bhargavan. De telles « attaques par canal auxiliaire » sont à l’origine de plusieurs des cyberattaques les plus notoires de ces dernières années, dont l’attaque Lucky Thirteen, a rapporté le Quantamagazine. Les chercheurs ont prouvé qu’EverCrypt ne divulgue jamais d’informations d’une manière qu’elles peuvent être exploitées par ce type d’attaques au moment opportun.
EverCrypt n’annonce pas pour autant une ère de logiciels parfaitement sécurisés
Si EverCrypt est à l’abri de nombreux types d’attaques, il n’annonce pas pour autant une ère de logiciels parfaitement sécurisés. En effet, EverCrypt ne peut pas être prouvé sûr contre des attaques auxquelles personne n’a pensé auparavant, a dit M. Protzenko.
De plus, même une bibliothèque cryptographique vérifiée doit fonctionner de concert avec une foule d’autres logiciels, comme un système d’exploitation et de nombreuses applications de bureau courantes qui ne sont généralement pas vérifiés. « Nous ne ciblons pas quelque chose d’aussi complexe qu’un traitement de texte ou un client Skype », a déclaré M. Protzenko, car il n’est pas évident de savoir comment saisir dans un langage formel ce qu’il est censé faire. « C’est difficile de penser au comportement prévu de ces choses. »
A cause de ces vulnérabilités de programmes adjacents non vérifiés qui peuvent saper une bibliothèque cryptographique, Project Everest vise à entourer EverCrypt avec autant de logiciels vérifiés que possible. « Le projet Everest tente de construire une plus grande pile de logiciels qui ont tous été vérifiés et vérifiés pour fonctionner ensemble. Avec le temps, nous espérons que la frontière des logiciels vérifiés continuera de s’agrandir », a déclaré M. Parno.
Le Titanic était insubmersible, pourtant il a coulé. Ces outils présentés comme « totalement sécurisé », seront-il hackés ?