{"id":31922,"date":"2026-09-09T13:44:46","date_gmt":"2026-09-09T11:44:46","guid":{"rendered":"https:\/\/www.sysbus.eu\/?p=31922"},"modified":"2026-09-02T13:53:30","modified_gmt":"2026-09-02T11:53:30","slug":"fraunhofer-aisec-tritt-sel4-foundation-bei-und-setzt-auf-formal-verifizierten-mikrokernel","status":"publish","type":"post","link":"https:\/\/www.sysbus.eu\/?p=31922","title":{"rendered":"Fraunhofer AISEC tritt seL4 Foundation bei und setzt auf formal verifizierten Mikrokernel"},"content":{"rendered":"\n

Das Fraunhofer-Institut f\u00fcr Angewandte und Integrierte Sicherheit AISEC ist der seL4 Foundation beigetreten. Damit will das Institut den Einsatz des formal verifizierten seL4-Mikrokernels als Grundlage f\u00fcr 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\u00f6nnen. 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.<\/p>\n\n\n\n

\"\"
Quelle: Fraunhofer AISEC\/Magnific<\/figcaption><\/figure>\n\n\n\n

Wachsender Sicherheitsdruck durch Agentic AI<\/p>\n\n\n\n

Software und Betriebssysteme bilden einen zentralen Bestandteil nahezu aller digitalen Systeme \u2013 von Industrieanlagen \u00fcber Cloud-Dienste bis hin zu medizinischen Ger\u00e4ten und vernetzten Komponenten. Gleichzeitig w\u00e4chst laut Fraunhofer AISEC der Druck, diese Systeme gegen gezielte Angriffe abzusichern: Neue Entwicklungen im Bereich Agentic AI erm\u00f6glichten es Angreifern, Software automatisiert zu analysieren, Schwachstellen schneller zu identifizieren und Angriffe gezielter vorzubereiten und durchzuf\u00fchren. Vor diesem Hintergrund gewinnen Systeme an Bedeutung, deren Sicherheit sich nicht nur testen, sondern mathematisch nachweisen l\u00e4sst. Genau hier setzt der Beitritt zur seL4 Foundation an: Das Institut nutzt den formal verifizierten seL4-Mikrokernel als Basis f\u00fcr robuste und vertrauensw\u00fcrdige Systemarchitekturen, die unter anderem in kritischen Infrastrukturen, eingebetteten Systemen, der Medizintechnik und virtualisierten IT-Umgebungen zum Einsatz kommen sollen.<\/p>\n\n\n\n

Formal verifizierter Mikrokernel als kleinere Angriffsfl\u00e4che<\/p>\n\n\n\n

Der seL4-Mikrokernel ist ein schlanker Betriebssystemkern, der sich auf grundlegende Funktionen wie Speicherverwaltung, Kommunikation zwischen Komponenten und Zugriffssteuerung beschr\u00e4nkt. Weitere Funktionen wie Ger\u00e4tetreiber laufen getrennt vom Kernel in isolierten Bereichen des Systems. Ein Kernel verwaltet dabei die Hardware-Ressourcen \u2013 etwa CPU und Arbeitsspeicher \u2013 und erm\u00f6glicht Anwendungen kontrollierten Zugriff darauf, w\u00e4hrend Treiber die Eigenschaften physischer Ger\u00e4te kapseln und dem Betriebssystem als standardisierte Schnittstelle zur Verf\u00fcgung stellen.<\/p>\n\n\n\n

Diese konsequente Funktionstrennung reduziert die Angriffsfl\u00e4che und begrenzt m\u00f6gliche Sch\u00e4den im Fall eines erfolgreichen Angriffs. Aufgrund seiner geringen Gr\u00f6\u00dfe l\u00e4sst sich seL4 formal verifizieren \u2013 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 \u00d6kosystem um Funktionen f\u00fcr Confidential Computing.<\/p>\n\n\n\n

Schwerpunkt virtuelle Maschinen und Confidential Computing<\/p>\n\n\n\n

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\u00fchren, und gelten als zentraler Baustein moderner Cloud- und Rechenzentrumsinfrastrukturen. Technologien f\u00fcr Confidential Computing sollen Daten und Anwendungen innerhalb einer VM vor Zugriffen durch den Hypervisor oder den Betreiber der zugrunde liegenden Infrastruktur sch\u00fctzen. Dennoch bleiben Kommunikationsschnittstellen, Ger\u00e4tetreiber und umfangreiche Betriebssystemkomponenten potenzielle Angriffspunkte \u2013 insbesondere bei gro\u00dfen Betriebssystemkernen kann eine Schwachstelle in einem Treiber weitreichende Folgen haben.<\/p>\n\n\n\n

Das Fraunhofer AISEC hat den seL4-Mikrokernel so erweitert, dass er als Gastsystem in einer durch AMDs Technologie SEV-SNP gesch\u00fctzten VM lauff\u00e4hig ist. SEV-SNP sch\u00fctzt den Speicher virtueller Maschinen kryptografisch und erschwert es Hypervisoren oder Rechenzentrumsbetreibern, auf darin verarbeitete Daten zuzugreifen. In der Referenzumgebung des Instituts \u2013 bestehend aus Linux-Host sowie der Virtualisierung QEMU\/KVM \u2013 lassen sich bereits kleinere seL4-basierte Anwendungen ausf\u00fchren. Auf dieser Basis entwickelt das Fraunhofer AISEC schrittweise vertrauensw\u00fcrdige Plattformen f\u00fcr sichere virtualisierte Systeme, mit dem Ziel, die Vorteile von Virtualisierung und Confidential Computing mit einer deutlich kleineren, formal abgesicherten Vertrauensbasis zu verbinden.<\/p>\n\n\n\n

Ausblick: RISC-V als offene Hardware-Basis<\/p>\n\n\n\n

Dar\u00fcber 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\u00fcr vertrauensw\u00fcrdige Systeme bilden. Langfristiges Ziel ist es, auf Basis des seL4-Mikrokernels robuste Plattformen f\u00fcr sichere Systemarchitekturen in Cloud, Industrie und vernetzten Ger\u00e4ten aufzubauen.

Direkt zu Fraunhofer AISEC: Fraunhofer AISEC – Fraunhofer AISEC<\/a>
Direkt zu seL4 Foundation: The seL4 Foundation | seL4<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

Das Fraunhofer-Institut f\u00fcr Angewandte und Integrierte Sicherheit AISEC ist der seL4 Foundation beigetreten. Damit will das Institut den Einsatz des formal verifizierten seL4-Mikrokernels als Grundlage f\u00fcr 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\u00f6nnen. 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.<\/p>\n","protected":false},"author":82,"featured_media":31924,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"colormag_page_container_layout":"default_layout","colormag_page_sidebar_layout":"default_layout","footnotes":""},"categories":[10036,4,37],"tags":[24459,26664,21120,26666,26665],"class_list":["post-31922","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-kuenstliche-intelligenz","category-news","category-security","tag-confidentialcomputing","tag-fraunhoferaisec","tag-itsicherheit","tag-riscv","tag-sel4"],"amp_enabled":true,"_links":{"self":[{"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/posts\/31922","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/users\/82"}],"replies":[{"embeddable":true,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=31922"}],"version-history":[{"count":1,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/posts\/31922\/revisions"}],"predecessor-version":[{"id":31926,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/posts\/31922\/revisions\/31926"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=\/wp\/v2\/media\/31924"}],"wp:attachment":[{"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=31922"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=31922"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.sysbus.eu\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=31922"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}