IdentifiantMot de passe
Loading...
Mot de passe oublié ?Je m'inscris ! (gratuit)

Vous êtes nouveau sur Developpez.com ? Créez votre compte ou connectez-vous afin de pouvoir participer !

Vous devez avoir un compte Developpez.com et être connecté pour pouvoir participer aux discussions.

Vous n'avez pas encore de compte Developpez.com ? Créez-en un en quelques instants, c'est entièrement gratuit !

Si vous disposez déjà d'un compte et qu'il est bien activé, connectez-vous à l'aide du formulaire ci-dessous.

Identifiez-vous
Identifiant
Mot de passe
Mot de passe oublié ?
Créer un compte

L'inscription est gratuite et ne vous prendra que quelques instants !

Je m'inscris !

Des chercheurs ont-ils publié une suite d'outils de cryptographie numérique mathématiquement totalement sécurisée,
Et exempte de bogues ?

Le , par Stan Adkens

220PARTAGES

12  1 
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 ?

Source : Quanta Magazine

Et vous ?

Que pensez-vous de la nouvelle bibliothèque cryptographique ?
Imaginez-vous une situation qui pourrait causer des problèmes à la nouvelle méthode de cryptographie ? Laquelle ?

Lire aussi

AMD PSP : le module cryptographique est affecté par une vulnérabilité, un dépassement de pile qui mène à son contrôle total
Google développe une suite d'outils pour tester des implémentations cryptographiques, le projet Wycheproof est open source
PHP 7.2 est disponible en version stable avec la bibliothèque de cryptographie Sodium, et d'autres améliorations et nouvelles fonctionnalités
Un niveau modéré de piratage des contenus protégés peut avoir un effet positif sur les ventes légales de ces œuvres, d'après des chercheurs
Le piratage catastrophique d'un fournisseur de services de messagerie détruit près de deux décennies de données, relatives à des courriels

Une erreur dans cette actualité ? Signalez-nous-la !

Avatar de dourouc05
Responsable Qt & Livres https://www.developpez.com
Le 04/04/2019 à 16:50
Citation Envoyé par Aiekick Voir le message
mème si l’implémentation est correcte, le bug peut ce trouver dans le compilateur qui conduira a un problème logiciel.
Si tu prends un compilateur au hasard (ce qui semble le cas ici, si pas pire, vu qu'ils ont implémenté leur propre langage), ce n'est pas vraisemblable, c'est certain. Maintenant, tu as aussi des compilateurs développés selon les mêmes principes : par exemple, http://compcert.inria.fr/compcert-C.html et https://cakeml.org/. Dans ce cas, les défauts peuvent encore résider du côté des prouveurs de théorèmes (malheureusement, Coq https://github.com/coq/coq, le prouveur derrière CompCert, utilise une suite de tests )

Citation Envoyé par Aiekick Voir le message
Donc parler de piratage impossible, puis exempt de bogue et totalement sécurisé est trompeur et faux.
C'est une conclusion bien rapide. Une implémentation vérifiée comme ça sera toujours beaucoup plus sûre qu'une autre. Ensuite, on ne peut vérifier que par rapport à des théories existantes sur les vecteurs d'attaque possibles. C'est plutôt qu'il faut être extrêmement ingénieux pour arriver à trouver une faille, puisqu'il faudrait faire quelque chose d'entièrement nouveau par rapport à toutes les attaques dont cette implémentation se prémunit.
3  0 
Avatar de Aiekick
Membre extrêmement actif https://www.developpez.com
Le 04/04/2019 à 13:02
mème si l’implémentation est correcte, le bug peut ce trouver dans le compilateur qui conduira a un problème logiciel.

ceci étant le titre de cette news est trompeur sur ce que disent vraiment les chercheurs, chose que l'ont découvre en fin d'article.

ils disent eux mème qu'il n'est pas sécurisé sur des nouveaux type d'attaque encore inconnu a ce jour.

D'un cote les chercheurs disent que leur implémentation n'a pas été concu suivant les procédés habituels, cad on fait et on teste sur un nombre de user case,
mais en fin d'article on apprend que il peut y avoir des failles faces a des nouveaux vecteurs d'attaque.

Donc parler de piratage impossible, puis exempt de bogue et totalement sécurisé est trompeur et faux.

Article intéressant mais a mon sens trop accrocheur et confus sur certains points.
1  0 
Avatar de Anselme45
Membre extrêmement actif https://www.developpez.com
Le 04/04/2019 à 11:15
... une suite d'outils de cryptographie numérique qui s'est avérée mathématiquement totalement sécurisée. Et exempte de bogues
Et mon coiffeur rase gratis!

Osez dire "totalement sécurisée" et "exempte de bogues" concernant un système informatique, c'est soit prendre les gens pour des imbéciles, soit être le dernier des crétins!
3  3 
Avatar de KsassPeuk
Membre confirmé https://www.developpez.com
Le 05/04/2019 à 12:49
Citation Envoyé par Stan Adkens Voir le message
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.
Ça fait un peu chier de voir qu'on ne retient que Microsoft comme fondateur. Le consortium contient un peu plus de membres que ça. Ok, les autres sont cités rapidement un peu plus tard mais à la base le consortium est plus large, et la communauté méthode formelle à bosser dessus est assez grosse.

C'est aussi dommage de ne pas citer que HACL*, un des résultats d'Everest est maintenant utilisés dans Firefox.

Autre point qui me semble important par rapport à la news, on a l'impression à la lecture (mais ce n'est peut être que moi), que les méthodes formelles sont quelque chose d'extrêmement nouveau. Ce n'est pas le cas. Ça existe depuis des décennies, et il y a de nombreux outils sur le marché pour faire ce genre de travail. Ce qui permet d'arriver à un niveau de fiabilité qui est très coûteux, certes, mais sans comparaison avec des méthodes de vérification plus conventionnelles en terme de sûreté et sécurité.

