Der seL4-Mikrokernel ist mathematisch für die RISC-V-Architektur verifiziert

RISC-V-Stiftung berichtet zur Überprüfung des Mikrokernelbetriebs seL4 auf Systemen mit RISC-V-Befehlssatzarchitektur. Die Verifizierung läuft darauf hinaus, mathematischer Beweis Zuverlässigkeit des seL4-Betriebs, was auf die vollständige Einhaltung der in der formalen Sprache angegebenen Spezifikationen hinweist. Nachweis der Zuverlässigkeit erlaubt Ihnen zu verwenden seL4 in unternehmenskritischen Systemen auf Basis von RISC-V RV64-Prozessoren, die eine erhöhte Zuverlässigkeit erfordern und die Abwesenheit von Fehlern garantieren. Entwickler von Software, die auf dem seL4-Kernel läuft, können absolut sicher sein, dass sich der Ausfall eines Teils des Systems nicht auf den Rest des Systems und insbesondere nicht auf seine kritischen Teile ausweitet.

Der seL4-Mikrokernel wurde zunächst für 32-Bit-ARM-Prozessoren und später für 64-Bit-x86-Prozessoren verifiziert. Es wird darauf hingewiesen, dass die Kombination der offenen RISC-V-Hardwarearchitektur mit dem offenen seL4-Mikrokernel das Erreichen eines neuen Sicherheitsniveaus ermöglicht, da die Hardwarekomponenten in Zukunft auch vollständig verifiziert werden können, was für proprietäre Hardwarearchitekturen nicht möglich ist.

Bei der Überprüfung von seL4 wird davon ausgegangen, dass die Hardware wie angekündigt funktioniert und die Spezifikation das Systemverhalten vollständig beschreibt. In Wirklichkeit ist die Hardware jedoch nicht fehlerfrei, was durch regelmäßig auftretende Probleme im spekulativen Ausführungsmechanismus deutlich wird. Offene Hardwareplattformen erleichtern die Integration sicherheitsrelevanter Änderungen – zum Beispiel das Blockieren aller möglichen Seitenkanallecks, wobei es viel effektiver ist, das Problem in der Hardware zu beheben, als zu versuchen, Workarounds in der Software zu finden.

Erinnern wir uns daran, dass die Architektur von seL4 bemerkenswert indem die Teile zur Verwaltung der Kernelressourcen in den Benutzerbereich verschoben werden und für diese Ressourcen dieselben Zugriffskontrolltools wie für Benutzerressourcen angewendet werden. Der Mikrokernel bietet keine vorgefertigten Abstraktionen auf hoher Ebene zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw., sondern nur minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Interrupts und Prozessorressourcen. Abstraktionen auf hoher Ebene und Treiber für die Interaktion mit der Hardware werden separat auf dem Mikrokernel in Form von Aufgaben implementiert, die auf Benutzerebene ausgeführt werden. Der Zugriff solcher Aufgaben auf die dem Mikrokernel zur Verfügung stehenden Ressourcen wird durch die Definition von Regeln organisiert.

RISC-V bietet einen offenen und flexiblen Maschinenbefehlssatz, der die Entwicklung von Mikroprozessoren für beliebige Anwendungsbereiche ermöglicht, ohne dass Lizenzgebühren oder Nutzungsbedingungen erforderlich sind. RISC-V ermöglicht die Erstellung vollständig offener SoCs und Prozessoren. Derzeit basierend auf der RISC-V-Spezifikation verschiedener Unternehmen und Communities unter verschiedenen freien Lizenzen (BSD, MIT, Apache 2.0) entwickelt sich Mehrere Dutzend Varianten von Mikroprozessorkernen, SoCs und Chips sind bereits in Produktion. RISC-V-Unterstützung ist seit den Veröffentlichungen von Glibc 2.27, binutils 2.30, gcc 7 und dem Kernel vorhanden. Linux 4.15

Source: opennet.ru