VerSeCloud: Der Weg zu einer vertrauenswürdigen, sicheren Cloud

Wie kann eine sichere, vertrauenswürdige und dazu zukunftsfähige Cloud aussehen? Eine Lösung will das Forschungsprojekt VerSeCloud liefern. Mittels eines Mikrokernel, formalen Beweismethoden und strikt durchgesetzter Trennung zwischen Kundenanwendungen entwickeln die Konsortialpartner, die Kernkonzept GmbH, die genua GmbH, die Universität Potsdam sowie die Technische Universität München Grundlagen für eine hochsichere Cloud-Infrastruktur. 

von Nicolas Frinker, Software Engineer bei genua

Virtualisierung als Basis für Cloudlösungen ist in der heutigen IT-Infrastruktur zu einem zentralen Baustein geworden. Die damit einhergehende Abstraktion existierender physischer Ressourcen in eine virtuelle Umgebung erlaubt deren flexible, skalierbare und kosteneffiziente Nutzung. 

Sensible Daten und Anwendungen erfordern jedoch ein hohes Maß an Datensicherheit und Vertrauenswürdigkeit, die von aktuellen Virtualisierungslösungen nicht geboten werden können: Aktuelle Lösungen sind aufgrund ihrer zugrunde liegenden Betriebssysteme komplex und umfangreich und lassen sich damit kaum auf verlässliche Sicherheit prüfen. Eine Zulassung oder Zertifizierung ist so nur mit sehr großem Aufwand überhaupt denkbar. 

Im Forschungsprojekt VerSeCloud arbeiten wir zusammen mit unseren Projektpartnern, der Kernkonzept GmbH aus Dresden, der Universität Potsdam und derTechnischen Universität München, an einer zukunftsfähigen, verlässlichen und sicheren Virtualisierungslösung auch für sicherheitskritische Cloudanwendungen. 

Cloudanwendungen: Schlank und verifizierbar

Auf Basis des L4Re-Mikrokernels entwickeln wir einen, dank Intel Vt-x performanten und flexiblen Hypervisor, der Linux und OpenBSD unmodifiziert ausführen kann. Mittels Nested Virtualization werden auch weitere Betriebssysteme wie MS Windows lauffähig. Durch die Mikrokernel-Basis bleibt dabei die Codebasis schlank und nachvollziehbar. Der mit Systemrechten laufende L4Re-Mikrokernel ist dabei nur für die grundlegendsten Aufgaben wie die Separation der Anwendungen zuständig. Alle anderen Aufgaben werden ausgelagert und nur mit eingeschränkten Zugriffsrechten ausgeführt. Mit dieser Architektur bleiben die sicherheitsrelevanten Komponenten schlank und verifizierbar und eignen sich so auch für tiefergehende Reviews, z. B. in einem Zulassungsprozess. 

Neben der soliden und sicheren technischen Basis werden im Forschungsprojekt VerSeCloud formale Methoden eingesetzt, um Sicherheitseigenschaften des Mikrokernels und der Treiber mathematisch zu beweisen. Mithilfe eines abstrakten Modells des L4Re-Mikrokernels wird ein erwarteter Zustand definiert, der dann durch eine sehr große Zahl automatisch generierter Tests mit dem tatsächlichen Zustand in der Implementierung verglichen wird. Für die Treiber werden im Projekt insbesondere Netzwerktreiber näher betrachtet, gemeinsame Eigenschaften ermittelt und diese in das Beweissystem Coq überführt. Dort kann deren Korrektheit bewiesen und Code synthetisiert werden, der dann Teile des Treibers mit bewiesenermaßen korrektem Code ersetzen kann. Dieser Einsatz von formalen Methoden erhöht die Sicherheit signifikant. 

Vier Fragen an Nicolas Frinker

Ist umfassende IT-Security und Datenschutz in einer Cloudumgebung, in der mit vielen verschiedenen Geräten und auch mobil auf Daten zugegriffen wird, überhaupt möglich?

Nicolas Frinker: IT-Security und Datenschutz in einer Cloudumgebung hängen von zwei Faktoren ab: Dem Anbieter und der eingesetzten Technik bzw. Software. Die eingesetzte Technik muss sicherstellen, dass Kunden in der Cloudumgebung sicher und zuverlässig voneinander separiert werden. Der vertrauenswürdige Anbieter wiederum muss sicherstellen, dass diese Technik auch konsequent eingesetzt wird. Trifft beides zusammen, sind Kundenanwendungen und -daten gut geschützt.

Was wären mögliche Anwendungsszenarien?

Nicolas Frinker: Die aktuell großen Cloud-Anbieter sitzen meist in den USA und genießen nicht unbedingt das Vertrauen vieler deutscher Firmen. Diesen fehlt somit der vertrauenswürdige Anbieter und auch die eingesetzte Software fällt immer wieder durch Sicherheitsprobleme auf.

Um den fehlenden, vertrauenswürdigen Cloud-Anbieter zu ersetzen, greifen viele Firmen auf selbstgehostete Clouds zurück, sogenannte Private Clouds. Dabei steht das Rechenzentrum "im eigenen Keller" und wird exklusiv von dieser jeweiligen Firma genutzt, sodass auch keine softwarebasierte Separation von mehreren Kunden mehr notwendig ist. Damit ist diese Lösung zwar sicher, gleichzeitig verliert man aber die wesentlichen Vorteile einer Public Cloud wie Skalierbarkeit und Kosteneffizienz.

Hier kann VerSeCloud die Grundlagen für eine vielversprechende Zukunft bieten: Eine Cloudumgebung auf Basis der in VerSeCloud erforschten Software mit ihren formal bewiesenen Sicherheitseigenschaften bietet die notwendige, sichere technische Basis, auf der sich mehrere Kunden die gleiche Cloudumgebung teilen können, ohne dabei um ihre Separation von anderen Kunden fürchten zu müssen. Wird diese Software dann auch noch von einem vertrauenswürdigen Cloudanbieter betrieben, sind Sicherheit und Datenschutz kosteneffizient und skalierbar möglich!

Wie ist das Projekt im Team aufgeteilt?

Nicolas Frinker: Im Wesentlichen forschen Kernkonzept und genua zusammen daran, den neuen Hypervisor zu verbessern, während Kernkonzept zusammen mit der Universität Potsdam mittels formaler Verifikation Sicherheitseigenschaften zu beweisen versucht. Meine Hauptaufgabe besteht darin, OpenBSD neben Linux als weiteres Gastsystem auf dem neuen Hypervisor lauffähig zu machen.

Welche Fortschritte wurden bereits gemacht?

Nicolas Frinker: Der neue Hypervisor ist mittlerweile ordentlich gereift und kann Linux und OpenBSD als Gastsysteme ausführen. Auch an der formalen Methoden-Front gibt es schon jede Menge Forschritte: So wurde beispielsweise ein kompletter, einfacher Treiber für L4Re aus dem Beweissystem Coq heraus synthetisiert.