Fortschritte im Bereich Agentic AI erleichtern es Angreifern zunehmend, Schwachstellen in Software zu finden und auszunutzen. Das Fraunhofer-Institut für Angewandte und Integrierte Sicherheit AISEC tritt daher der seL4 Foundation bei und erforscht den Einsatz des formal verifizierten seL4-Mikrokernels als Grundlage für nachweisbar sichere Systeme. Ein erster Schwerpunkt liegt auf virtuellen Maschinen und Confidential Computing.

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.

Das Fraunhofer AISEC ist deshalb der seL4 Foundation beigetreten. Das Institut nutzt den formal verifizierten seL4-Mikrokernel als Basis und entwickelt darauf aufbauend robuste und vertrauenswürdige Systemarchitekturen. Diese 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.

Zur Erklärung: 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 standardisierte, 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.

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 dabei 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. Insbesondere bei großen Betriebssystemkernen kann eine Schwachstelle in einem Treiber oder einer anderen Kernel-Komponente 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 -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. Ziel ist es, die Vorteile von Virtualisierung und Confidential Computing mit einer deutlich kleineren formal abgesicherten Vertrauensbasis zu verbinden.

Weiterentwicklung in Richtung offener Prozessor-Architekturen

Darüber hinaus untersucht das Institut den Einsatz von seL4 auf der offenen Prozessorarchitektur RISC-V, die besonders in eingebetteten und sicherheitskritischen Systemen zunehmend an Bedeutung gewinnt. 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.