Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

  1. #1
    Chroniqueur Actualités

    Homme Profil pro
    Consultant informatique
    Inscrit en
    avril 2018
    Messages
    440
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Côte d'Ivoire

    Informations professionnelles :
    Activité : Consultant informatique
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : avril 2018
    Messages : 440
    Points : 14 592
    Points
    14 592

    Par défaut Les chercheurs ont publié une suite d'outils de cryptographie numérique qui ne peut pas être piratée ?

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

    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.

    Nom : Cryp.jpg
Affichages : 5301
Taille : 75,3 Ko

    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
    Contribuez au club : Corrections, suggestions, critiques, ... : Contactez le service news et Rédigez des actualités

  2. #2
    Membre expérimenté
    Homme Profil pro
    Développeur informatique
    Inscrit en
    octobre 2017
    Messages
    323
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Suisse

    Informations professionnelles :
    Activité : Développeur informatique

    Informations forums :
    Inscription : octobre 2017
    Messages : 323
    Points : 1 357
    Points
    1 357

    Par défaut

    ... 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
    Membre extrêmement actif
    Homme Profil pro
    Consultant Ingenierie mécanique
    Inscrit en
    mars 2006
    Messages
    1 071
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Yvelines (Île de France)

    Informations professionnelles :
    Activité : Consultant Ingenierie mécanique
    Secteur : Transports

    Informations forums :
    Inscription : mars 2006
    Messages : 1 071
    Points : 2 284
    Points
    2 284

    Par défaut

    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.

  4. #4
    Responsable Qt & Livres


    Avatar de dourouc05
    Homme Profil pro
    Ingénieur de recherche
    Inscrit en
    août 2008
    Messages
    24 329
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Val de Marne (Île de France)

    Informations professionnelles :
    Activité : Ingénieur de recherche
    Secteur : Enseignement

    Informations forums :
    Inscription : août 2008
    Messages : 24 329
    Points : 160 119
    Points
    160 119

    Par défaut

    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.
    Vous souhaitez participer aux rubriques Qt ou PyQt (tutoriels, FAQ, traductions), HPC ? Contactez-moi par MP.

    Créer des applications graphiques en Python avec PyQt5
    Créer des applications avec Qt 5.

    Pas de question d'ordre technique par MP !

  5. #5
    Membre confirmé Avatar de KsassPeuk
    Homme Profil pro
    Post-Doctorant
    Inscrit en
    juillet 2013
    Messages
    119
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France

    Informations professionnelles :
    Activité : Post-Doctorant
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : juillet 2013
    Messages : 119
    Points : 486
    Points
    486

    Par défaut

    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).

Discussions similaires

  1. Réponses: 1
    Dernier message: 21/12/2016, 16h31
  2. Réponses: 24
    Dernier message: 06/12/2016, 16h53
  3. Réponses: 8
    Dernier message: 25/01/2011, 09h23
  4. Fonction qui renvoie les premières lettres d'une suite de mots
    Par shaun_the_sheep dans le forum Oracle
    Réponses: 16
    Dernier message: 30/06/2010, 13h58
  5. Les sessions ont-ils une taille limite?
    Par wormseric dans le forum Sessions
    Réponses: 1
    Dernier message: 26/03/2008, 10h11

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo