Erweiterte Vertrauenswürdigkeit durch binäre Verifizierung des seL4®-Mikrokernels auf der RISC-V®-Prozessorarchitektur

**Taufkirchen,^5.

Mai 2021** - Das deutsche Cybersicherheitsunternehmen HENSOLDT Cyber hat in Zusammenarbeit mit CSIRO ein automatisiertes Tool für die binäre Verifikation des seL4-Mikrokerns in Bezug auf die 64-Bit RISC-V Prozessorarchitektur veröffentlicht.

"Der verifizierte seL4-Mikrokernel bildet die Grundlage von ^TRENTOS®

, dem sicheren Betriebssystem für MiG-V, einem RISC-V-Prozessor mit Supply Chain Security. Diese einzigartige Kombination aus Hardware- und Softwaresicherheit kann kritische IT-Systeme vor APTs schützen", so Sascha Kegreiß, CTO von HENSOLDT Cyber.

HENSOLDT Cyber erhöht die Vertrauenswürdigkeit dieser Hardware- und Softwarekombination, indem es in Zusammenarbeit mit CSIRO's Data61 mathematisch nachweist, dass der Binärcode des seL4-Mikrokerns die korrekte Übersetzung des Quellcodes ist. Diese Zuverlässigkeit wurde dadurch erreicht, dass sowohl der Binär- als auch der Quellcode in eine gemeinsame Zwischensprache abgebildet wurden, bevor die Äquivalenz mit automatischen Theorembeweisern überprüft wurde.

Durch die binäre Überprüfung entfällt die Notwendigkeit, dem eingesetzten Compiler zu vertrauen. Compiler können Fehler oder unbeabsichtigtes Verhalten einführen, die wiederum von Angreifern ausgenutzt werden können. Diese Fehler lassen sich durch die formale Verifikation des Quellcodes nicht erkennen; der Prozess muss daher auf den Binärcode ausgedehnt werden, um Fehler in der eingesetzten Software auszuschließen. Mit der binären Verifikation haben wir den Beweis, dass alles, was der Quellcode garantiert, auch für den Binärcode gilt, da die automatischen Theorembeweiser überprüft haben, dass sie tatsächlich äquivalent sind.

RISC-V ist die erste 64-Bit-Architektur, für die eine binäre Verifikation eines Betriebssystems erreicht wurde. Damit ist seL4 der erste vollständig formal verifizierte Kern für einen 64-Bit-Prozessor. Durch die Kombination einer offen zugänglichen und testbaren Prozessorarchitektur mit einem formal verifizierten Betriebssystemkern bietet seL4 auf RISC-V den bisher umfassendsten Sicherheitsansatz für einen Prozessor. Das Verfahren stellt sicher, dass der von der seL4-Gemeinschaft (organisiert in der seL4 Foundation) geschriebene und für korrekt befundene Programmcode fehlerfrei für die RISC-V-Architektur kompiliert wurde und somit als verifiziertes Binary zur Verfügung steht.

"Dies ist ein wichtiger Schritt, er stärkt die Position von seL4, den Stand der Technik bei sicheren Betriebssystemen zu definieren", sagte Prof. Gernot Heiser, Vorsitzender der seL4 Foundation.

Dr. Zoltan Kocsis, CSIRO-Verifizierungsingenieur, sagte: "Die Übersetzungsvalidierung verbindet alle unsere Verifizierungsbemühungen miteinander. Die Übertragung der Übersetzungsvalidierung auf einen modernen 64-Bit-Prozessor stellte uns vor erhebliche Herausforderungen in Bezug auf die Skalierbarkeit, die wir jedoch letztendlich meistern konnten."

Vertrauenswürdigkeit ist der zentrale Wert bei HENSOLDT Cyber, der sich in der Unternehmensvision "Sichere IT statt IT-Sicherheit" manifestiert. Sichere IT muss nachweislich sicher sein, dafür ist die binäre Verifikation von seL4 auf RISC-V ein wichtiger Schritt. HENSOLDT Cyber arbeitet gemeinsam mit seinen Partnern kontinuierlich daran, die einzelnen Komponenten seiner Lösungen auf ein noch nie dagewesenes Sicherheitsniveau zu heben, um seinen Kunden die daraus resultierenden Sicherheitsmerkmale einfach zur Verfügung stellen zu können.

Weitere Informationen über die MiG-V von HENSOLDT Cyber: https://hensoldt-cyber.com/mig-v

Über HENSOLDT Cyber

Die 2018 gegründete HENSOLDT Cyber GmbH ist ein deutsches Corporate Start-up-Unternehmen mit Sitz in Taufkirchen bei München, das eingebettete Informationstechnologieprodukte für höchste Sicherheitsanforderungen entwickelt. Diese integrieren ein hochsicheres Betriebssystem mit sicherheitsgehärteter Hardware und schaffen so eine sichere IT anstelle von IT-Sicherheit für den globalen IT-Markt. Das Unternehmen vereint mehr als 50 Jahre Erfahrung in der Verteidigungs- und Sicherheitselektronik der HENSOLDT-Gruppe mit akademischer Weltklasse-Expertise in der Hard- und Softwareentwicklung. HENSOLDT Cyber beschäftigt derzeit über 50 Mitarbeiter an verschiedenen Standorten.

Weitere Informationen über das Unternehmen finden Sie unter www.hensoldt-cyber.com.

Kontakt für Presseanfragen, Bilder und Artikelanfragen

Simone Rudow

Leiterin Marketing & PR

Tel.: +49 (0) 174 218 8102

simone.rudow@hensoldt-cyber.com