Chaque fois que vous achetez quelque chose sur Amazon, vos données client sont automatiquement mises à jour et stockées sur des milliers de machines virtuelles dans le cloud. Pour des entreprises comme Amazon, il est essentiel d'assurer la sûreté et la sécurité des données de ses millions de clients. Cela est vrai pour les grandes et les petites organisations. Mais jusqu'à présent, il n'y avait aucun moyen de garantir qu'un système logiciel est protégé contre les bogues, les pirates et les vulnérabilités.
Les chercheurs de Columbia Engineering ont peut-être résolu ce problème de sécurité. Ils ont développé SeKVM, le premier système qui garantit - par preuve mathématique - la sécurité des machines virtuelles dans le cloud. Dans un nouvel article qui sera présenté le 26 mai 2021 lors du 42e Symposium IEEE sur la sécurité et la confidentialité, les chercheurs espèrent jeter les bases des futures innovations dans la vérification des logiciels système, conduisant à une nouvelle génération de logiciels système cyber-résilients.
SeKVM est le premier système officiellement vérifié pour le cloud computing. La vérification formelle est une étape critique car il s'agit de prouver que le logiciel est mathématiquement correct, que le code du programme fonctionne comme il se doit et qu'il n'y a pas de bogues de sécurité cachés à craindre.
« C'est la première fois qu'un système logiciel multiprocesseur réel s'avère mathématiquement correct et sécurisé », a déclaré Jason Nieh, professeur d'informatique et codirecteur du Software Systems Laboratory. « Cela signifie que les données des utilisateurs sont correctement gérées par un logiciel exécuté dans le cloud et sont à l'abri des bugs de sécurité et des pirates. »
La construction de logiciels système corrects et sécurisés a été l'un des grands défis de l'informatique. | Nieh a travaillé sur différents aspects des systèmes logiciels depuis qu'il a rejoint Columbia Engineering en 1999. Lorsque Ronghui Gu, professeur adjoint d'informatique de la famille Tang et expert en vérification formelle, a rejoint le département d'informatique en 2018, lui et Nieh ont décidé de collaborer sur l'exploration de la vérification formelle des systèmes logiciels.
Leurs recherches ont suscité un intérêt majeur : les deux chercheurs ont remporté un Amazon Research Award, plusieurs subventions de la National Science Foundation, ainsi qu'un contrat de plusieurs millions de dollars avec la Defense Advanced Research Projects Agency (DARPA) pour poursuivre le développement du projet SeKVM. En outre, Nieh a reçu une bourse Guggenheim pour ce travail.
Au cours des douze dernières années, une grande attention a été accordée à la vérification formelle, y compris des travaux sur la vérification des systèmes d'exploitation multiprocesseurs. «Mais toutes ces recherches ont été menées sur de petits systèmes ressemblant à des jouets que personne n'utilise dans la vraie vie», a déclaré Gu. «La vérification d'un système de base multiprocesseur, un système largement utilisé comme Linux, a été considérée comme plus ou moins impossible.»
La croissance exponentielle du cloud computing a permis aux entreprises et aux utilisateurs de déplacer leurs données et leurs calculs hors site vers des machines virtuelles exécutées sur des hôtes dans le cloud. Les fournisseurs de cloud computing, comme Amazon, déploient des hyperviseurs pour prendre en charge ces machines virtuelles
Un hyperviseur est le logiciel clé qui rend possible le cloud computing. La sécurité des données de la machine virtuelle dépend de l'exactitude et de la fiabilité de l'hyperviseur. Malgré leur importance, les hyperviseurs sont compliqués : ils peuvent inclure un système d'exploitation Linux complet. Un seul maillon faible dans le code, quasiment impossible à détecter via des tests traditionnels, peut rendre un système vulnérable aux pirates. Même si un hyperviseur est écrit correctement à 99%, un pirate peut toujours se faufiler dans cette configuration particulière de 1% et prendre le contrôle du système.
Le travail de Nieh et Gu est le premier à vérifier un système de base, en particulier l'hyperviseur KVM largement utilisé, qui est utilisé pour exécuter des machines virtuelles par des fournisseurs de cloud tels qu'Amazon. Ils ont prouvé que SeKVM, qui est KVM avec quelques petits changements, est sécurisé et garantit que les ordinateurs virtuels sont isolés les uns des autres.
«Nous avons montré que notre système peut protéger et sécuriser les données privées et l'informatique téléchargées sur le cloud avec des garanties mathématiques», a déclaré Xupeng Li, Ph.D. de Gu. étudiant et co-auteur principal de l'article. «Cela n’a jamais été fait auparavant.»
SeKVM a été vérifié à l'aide de MicroV, un nouveau cadre de vérification des propriétés de sécurité des grands systèmes. Il est basé sur l'hypothèse que de petits changements apportés au système peuvent le rendre beaucoup plus facile à vérifier, une nouvelle technique que les chercheurs appellent la vérification MICR. Cette nouvelle technique de stratification modernise un système existant et extrait les composants qui assurent la sécurité dans un petit noyau qui est vérifié et garantit la sécurité de l'ensemble du système.
Les changements nécessaires pour moderniser un grand système sont assez modestes : les chercheurs ont démontré que si le petit noyau du plus grand système est intact, alors le système est sécurisé et aucune donnée privée ne sera divulguée. C'est ainsi qu'ils ont pu vérifier un gros système tel que KVM, ce qui était auparavant considéré comme impossible.
«Pensez à une maison - une fissure dans la cloison sèche ne signifie pas que l'intégrité de la maison est en danger», a expliqué Nieh. «Il est toujours structurellement solide et le système structurel clé est bon.»
Shih-Wei Li, Ph.D. de Nieh étudiant et co-auteur principal de l'étude, a ajouté: «SeKVM servira de garantie dans divers domaines, des systèmes bancaires et des dispositifs de l'Internet des objets aux véhicules autonomes et aux crypto-monnaies.»
En tant que premier hyperviseur de produits vérifié, SeKVM pourrait changer la façon dont les services cloud doivent être conçus, développés, déployés et approuvés. Dans un monde où cybersécurité est une préoccupation croissante, cette résilience est très demandée. Les grandes entreprises du cloud explorent déjà comment elles peuvent tirer parti de SeKVM pour répondre à cette demande.