Ein erster Schwerpunkt liegt auf virtuellen Maschinen und Confidential Computing. Kombination aus einem formal verifizierten Mikrokernel und offener Hardware-Architektur…
Hintergrund
Fortschritte im Bereich Agentic AI erleichtern es Angreifern zunehmend, Schwachstellen in Software zu finden und auszunutzen. Kommunikationsschnittstellen, Gerätetreiber und umfangreiche Betriebssystemkomponenten stellen potenzielle Angriffspunkte dar. Insbesondere bei großen Betriebssystemkernen können Schwachstellen in einem Treiber oder einer anderen Kernel-Komponente weitreichende Folgen haben. Das Fraunhofer AISEC ist deshalb der seL4 Foundation beigetreten. Das Institut nutzt dazu den formal verifizierten seL4-Mikrokernel als Basis und entwickelt darauf aufbauend robuste und vertrauenswürdige Systemarchitekturen.
Weitere Informationen (Quelle: AISEC)
„Software und insbesondere Betriebssysteme sind ein zentraler Teil nahezu aller digitalen Systeme – von Industrieanlagen und Cloud-Diensten bis zu medizinischen Geräten und vernetzten Komponenten. Gleichzeitig steigt der Druck, diese Systeme vor gezielten Angriffen zu schützen: Durch neue Entwicklungen im Bereich Agentic AI können Angreifer Software zunehmend automatisiert analysieren, Schwachstellen schneller identifizieren und Angriffe gezielter vorbereiten und automatisiert durchführen.
Umso wichtiger werden Systeme, deren Sicherheit nicht nur getestet, sondern mathematisch nachgewiesen werden kann. Robuste und vertrauenswürdige Systemarchitekturen können insbesondere in kritischen Infrastrukturen, eingebetteten Systemen, der Medizintechnik und virtualisierten IT-Umgebungen eingesetzt werden.
Formal verifizierter Mikrokernel als kleinere Angriffsfläche
Der seL4-Mikrokernel ist ein besonders schlanker Betriebssystemkern. Er beschränkt sich auf grundlegende Funktionen wie Speicherverwaltung, Kommunikation zwischen Komponenten und Zugriffssteuerung. Weitere Funktionen, etwa Gerätetreiber, laufen getrennt vom Kernel in isolierten Bereichen des Systems.
Anmerkung: Ein Kernel verwaltet die Ressourcen von Hardware (bspw. CPU, Arbeitsspeicher) und ermöglicht Anwendungen kontrollierten Zugriff darauf. Treiber kapseln die spezifischen Hardware-Eigenschaften eines physischen Geräts und stellen sie dem Betriebssystem als hardwareunabhängige Schnittstelle (API) zur Verfügung. Diese konsequente Funktionstrennung reduziert die Angriffsfläche und begrenzt mögliche Schäden bei einem erfolgreichen Angriff.
Aufgrund seiner geringen Größe kann seL4 formal verifiziert werden. Das bedeutet: Zentrale Sicherheitseigenschaften des Mikrokernels werden mithilfe mathematischer Methoden nachgewiesen. seL4 bietet damit eine Grundlage für Systeme, bei denen hohe Anforderungen an Sicherheit, Zuverlässigkeit und Nachvollziehbarkeit bestehen. 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.
Abb.1: Die folgende Abbildung zeigt eine der Anwendungsmöglichkeiten von seL4: die Isolierung zwischen vertrauenswürdigen und nicht vertrauenswürdigen Komponenten in einem System, einschließlich vollständiger virtueller Maschinen (Bildquelle: seL4 white paper, What is seL4?)
Externer Link > https://sel4.systems/
Fokus auf virtuelle Maschinen und Confidential Computing
Ein erster Schwerpunkt der Arbeiten des Fraunhofer AISEC liegt auf virtuellen Maschinen (VMs) und Confidential Computing. VMs ermöglichen es, mehrere Betriebssysteme voneinander getrennt auf einem gemeinsamen, physischen Rechner auszuführen. Sie sind ein zentraler Baustein moderner Cloud- und Rechenzentrumsinfrastrukturen.
Technologien für Confidential Computing schützen Daten und Anwendungen innerhalb einer VM vor Zugriffen durch den Hypervisor – einer Software, die mehrere VMs verwaltet – oder den Betreiber der zugrunde liegenden Infrastruktur. Dennoch bleiben Kommunikationsschnittstellen, Gerätetreiber und umfangreiche Betriebssystemkomponenten potenzielle Angriffspunkte.
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 -Virtualisierung QEMU/KVM – lassen sich danch bereits kleinere seL4-basierte Anwendungen ausführen.
Auf dieser Basis entwickelt das Fraunhofer AISEC schrittweise vertrauenswürdige Plattformen für sichere virtualisierte Systeme. Ziel ist es, die Vorteile von Virtualisierung und Confidential Computing mit einer deutlich kleineren formal abgesicherten Vertrauensbasis zu verbinden.
** Quelle / externer Link > https://www.amd.com/de/developer/sev.html
Weiterentwicklung in Richtung offener Prozessor-Architekturen
Darüber hinaus untersucht das Institut nach vorliegenden Angaben den Einsatz von seL4 auf der offenen Prozessorarchitektur RISC-V, die besonders in eingebetteten und sicherheitskritischen Systemen zunehmend an Bedeutung gewinnt."
Fazit
Die Kombination aus einem formal verifizierten Mikrokernel und einer offenen Hardware-Architektur bietet die Grundlage für vertrauenswürdige Systeme. Ziel ist es, auf Basis des seL4-Mikrokernels robuste, vertrauenswürdige Plattformen für sichere Systemarchitekturen in der Cloud, der Industrie und vernetzten Geräten aufzubauen.
Stand 7. Sept. 2026.
Querverweis:
Unser Beitrag > Memory Centric Storage MCSS: Fraunhofer ITWM zeigt neues Storagesystem erstmals auf ISC 2025
Unser Beitrag > Bayern fördert generative KI mit 30 Millionen Euro
Unser Beitrag > IBM und Red Hat starten Lightwell Network: Sicherheitslücken in Open-Source-Software schneller beheben