Wenn Sie etwas bei Amazon kaufen, werden Ihre Kundendaten automatisch aktualisiert und auf Tausenden von virtuellen Maschinen in der Cloud gespeichert. Für Unternehmen wie Amazon ist die Gewährleistung der Sicherheit der Daten von Millionen von Kunden von entscheidender Bedeutung. Dies gilt sowohl für große als auch für kleine Organisationen. Bisher konnte jedoch nicht garantiert werden, dass ein Softwaresystem vor Fehlern, Hackern und Sicherheitslücken geschützt ist.
Forscher von Columbia Engineering haben dieses Sicherheitsproblem möglicherweise gelöst. Sie haben SeKVM entwickelt, das erste System, das durch mathematische Beweise die Sicherheit virtueller Maschinen in der Cloud garantiert. In einem neuen Artikel, der am 26. Mai 2021 auf dem 42. IEEE-Symposium für Sicherheit und Datenschutz vorgestellt wird, hoffen die Forscher, den Grundstein für zukünftige Innovationen bei der Überprüfung von Systemsoftware zu legen, die zu einer neuen Generation von Cyber-Resilient-Systemsoftware führen.
SeKVM ist das erste formal verifizierte System für Cloud Computing. Die formale Überprüfung ist ein entscheidender Schritt, da nachgewiesen werden muss, dass die Software mathematisch korrekt ist, der Code des Programms ordnungsgemäß funktioniert und keine versteckten Sicherheitslücken bestehen, über die Sie sich Sorgen machen müssen.
"Dies ist das erste Mal, dass sich gezeigt hat, dass ein reales Multiprozessor-Softwaresystem mathematisch korrekt und sicher ist", sagte Jason Nieh, Professor für Informatik und Co-Direktor des Software Systems Laboratory. "Dies bedeutet, dass die Benutzerdaten von der in der Cloud ausgeführten Software korrekt verwaltet werden und vor Sicherheitslücken und Hackern geschützt sind."
Der Aufbau einer korrekten und sicheren Systemsoftware war eine der großen Herausforderungen beim Rechnen. | Nieh hat seit seinem Eintritt bei Columbia Engineering im Jahr 1999 an verschiedenen Aspekten von Softwaresystemen gearbeitet. Als Ronghui Gu, Assistenzprofessor für Informatik in der Tang-Familie und Experte für formale Verifikation, 2018 in die Abteilung für Informatik eintrat, beschlossen er und Nieh, zusammenzuarbeiten zur Erforschung der formalen Verifikation von Softwaresystemen.
Ihre Forschung hat großes Interesse geweckt: Beide Forscher gewannen einen Amazon Research Award, mehrere Zuschüsse der National Science Foundation sowie einen Auftrag der Defense Advanced Research Projects Agency (DARPA) in Höhe von mehreren Millionen Dollar, um die Entwicklung des SeKVM-Projekts voranzutreiben. Darüber hinaus erhielt Nieh für diese Arbeit ein Guggenheim-Stipendium.
In den letzten zwölf Jahren wurde der formalen Überprüfung viel Aufmerksamkeit geschenkt, einschließlich der Arbeit an der Überprüfung von Multiprozessor-Betriebssystemen. "Aber all diese Forschungen wurden an kleinen spielzeugähnlichen Systemen durchgeführt, die niemand im wirklichen Leben verwendet", sagte Gu. "Die Überprüfung eines Multiprozessor-Warensystems, eines weit verbreiteten Systems wie Linux, wurde als mehr oder weniger unmöglich angesehen."
Das exponentielle Wachstum des Cloud Computing hat es Unternehmen und Benutzern ermöglicht, ihre Daten und Berechnungen außerhalb des Standorts in virtuelle Maschinen zu verschieben, die auf Hosts in der Cloud ausgeführt werden. Cloud-Computing-Anbieter wie Amazon setzen Hypervisoren ein, um diese virtuellen Maschinen zu unterstützen
Ein Hypervisor ist das Schlüsselstück der Software, die Cloud Computing ermöglicht. Die Sicherheit der Daten der virtuellen Maschine hängt von der Richtigkeit und Vertrauenswürdigkeit des Hypervisors ab. Trotz ihrer Bedeutung sind Hypervisoren kompliziert - sie können ein ganzes Linux-Betriebssystem enthalten. Nur ein einziges schwaches Glied im Code - eines, das mit herkömmlichen Tests praktisch nicht zu erkennen ist - kann ein System für Hacker anfällig machen. Selbst wenn ein Hypervisor zu 99% korrekt geschrieben ist, kann sich ein Hacker dennoch in diese bestimmte 1% -Einstellung einschleichen und die Kontrolle über das System übernehmen.
Die Arbeit von Nieh und Gu ist die erste, die ein Warensystem überprüft, insbesondere den weit verbreiteten KVM-Hypervisor, mit dem virtuelle Maschinen von Cloud-Anbietern wie Amazon ausgeführt werden. Sie haben bewiesen, dass SeKVM, bei dem es sich um KVM mit einigen kleinen Änderungen handelt, sicher ist und garantiert, dass virtuelle Computer voneinander isoliert sind.
"Wir haben gezeigt, dass unser System private Daten und Computer, die in die Cloud hochgeladen wurden, mit mathematischen Garantien schützen und sichern kann", sagte Xupeng Li, Ph.D. Student und Co-Hauptautor der Arbeit. "Das wurde noch nie gemacht."
SeKVM wurde mit MicroV überprüft, einem neuen Framework zur Überprüfung der Sicherheitseigenschaften großer Systeme. Es basiert auf der Hypothese, dass kleine Änderungen am System die Überprüfung erheblich vereinfachen können, eine neue Technik, die die Forscher als MICR-Überprüfung bezeichnen. Diese neuartige Schichttechnik rüstet ein vorhandenes System nach und extrahiert die Komponenten, die die Sicherheit erzwingen, in einen kleinen Kern, der überprüft wird und die Sicherheit des gesamten Systems garantiert.
Die Änderungen, die zur Nachrüstung eines großen Systems erforderlich sind, sind recht bescheiden. Die Forscher haben gezeigt, dass das System sicher ist und keine privaten Daten verloren gehen, wenn der kleine Kern des größeren Systems intakt ist. Auf diese Weise konnten sie ein großes System wie KVM verifizieren, was bisher für unmöglich gehalten wurde.
"Denken Sie an ein Haus - ein Riss in der Trockenbauwand bedeutet nicht, dass die Integrität des Hauses gefährdet ist", erklärte Nieh. "Es ist immer noch strukturell solide und das wichtige strukturelle System ist gut."
Shih-Wei Li, Niehs Ph.D. Der Student und Co-Hauptautor der Studie fügte hinzu: „SeKVM wird als Schutz in verschiedenen Bereichen dienen, von Bankensystemen und Geräten für das Internet der Dinge bis hin zu autonomen Fahrzeugen und Kryptowährungen.“
Als erster verifizierter Commodity-Hypervisor könnte SeKVM ändern, wie Cloud-Services entworfen, entwickelt, bereitgestellt und vertrauenswürdig sein sollten. In einer Welt, in der Internet-Sicherheit ist ein wachsendes Problem, diese Ausfallsicherheit ist sehr gefragt. Große Cloud-Unternehmen untersuchen bereits, wie sie SeKVM nutzen können, um diese Nachfrage zu befriedigen.