Schwerpunkte

Open Source

Sicherer Mikrokernel seL4 für RISC-V

10. Juni 2020, 07:01 Uhr   |     

Sicherer Mikrokernel seL4 für RISC-V
© CSIRO, RISC-V International

Der sichere Open-Source-Mikrokernel seL4 wurde auf RISC-V implementiert.

Australische Wissenschaftler haben den sicheren Open-Source-Mikrokernel seL4 für die RISC-V-ISA impelementiert – und die Implementierung jetzt erfolgreich verifiziert. Ihre Arbeit wurde von einem deutschen Unternehmen bezahlt.

Data61, die Abteilung für Daten- und Digital-Spezialisten der nationalen Wissenschaftsagentur Australiens (CSIRO, Commonwealth Scientific and Industrial Research Organisation), hat die Implementierung des Open-Source-Mikrokernels seL4 für die RISC-V-Befehlssatzarchitektur (ISA, Instruction Set Architecture) abgeschlossen und die Korrektheit der Implementierung nachgewiesen. Damit steht Entwicklern, die mit RISC-V arbeiten, nun auch das sichere Open-Source-Betriebssystem seL4 zur Verfügung.

Dr. Rafal Kolanski, Leiter des Proof-Engineering-Teams der Forschungsgruppe »Vertrauenswürdige Systeme« von Data61: »Unser Ziel ist es, die Softwareindustrie weg von ad-hoc, unzuverlässigen technischen Praktiken und hin zu prinzipienbasierten Ansätzen auf der Grundlage mathematischer Prinzipien zu bewegen. Die Verifikation wird zur Standardwahl werden, wenn es um Sicherheit oder Gefahrenabwehr geht, und die Verifikation von seL4 auf der RISC-V-Architektur ist ein wichtiger Meilenstein“.

Das Betriebssystem seL4 wurde ursprünglich für 32-bit-ARM-Prozessoren verifiziert, die in allgegenwärtigen Mobilgeräten verwendet werden, und später für 64-bit-Intel-Prozessoren, die in PCs dominieren. Professor Gernot Heiser, Vorsitzender der seL4 Foundation: »Dieser Beweis macht die unübertroffene Sicherheit von seL4 für das am schnellsten wachsende Hardware-Wirtschaftsökosystem verfügbar, es deckt nun alle wichtigen Computerarchitekturen ab.«

Entwicklung mit deutscher Beteiligung

Marian Rachow, CEO Hensoldt Cyber
© Hensoldt Cyber

Marian Rachow, Geschäftsführer von Hensoldt Cyber: »Open Source für sichere Systeme wird die Kernstrategie von Hensoldt Cyber sein. Jetzt ist es wichtig, diese Techniken dem breiten Markt zugänglich zu machen. Unser SDK ‚Trentos-M‘, das auf dem seL4-Mikrokernel basiert, ist der erste Schritt zu einem sicheren Wirtschaftsökosystem«.

Die in Taufkirchen ansässige Hensoldt Cyber GmbH, ein als Sratup gegründetes Tochterunternhemen von Hensoldt, investierte in die RISC-V-Verifikation von seL4 um ihren eigenen, hochsicheren RISC-V-Prozessor zu ergänzen, der Verteidigungssysteme, smarte Fabriken, autonome Fahrzeuge und kritische Infrastrukturen vor Cyberangriffen schützen soll.

Marian Rachow, Geschäftsführer von Hensoldt Cyber: »Wir haben diese Arbeit finanziert, weil wir glauben, dass seL4 – als Open Source und der sicherste Mikrokernel – und RISC-V – als offene und sichere Prozessorarchitektur – die beste Grundlage für sichere Systeme sind«.

Krste Asanovic, Vorsitzende des Vorstands von RISC-V International, freut sich über den Erfolg: »Fortschritte in der Software- und Hardware-Standardisierung durch globale Zusammenarbeit und Konsens sowie die Open-Source-Entwicklung und Bereitstellung von Software- und Hardware-Entwicklungen haben den technischen Fortschritt in einem beispiellosen globalen Maßstab beschleunigt. Wir freuen uns darauf, die Annahme von seL4 in der globalen RISC-V-Gemeinschaft zu erleben«.

Auf Facebook teilenAuf Twitter teilenAuf Linkedin teilenVia Mail teilen

Verwandte Artikel

RISC-V Foundation