« Un jour on sera attaqué » : cryptographie et méthodes formelles au chevet de la cybersécurité
Pour éviter d’accuser un « bug » et le stagiaire
Notre dossier sur le plan Cyber :
Le 02 mars 2021 à 11h06
11 min
Internet
Internet
Contre les cyberattaques, les mathématiques sont une aide précieuse. On connait la cryptographie pour protéger les données de regards indiscrets et limiter les dégâts en cas de fuite. Il y a aussi les méthodes formelles pour « générer des garanties » et le machine learning pour épauler les experts… avant de les remplacer ?
Après le plan quantique (lire notre dossier), le gouvernement a récemment annoncé un plan sur la cybersécurité avec un milliard d’euros à la clé, dont 720 millions de financements publics. Il comprend six grands piliers, qui ont été détaillés par une demi-douzaine de chercheurs des trois laboratoires impliqués : CEA, CNRS et Inria.
Ils pilotent notamment les Programmes et équipements prioritaires de recherche (PEPR), qui se voient attribuer 65 millions d'euros. Dans cette seconde partie de notre dossier, nous revenons en détail sur les enjeux et les attentes de deux des six piliers : le codage et la cryptographie tout d'abord, avec des explications de David Pointcheval (cryptographe du CNRS au Département d'informatique de l'École Normale Supérieure), puis les méthodes formelles avec Florent Kirchner (responsable du programme Cybersécurité du CEA List).
- Cybersécurité : on peut prouver que « la sécurité parfaite n'existe pas »
- Cybersécurité : le miroir aux alouettes de l’open source, la confiance dans les composants
- « Un jour ou l'autre on sera attaqué » : cryptographie et méthodes formelles au chevet de la cybersécurité
- En cybersécurité, « la maîtrise totale est sans doute totalement hors de portée »
Certains dommages sont « irréparables »
Personne ne peut revendiquer disposer de cyberprotections à toute épreuve, un point d’autant plus inquiétant que, c’est une quasi-certitude, « un jour ou l'autre on sera attaqué », lâche David Pointcheval. Cela ne doit pas empêcher de dresser et vérifier un maximum de protections, mais il faut aussi anticiper le pire.
Le chercheur se veut rassurant : « Si la détection est assez rapide sur certaines attaques telles que les rançongiciels […] et si de bonnes mesures ont été prises, on peut espérer une réparation sans séquelles ». Il ne faut pas généraliser pour autant : on ne peut pas toujours faire machine arrière.
« Ce n'est pas forcément le cas dans les fuites d'informations sensibles, qui peuvent d'un côté prendre beaucoup de temps pour être détectées, et de plus conduire à des dommages irréparables, notamment s'il s'agit de données personnelles ». Avec un rançongiciel, on peut en effet restaurer une sauvegarde. Avec une fuite de données, impossible de rappeler les informations dévoilées, elles sont dans la nature et y resteront.
Un des buts de la cryptographie est justement de limiter les risques : assurer la « confidentialité des données stockées, transmises ou calculées, avec des garanties que l'on appelle parfois mathématiques », explique le cryptographe du CNRS. Il ajoute qu’il existe des « méthodes sûres, ou tout du moins des méthodes raisonnables » pour assurer la confidentialité du « stockage et des communications ».
Avec tout de même un bémol important dans la pratique : il y a en effet de « nombreuses menaces résiduelles […] telles que des failles dans les briques élémentaires qui sont la base de la sécurité des systèmes ».
Le spectre de l’ordinateur quantique sur la cryptographie
Des algorithmes considérés comme sûrs pendant un temps peuvent rapidement représenter un danger, voire devenir des passoires ; le passé regorge d’exemples. On peut citer le cas emblématique d’Heartbleed, quand une brèche dans une brique open source a fait trembler Internet, la menace (à venir) de l’ordinateur quantique, etc.
- Quand le chiffrement des données est mis à mal par des mathématiciens
- Chiffrement et sécurité dans tous leurs états, du WEP à la distribution quantique de clés
Il n’est pour le moment pas en mesure de battre un ordinateur classique sur des problèmes « utiles » – c’est pour cela que certains parlent plutôt d’avantage quantique à la place de suprématie – mais son spectre inquiète, à raison. Peu importe que ce soit dans un horizon de cinq ou quinze ans, une machine quantique sera un jour capable de casser certains pans de la cryptographie actuelle.
Il « suffit » donc de stocker dès à présent des données (des communications par exemple) pour les décrypter dans plusieurs années. C’est d’autant plus vrai que, « avant même l'existence d'un véritable ordinateur quantique, on a déjà à notre disposition des algorithmes qui seront efficaces pour casser la cryptographie actuelle ».
Bonne nouvelle, des parades sont disponibles et d’autres sont à l’étude : « les cryptographes travaillent sur la cryptographie quantique avec de nouveaux systèmes pour nos ordinateurs actuels qui résisteront à un éventuel ordinateur quantique attaquant pour l'exploiter ».
Dilemme moderne : traitement de masse VS vie privée
Pour David Pointcheval on serait actuellement confronté à un dilemme :
« Soit on ne traite pas les données parce qu'elles sont trop sensibles, et cela peut conduire à un manque à gagner important dans de nombreux domaines où les données ont une grande valeur. Soit on traite, mais on ne protège pas assez, voire on ne protège pas du tout ses données et donc avec de gros risques de fuite ».
Il cite l’exemple de l’apprentissage automatique, une technique nécessitant de très grandes quantités de données pour entrainer les algorithmes, « parfois très sensibles comme des données personnelles, médicales, financières, économiques… ». Traiter en masse avec une garantie de la confidentialité est actuellement un « enjeu majeur » en cryptographie. Des solutions existent, mais malgré d’importantes améliorations, « elles restent encore coûteuses et limitées ». On peut citer le chiffrement homomorphe, sur lequel nous aurons l’occasion de revenir.
Un exemple frappant concerne le vote électronique ou « l’authenticité, l'intégrité des données et des calculs » sont des points primordiaux, qui doivent se conjuguer « avec un fort besoin de confidentialité ». On doit arriver à des résultats « sincères » avec un maximum de précaution sur le respect de la vie privée… et ce n’est pas si simple.
David Pointcheval cite aussi l’exemple de la « décentralisation, dans des contextes où nul ne peut faire confiance à un tiers, comme dans le cas de la blockchain ».
Méthodes formelles et preuves mathématiques
Florent Kirchner, responsable du programme Cybersécurité du CEA List, prend la relève pour le second pilier de la cybersécurité : les méthodes formelles. Le chercheur commence par un rappel : « c'est utiliser des bases, des théories et des raisonnements mathématiques pour donner des outils qui permettent de comprendre les systèmes numériques dans toute leur complexité, et de générer des garanties qui ont la force de preuves mathématiques ».
Certains systèmes nécessitent en effet de produire des preuves (aussi appelées démonstrations) mathématiques. Depuis des années, c’est le cas « des cartes à puce qui sont critiques pour le domaine bancaire et qui requièrent de fournir des garanties très fortes de leur fonctionnement ».
Dans ce domaine de la cybersécurité, les mathématiques permettent deux choses intéressantes : « D'abord, une fois qu'on a construit cette garantie, de s'assurer qu'il y a une forme d'exhaustivité […] Le deuxième impact, c'est que les mathématiques sont facilement automatisables – en tout cas ça peut s’automatiser, facilement c'est peut-être un peu rapide ». Florent Kirchner détaille « trois défis » actuels des méthodes formelles en cybersécurité :
« Le premier, c'est la complexification de ce qui constitue une vulnérabilité […] On voit par exemple avec les failles Spectre-Meltdown que finalement, aujourd'hui, les attaques évoluent pour devenir de plus en plus complexes. Dans une attaque logicielle, elles exploitent, par exemple, un dysfonctionnement ou une faille du matériel […]
Le deuxième défi, c'est celui de traiter des systèmes nouveaux et de plus en plus complexes. Et à ce titre-là, c'est intéressant de prendre l'exemple du vote électronique pour lequel on veut non seulement avoir des garanties sur le résultat du vote, mais aussi sur l'anonymat des votants […] Mais on a aussi tous les systèmes déjà en place – qu'on appelle legacy – et qui sont de plus en plus nombreux, qui restent et qu'il faut pouvoir sécuriser en place […].
Le troisième défi, c'est que ces systèmes – qu’ils soient nouveaux ou anciens – deviennent de plus en plus dynamiques. Tout le monde a en tête l'exemple de Tesla, qui met à jour ses voitures tous les dix jours grosso modo ces derniers temps. Mais également un exemple comme SolarWinds, une attaque toute récente sur un système de gestion de l'infrastructure informatique utilisé par les grands acteurs, en particulier chez nos collègues américains ».
Même si on construit son système comme une forteresse, il faut régulièrement le mettre à jour, ce qui en fait potentiellement un vecteur d’attaque. Il faut également vérifier régulièrement les briques élémentaires de son système, car un seul petit composant défectueux peut faire tomber l’ensemble comme un château de cartes.
Ce dessin de xkcd résume parfaitement la situation.
Espoir du machine learning, douche froide sur les données
Pour détecter d’éventuels risques de brèches, l’informatique moderne peut apporter une aide importante. Ludovic Mé, adjoint au directeur scientifique d’Inria en charge du domaine de recherche « Cybersécurité », explique ainsi que le « machine learning est un grand espoir dans le monde de la sécurité réactive »… mais ce n’est pour le moment guère plus qu’un espoir : « On n’a pas vu de révolution [...], on en est toujours à évaluer l'apport réel des différents mécanismes […], on en est dans une phase d'expérimentation ».
Comme pour le quantique, nous sommes à un point de pivot : « Ces systèmes à base de machine learning permettent de faire parfois/souvent – j'hésite entre parfois et souvent, on est encore en train de rechercher, c'est difficile de se prononcer – à faire aussi bien que les experts humains ». David Pointcheval va plus loin : dans « des mécanismes complexes, seuls des outils automatiques peuvent aider l'humain ».
Les attentes sont pourtant élevées dans un marché où les systèmes « génèrent énormément de données et [où] il faut beaucoup d'experts humains » pour les traiter… sans oublier que ces experts ne sont pas nombreux. Bref, les enjeux économiques et en termes de sécurité sont importants.
Sur le sujet du machine learning, Ludovic Mé rejoint David Pointcheval concernant l’accès aux données : « Pour vraiment être capable de faire de bons systèmes de détection, il faudra avoir beaucoup de données qui permettent de les entrainer et ça, c'est un problème extrêmement aigu : on a beaucoup beaucoup beaucoup beaucoup (sic) de mal dans le monde académique à avoir des données pertinentes en volume suffisant ».
Même quand il n’y a aucune intrusion, ces données sont généralement considérées comme sensibles par les entreprises, qui ne veulent laisser personne y accéder, y compris pour des recherches. « On court après des volumes de données importants depuis des années », regrette le chercheur de l’Inria.
Dans le prochain article de notre dossier, nous reviendrons sur d’autres piliers du plan cybersécurité comme la protection de la vie privée et l’anonymisation, la sécurité des systèmes, des logiciels et des réseaux, la sécurité des contenus multimédia et enfin celle du matériel.
« Un jour on sera attaqué » : cryptographie et méthodes formelles au chevet de la cybersécurité
-
Certains dommages sont « irréparables »
-
Le spectre de l’ordinateur quantique sur la cryptographie
-
Dilemme moderne : traitement de masse VS vie privée
-
Méthodes formelles et preuves mathématiques
-
Espoir du machine learning, douche froide sur les données
Commentaires (8)
Vous devez être abonné pour pouvoir commenter.
Déjà abonné ? Se connecter
Abonnez-vousLe 02/03/2021 à 11h18
Les méthodes formelles c’est bien mais ça reste très limité au monde académique. Vous avez déjà essayé d’utiliser Coq ? Quand on s’éloigne des exemples triviaux, ça devient d’une extrême complication pour réussir à traiter et comprendre tous les cas.
Et derrière ça (comme dit l’article), vérifier que l’implémentation respecte et implémente correctement tous les cas particuliers détectés par les méthodes formelles reste un travail titanesque.
Le 03/03/2021 à 09h53
Ben à l’époque du développement de la première ligne de métro automatique à Paris, l’ensemble du logiciel a été « prouvé » à l’aide de méthodes formelles. C’était effectivement en partenariat avec le monde académique (inria / ensimag), mais ça me semble très concret pour le coup !
Le 02/03/2021 à 12h15
En SSI, on a coutume de dire : “il y a deux catégories d’entreprises : celles qui ont été hackées au moins une fois, et celles qui ne savent pas qu’elles ont été hackées au moins une fois”.
Cependant, bien que pessimiste de nature, je reste réservé sur certaines de ces technos.
Côté quantique, il faut un nombre conséquent de qubits pour cracker une clé asymétrique (les clés symétriques n’étant pas sensibles à ce type d’attaque). Or la décohérence quantique force à multiplier les qubits “correctifs” pour avoir des qubits “utiles”, ce qui fait qu’on est en ce moment face à un mur qu’on arrive à contourner mais pas à franchir. Il faudrait maintenant non pas des progrès mais une découverte pour que l’informatique quantique puisse servir à (ou plutôt contre) la factorisation d’entiers, à la base du chiffrement asymétrique. Et a priori une découverte au moins équivalente à ce qu’a pu être le transistor miniaturisé, sauf que pour le transistor on reste dans un monde électrique, maîtrisable, alors que pour le quantique on entre dans le monde des particules beaucoup moins dociles que prévues, cf la déconvenue de Microsoft à ce sujet.
Côté chiffrement homomorphe, les avancées sont très lentes là aussi, et les annonces se multiplient sans qu’en pratique on n’atteigne la possibilité d’un algorithme utilisable en pratique. On attend depuis longtemps que ça progresse (ça serait l’idéal pour aller dans le cloud), mais les déceptions s’accumulent…
Ca ressemble aussi aux mécanismes formels, qui va de déceptions en déceptions, d’autant que la complexité des systèmes actuels rend d’autant plus difficile leur démonstration…
Donc tout en restant méfiant, il faut aussi remettre les choses à leur place : en entreprise, la menace provient le plus souvent d’un simple e-mail, et non de techniques expérimentales. Mais je ne suis pas devin, et l’avenir sera toujours plein de surprises…
Le 02/03/2021 à 12h54
Les méthodes formelles développées au CEA l’ont notamment été pour auditer le code informatique utilisé dans la gestion des centrales nucléaires. L’enjeu valait le coup de se faire des nœuds au cerveau. Par contre l’environnement matériel et logiciel de tels système est très bien maîtrisé (comme pour les cartes à puces je suppose).
Bon courage pour implanter ça pour un data-center qui fournit derrière des services de stockage objet pour des applications sensibles !
Le 02/03/2021 à 13h26
Pour info :
Le 03/03/2021 à 14h36
Merci pour l’article. C’est expliqué relativement simplement, avec des ordres de grandeurs. Ca permet au lecteur moyen que nous sommes de rationnaliser les annonces plus ou moins dithyrambiques des acteurs du secteur, même si la communication s’est assagie en 2021.
Le 03/03/2021 à 13h04
Avec les méthodes formelles, on peut aussi créer ou améliorer des langages de programmation existants qui auront by design des propriétés de sécurité à un certain nombre d’attaques.
Typiquement il y a des travaux pour des versions améliorées de la grammaire SQL pour robustifier de facto tout risque d’attaque par injection.
Les méthodes formelles permettent aussi de développer des outils d’analyse automatisés qui vont permettre de valider (ou non) des propriétés prédéfinies, que ce soit sur du code ou des modèles.
Bref c’est compliqué mais c’est stylé les méthodes formelles.
Le 03/03/2021 à 16h12
C’est pas toujours de la faute du stagiaire
https://www.toolbox.com/security/threat-reports/news/solarwinds-ceo-blames-intern-for-github-password-fiasco/