Citation Envoyé par Anselme45 Voir le message
Osez dire "totalement sécurisée" et "exempte de bogues" concernant un système informatique, c'est soit prendre les gens pour des imbéciles, soit être le dernier des crétins!
Autant le problème de la formulation "exempts de bogues" est qu'elle est trop imprécise (parce qu'il faut définir précisément ce qu'on entend par bug) et la formulation "totalement sécurisée" élude un élément important de toute preuve crypto (la proba de fuite d'info), autant ce serait bien de se renseigner sur ce qui est présenté avant de railler ... Parce que ta phrase en elle-même n'a pas plus de sens que leur formulation douteuse. Il serait difficilement défendable de dire qu'un programme de 10 lignes ne peut pas être parfaitement exempt de bug et sécurisé. On a alors la réponse "oui mais on parle de vrais systèmes, qui font plus de 10 lignes". D'accord. Du coup c'est à partir de combien de lignes qu'on passe de possible à impossible ?

Citation Envoyé par dourouc05 Voir le message
Maintenant, tu as aussi des compilateurs développés selon les mêmes principes : par exemple, http://compcert.inria.fr/compcert-C.html et https://cakeml.org/. Dans ce cas, les défauts peuvent encore résider du côté des prouveurs de théorèmes (malheureusement, Coq https://github.com/coq/coq, le prouveur derrière CompCert, utilise une suite de tests )
Malheureusement, c'est plus simple que ça : tu ne peux pas prouver une théorie dans elle-même. Donc l'idée est d'avoir une théorie de base sur laquelle on se repose (et pour laquelle on a par ailleurs de bonnes raisons de penser qu'elle est cohérente (et pour ça, on repose sur des preuves papiers)) et de l'implémenter avec un coeur de confiance aussi petit que possible pour que ce soit facile de se pencher dessus et d'évaluer sa qualité (notamment par du test). Coq est un système assez riche, donc ça fait un gros coeur, mais il y a des systèmes avec des coeurs de taille très modérée.

Mais la présence possible de bugs dans Coq n'est pas fondamentalement bloquante. Pour qu'un bug soit vraiment problématique dans un tel système il faut avoir des bugs qui :
  • permettent de prouver quelque chose de faux
  • soient possibles à déclencher suffisamment facilement pour que ça impacte notre système
  • qu'on ne s'aperçoive pas que l'on est en train de prouver quelque chose de faux

Ça fait pas mal de conditions, et fort heureusement, c'est dur de trouver un bug tel que le premier (mais c'est déjà arrivé dans Coq). C'est encore plus dur de le déclencher, et en général, c'est plutôt des gens qui jouent avec le coeur de Coq pendant leurs recherches qui tombent sur ce genre d'anomalies, pas ceux qui utilisent les fonctionnalités plus habituelles. Et on a tendance à s'apercevoir qu'on est en train de faire un truc pas clair, surtout quand en plus d'un coup on se met à tout prouver avec beaucoup trop de facilité (parce que quand on a une preuve de faux, on prouve tout ce qu'on veut).

Comparativement, les hypothèses que l'on fait sur nos environnements d'exécution sont bien plus fortes. Par exemple, il existe un OS prouvé formellement, seL4, dans lequel plusieurs bugs ont déjà été découverts. Si je me souviens bien, tous ces bugs étaient dus à des hypothèses fausses à propos du matériel (coucou Spectre). C'est notamment une des raisons pour lesquelles pas mal de chercheurs en méthodes formelles poussent à ce que l'on développe des architectures processeur elle-mêmes formellement prouvées.

Citation Envoyé par dourouc05 Voir le message
Ensuite, on ne peut vérifier que par rapport à des théories existantes sur les vecteurs d'attaque possibles. C'est plutôt qu'il faut être extrêmement ingénieux pour arriver à trouver une faille, puisqu'il faudrait faire quelque chose d'entièrement nouveau par rapport à toutes les attaques dont cette implémentation se prémunit.
Pour être un peu plus précis sur l'aspect "vecteurs d'attaque possible" ici. Ils ont quand même quelques garanties (s'ils utilisent un compilo vérifié), notamment l'absence d'exploit dus à des runtimes errors (le truc classique en C), et le fait que leur implémentation correspond bien à la définition formelle du protocole. Ce qui reste c'est, comme je l'ai dit avant les suppositions sur l'environnement d'exécution, et la possibilité qu'il existe un faille intrinsèque au protocole (il y a aussi de gros travaux en ce moment de ce côté dans la communauté méthodes formelles).
0  0