Fraunhofer AISEC tritt seL4 Foundation bei und setzt auf formal verifizierten Mikrokernel
Das Fraunhofer-Institut für Angewandte und Integrierte Sicherheit AISEC ist der seL4 Foundation beigetreten. Damit will das Institut den Einsatz des formal verifizierten seL4-Mikrokernels als Grundlage für nachweisbar sichere IT-Systeme vorantreiben. Hintergrund ist die wachsende Bedrohungslage durch Agentic AI, mit deren Hilfe Angreifer Schwachstellen in Software zunehmend automatisiert finden und ausnutzen können. Ein erster Arbeitsschwerpunkt des Fraunhofer AISEC liegt auf virtuellen Maschinen und Confidential Computing. Perspektivisch untersucht das Institut zudem den Einsatz von seL4 auf der offenen Prozessorarchitektur RISC-V.
Wachsender Sicherheitsdruck durch Agentic AI
Software und Betriebssysteme bilden einen zentralen Bestandteil nahezu aller digitalen Systeme – von Industrieanlagen über Cloud-Dienste bis hin zu medizinischen Geräten und vernetzten Komponenten. Gleichzeitig wächst laut Fraunhofer AISEC der Druck, diese Systeme gegen gezielte Angriffe abzusichern: Neue Entwicklungen im Bereich Agentic AI ermöglichten es Angreifern, Software automatisiert zu analysieren, Schwachstellen schneller zu identifizieren und Angriffe gezielter vorzubereiten und durchzuführen. Vor diesem Hintergrund gewinnen Systeme an Bedeutung, deren Sicherheit sich nicht nur testen, sondern mathematisch nachweisen lässt. Genau hier setzt der Beitritt zur seL4 Foundation an: Das Institut nutzt den formal verifizierten seL4-Mikrokernel als Basis für robuste und vertrauenswürdige Systemarchitekturen, die unter anderem in kritischen Infrastrukturen, eingebetteten Systemen, der Medizintechnik und virtualisierten IT-Umgebungen zum Einsatz kommen sollen.
Formal verifizierter Mikrokernel als kleinere Angriffsfläche
Der seL4-Mikrokernel ist ein schlanker Betriebssystemkern, der sich auf grundlegende Funktionen wie Speicherverwaltung, Kommunikation zwischen Komponenten und Zugriffssteuerung beschränkt. Weitere Funktionen wie Gerätetreiber laufen getrennt vom Kernel in isolierten Bereichen des Systems. Ein Kernel verwaltet dabei die Hardware-Ressourcen – etwa CPU und Arbeitsspeicher – und ermöglicht Anwendungen kontrollierten Zugriff darauf, während Treiber die Eigenschaften physischer Geräte kapseln und dem Betriebssystem als standardisierte Schnittstelle zur Verfügung stellen.
Diese konsequente Funktionstrennung reduziert die Angriffsfläche und begrenzt mögliche Schäden im Fall eines erfolgreichen Angriffs. Aufgrund seiner geringen Größe lässt sich seL4 formal verifizieren – zentrale Sicherheitseigenschaften des Mikrokernels werden also mithilfe mathematischer Methoden nachgewiesen. Die Verifikation des Kernels erfolgt durch die seL4-Community; das Fraunhofer AISEC setzt darauf auf und erweitert das Ökosystem um Funktionen für Confidential Computing.
Schwerpunkt virtuelle Maschinen und Confidential Computing
Ein erster Arbeitsschwerpunkt des Instituts liegt auf virtuellen Maschinen (VMs) und Confidential Computing. VMs erlauben es, mehrere Betriebssysteme getrennt voneinander auf einem gemeinsamen physischen Rechner auszuführen, und gelten als zentraler Baustein moderner Cloud- und Rechenzentrumsinfrastrukturen. Technologien für Confidential Computing sollen Daten und Anwendungen innerhalb einer VM vor Zugriffen durch den Hypervisor oder den Betreiber der zugrunde liegenden Infrastruktur schützen. Dennoch bleiben Kommunikationsschnittstellen, Gerätetreiber und umfangreiche Betriebssystemkomponenten potenzielle Angriffspunkte – insbesondere bei großen Betriebssystemkernen kann eine Schwachstelle in einem Treiber weitreichende Folgen haben.
Das Fraunhofer AISEC hat den seL4-Mikrokernel so erweitert, dass er als Gastsystem in einer durch AMDs Technologie SEV-SNP geschützten VM lauffähig ist. SEV-SNP schützt den Speicher virtueller Maschinen kryptografisch und erschwert es Hypervisoren oder Rechenzentrumsbetreibern, auf darin verarbeitete Daten zuzugreifen. In der Referenzumgebung des Instituts – bestehend aus Linux-Host sowie der Virtualisierung QEMU/KVM – lassen sich bereits kleinere seL4-basierte Anwendungen ausführen. Auf dieser Basis entwickelt das Fraunhofer AISEC schrittweise vertrauenswürdige Plattformen für sichere virtualisierte Systeme, mit dem Ziel, die Vorteile von Virtualisierung und Confidential Computing mit einer deutlich kleineren, formal abgesicherten Vertrauensbasis zu verbinden.
Ausblick: RISC-V als offene Hardware-Basis
Darüber hinaus untersucht das Institut den Einsatz von seL4 auf der offenen Prozessorarchitektur RISC-V, die vor allem in eingebetteten und sicherheitskritischen Systemen zunehmend an Bedeutung gewinnt. Die Kombination aus einem formal verifizierten Mikrokernel und einer offenen Hardware-Architektur soll laut Fraunhofer AISEC die Grundlage für vertrauenswürdige Systeme bilden. Langfristiges Ziel ist es, auf Basis des seL4-Mikrokernels robuste Plattformen für sichere Systemarchitekturen in Cloud, Industrie und vernetzten Geräten aufzubauen.
Direkt zu Fraunhofer AISEC: Fraunhofer AISEC – Fraunhofer AISEC
Direkt zu seL4 Foundation: The seL4 Foundation | seL4
