L’équipe crée le premier système logiciel cloud résistant aux hackers

L'équipe d'ingénierie de Columbia crée le premier système logiciel cloud résistant aux hackers

Microverification des hyperviseurs cloud. Crédit: Jason Nieh et Ronghui Gu / Columbia Engineering

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 une 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 en matière de 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 se révèle 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 fonctionnant dans le cloud et sont à l’abri des bogues 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.

Leur recherche a 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 de 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 aux travaux de 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 commodité 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.

L'équipe d'ingénierie de Columbia crée le premier système logiciel cloud résistant aux hackers

Microverification des hyperviseurs cloud. Crédit: Jason Nieh et Ronghui Gu / Columbia Engineering

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 complexes: ils peuvent inclure un système d’exploitation Linux entier. 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 microvérification. 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ù la cybersécurité est une préoccupation croissante, cette résilience est très demandée. Les grandes entreprises du cloud explorent déjà comment tirer parti de SeKVM pour répondre à cette demande.

L’étude s’intitule «Un hyperviseur KVM Linux sécurisé et officiellement vérifié».

L’étude sera présentée lors du 42e symposium de l’IEEE sur la sécurité et la confidentialité le 26 mai 2021.


Amazon ramène un ancien dirigeant pour gérer son activité cloud


Plus d’information:
Un hyperviseur KVM Linux sécurisé et officiellement vérifié, DOI: 10.1109 / SP40001.2021.00049

Fourni par l’École d’ingénierie et de sciences appliquées de l’Université Columbia

Citation: L’équipe crée le premier système logiciel cloud résistant aux hackers (2021, 25 mai) récupéré le 25 mai 2021 sur https://techxplore.com/news/2021-05-team-hacker-resistant-cloud-software.html

Ce document est soumis au droit d’auteur. En dehors de toute utilisation équitable à des fins d’étude ou de recherche privée, aucune partie ne peut être reproduite sans l’autorisation écrite. Le contenu est fourni seulement pour information.