Das Mikro-Kernel seL4 wurde mathematisch für die RISC-V-Architektur verifiziert.

RISC-V Foundation meldete zur Verifizierung der Funktionsweise des Mikro-Kernels seL4 auf Systemen mit RISC-V-Befehlssatzarchitektur. Die Verifizierung reduziert sich auf mathematische Beweise der Zuverlässigkeit von seL4, die die vollständige Übereinstimmung mit den in formaler Sprache spezifizierten Anforderungen belegen. Der Nachweis der Zuverlässigkeit erlaubt die Nutzung von seL4 in sicherheitskritischen Systemen auf Basis von RISC-V RV64-Prozessoren, die ein höheres Maß an Zuverlässigkeit erfordern und Ausfälle garantieren. Softwareentwickler, die auf dem seL4-Kernel basierende Anwendungen entwickeln, können sich sicher sein, dass ein Fehler in einem Teil des Systems sich nicht auf den Rest des Systems und insbesondere auf dessen kritische Komponenten ausbreitet.

Ursprünglich wurde das Mikro-Kernel seL4 für 32-Bit-ARM-Prozessoren verifiziert und später für 64-Bit-x86-Prozessoren. Es wird angemerkt, dass die Kombination der offenen Hardwarearchitektur RISC-V mit dem offenen Mikro-Kernel seL4 ein neues Sicherheitsniveau ermöglichen wird, da auch die Hardwarekomponenten in der Zukunft vollständig verifiziert werden können, was bei proprietären Hardwarearchitekturen nicht möglich ist.

Bei der Verifizierung von seL4 wird davon ausgegangen, dass die Hardware wie angekündigt funktioniert und die Spezifikation das Verhalten des Systems vollständig beschreibt, in der Praxis ist die Hardware jedoch nicht fehlerfrei, was gut durch regelmäßig auftretende Probleme im Mechanismus der spekulativen Ausführung von Instruktionen demonstriert wird. Offene Hardwareplattformen erleichtern die Integration sicherheitsbezogener Änderungen – zum Beispiel zur Blockierung aller möglichen Seitenkanäle für Datenlecks, wobei es viel effektiver ist, das Problem hardwareseitig zu beheben, als softwareseitig nach Lösungen zu suchen.

Wir erinnern daran, dass die Architektur seL4 ist bemerkenswert Die Auslagerung von Teilen zur Verwaltung der Ressourcen des Kernels in den Benutzerspeicher und die Anwendung der gleichen Zugriffskontrollmittel wie für Benutzerressourcen. Das Mikro-Kernel bietet keine sofort einsatzbereiten hochrangigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw., sondern bietet lediglich minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Interrupts und CPU-Ressourcen. Hochrangige Abstraktionen und Treiber zur Interaktion mit der Hardware werden separat über dem Mikro-Kernel in Form von Aufgaben implementiert, die auf Benutzerebene ausgeführt werden. Der Zugang dieser Aufgaben zu den Ressourcen des Mikro-Kernels wird durch die Festlegung von Regeln organisiert.

RISC-V bietet ein offenes und flexibles System von Maschineninstruktionen, das es ermöglicht, Mikroprozessoren für beliebige Anwendungsbereiche zu erstellen, ohne dafür Abgaben zu verlangen oder Bedingungen für die Nutzung auferlegt werden. RISC-V ermöglicht die Erstellung von vollständig offenen SoCs und Prozessoren. Derzeit basierend auf der Spezifikation RISC-V gibt es verschiedene Unternehmen und Gemeinschaften, die unter verschiedenen Open-Source-Lizenzen (BSD, MIT, Apache 2.0) entwickelt sich mehrere Dutzend Varianten von Mikroprozessor-Kernen, SoCs und bereits produzierten Chips. Die Unterstützung von RISC-V ist seit den Versionen Glibc 2.27, binutils 2.30, gcc 7 und dem Linux-Kernel 4.15 vorhanden.

Quelle: opennet.ru