Der Mikro-Kernel seL4 ist mathematisch für die RISC-V-Architektur verifiziert.

Organisation der RISC-V Foundation berichtet zur Verifikation der Funktionalität des Mikro-Kernels seL4 auf Systemen mit RISC-V Befehlssatzarchitektur. Die Verifikation umfasst mathematische Beweise der Zuverlässigkeit von seL4, die die vollständige Übereinstimmung mit den formalen Spezifikationen bestätigt. Der Nachweis der Zuverlässigkeit ermöglicht den Einsatz von seL4 in sicherheitskritischen Systemen basierend auf RISC-V RV64-Prozessoren, die ein erhöhtes Maß an Zuverlässigkeit erfordern und Ausfälle garantieren. Entwickler von Software, die auf dem seL4-Kernel betrieben wird, können sich vollkommen darauf verlassen, dass im Falle eines Fehlers in einem Teil des Systems dieser Fehler nicht auf den Rest des Systems und insbesondere auf die kritischen Teile übergreift.

Ursprünglich wurde der Mikro-Kernel seL4 für 32-Bit ARM-Prozessoren verifiziert und später für 64-Bit x86-Prozessoren. Es wird festgestellt, dass die Kombination der offenen Hardware-Architektur RISC-V mit dem offenen Mikro-Kernel seL4 ein neues Sicherheitsniveau erreichen 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 angegeben funktioniert und die Spezifikation das Verhalten des Systems vollständig beschreibt. In der Praxis ist die Hardware jedoch nicht fehlerfrei, was durch regelmäßig auftretende Probleme im Mechanismus der spekulativen Ausführung von Anweisungen deutlich wird. Offene Hardwareplattformen erleichtern die Integration sicherheitsrelevanter Änderungen, beispielsweise zur Blockierung aller möglichen Leckkanäle durch externe Verbindungen, wo es oft effektiver ist, das Problem hardwareseitig zu lösen, als nach softwareseitigen Workarounds zu suchen.

Wir erinnern daran, dass die Architektur von seL4 zeichnet sich aus durch Durch die Auslagerung von Teilen des Kernel-Ressourcenmanagements in den Benutzermodus wird gewährleistet, dass für diese Ressourcen die gleichen Zugangskontrollmethoden wie für Benutzerressourcen angewendet werden. Das Mikro-Kernel bietet keine vorgefertigten hochrangigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw.; stattdessen stellt es lediglich minimale Mechanismen zum Zugriff auf den physischen Adressraum, Interrupts und CPU-Ressourcen bereit. Hochrangige Abstraktionen und Treiber für die Interaktion mit der Hardware werden separat über dem Mikro-Kernel in Form von Aufgaben, die im Benutzermodus ausgeführt werden, realisiert. 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 die Erstellung von Mikrochips für verschiedene Anwendungsbereiche ermöglicht, ohne dass Lizenzgebühren erforderlich sind oder Nutzungsbedingungen auferlegt werden. RISC-V erlaubt die Entwicklung vollständig offener SoCs und Prozessoren. Derzeit entwickeln verschiedene Unternehmen und Gemeinschaften auf Basis der RISC-V-Spezifikation unter verschiedenen freien Lizenzen (BSD, MIT, Apache 2.0) mehrere Dutzend Varianten von Mikroprozessor-Kernen, SoCs und bereits produzierten Chips. seit Sommer 2016). Bis Ende 2019 ist die Veröffentlichung einer weiteren experimentellen Version der GTK 3.9x-Reihe geplant, gefolgt von einem finalen Testrelease von GTK 3.99 im Frühling 2020, das alle angestrebten Funktionen enthalten wird. Die Veröffentlichung von GTK 4 wird für Anfang Herbst 2020 erwartet, zeitgleich mit GNOME 3.38. Die Unterstützung von RISC-V ist ab den Versionen von Glibc 2.27, binutils 2.30, gcc 7 und dem Linux-Kernel 4.15 vorhanden.

Quelle: opennet.ru