Taufkirchen, 5. Mai 2021 – Das deutsche Cybersicherheits-Unternehmen HENSOLDT Cyber gibt gemeinsam mit seinem Partner CSIRO die Veröffentlichung eines automatischen Tools zur binären Verifikation des seL4-Mikrokerns für die 64-Bit RISC-V-Prozessorarchitektur bekannt.
„Der verifizierte seL4-Mikrokern bildet die Basis von TRENTOS®, des sicheren Betriebssystems 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", sagt Sascha Kegreiß, CTO von HENSOLDT Cyber.
HENSOLDT Cyber erhöht die Vertrauenswürdigkeit dieser Hardware- und Software-Kombination, indem sie in Zusammenarbeit mit CSIRO’s Data61 mathematisch beweisen, dass der Binärcode des seL4-Mikrokerns die korrekte Übersetzung seines Quellcodes ist. Diese Zuverlässigkeit wurde erreicht, indem sowohl der Binär- als auch der Quellcode in eine einheitliche Zwischensprache abgebildet wurden, bevor die Äquivalenz mit automatischen Theorembeweisern überprüft wurde.
Durch die binäre Verifikation muss dem eingesetzten Compiler nicht mehr vertraut werden. Eingesetzte Compiler können die Quelle für Fehler oder unbeabsichtigtes Verhalten darstellen, welche wiederum von Hackern ausgenutzt werden, um Angriffe durchzuführen. Diese Fehler sind durch die formale Verifikation des Quellcodes nicht identifizierbar, das Verfahren muss auch den Binärcode betrachten, um Fehler in der eingesetzten Software auszuschließen. Mit der binären Verifikation haben wir den Beweis, dass alles, was durch den Quellcode garantiert wird, auch für den Binärcode gilt, da die automatischen Theorembeweiser geprü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 von offen verfügbarer und prüfbarer Prozessorarchitektur und einem formal verifizierten Betriebssystemkern bietet RISC-V mit seL4 das umfassendste Sicherheitskonzept, das bisher von einem Prozessor erreicht wurde. Das Verfahren stellt sicher, dass der von der seL4 Community (organisiert in der seL4 Foundation) geschriebene, bewiesenermaßen korrekte 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 als den Stand der Technik bei sicheren Betriebssystemen definierend", sagte Prof. Gernot Heiser, Vorsitzender der seL4 Foundation.
Dr. Zoltan Kocsis, CSIRO Verifikationsingenieur, bestätigt: „Die Übersetzungsüberprüfung bringt alle unsere Verifikationserrungenschaften zusammen. Ein moderner 64-Bit-Prozessor erzeugt hierbei erhebliche Skalierbarkeitsprobleme, die wir aber schlussendlich meistern konnten."
Vertrauenswürdigkeit ist die Kernaussage von HENSOLDT Cyber, welche sich in der Unternehmensvision "Sichere IT statt IT-Sicherheit" manifestiert. Sichere IT muss nachweisbar sicher sein; hierfür stellt die Binärverifikation des seL4 auf RISC-V einen wichtigen Schritt dar. HENSOLDT Cyber arbeitet mit seinen Partnern stetig daran, die einzelnen Komponenten seiner Lösungen auf bisher unerreichte Sicherheitsniveaus zu heben, um somit seinen Kunden, die sich daraus ergebenden Sicherheitseigenschaften einfach zur Verfügung stellen zu können.
Für weitere Informationen über das 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 Informationstechnologie-Produkte 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 kombiniert 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
Head of Marketing & PR
Tel.: +49 (0) 174 218 8102
simone.rudow@hensoldt-cyber.com