RISC-V-Stiftung über die Überprüfung des Betriebs des Mikrokernels auf Systemen mit RISC-V-Befehlssatzarchitektur. Auf die Überprüfung kommt es an Zuverlässigkeit des seL4-Betriebs, was die vollständige Einhaltung der in der formalen Sprache festgelegten Spezifikationen anzeigt. Nachweis der Zuverlässigkeit seL4 in geschäftskritischen Systemen auf Basis von RISC-V RV64-Prozessoren, die ein erhöhtes Maß an Zuverlässigkeit erfordern und die Abwesenheit von Ausfällen garantieren. Entwickler von Software, die auf dem seL4-Kernel läuft, können völlig sicher sein, dass sich ein Fehler in einem Teil des Systems nicht auf den Rest des Systems und insbesondere auf seine kritischen Teile ausbreitet.
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 durch die Kombination der offenen RISC-V-Hardwarearchitektur mit dem offenen seL4-Mikrokernel ein neues Sicherheitsniveau erreicht wird, da die Hardwarekomponenten künftig auch vollständig verifiziert werden können, was für proprietäre Hardwarearchitekturen nicht erreichbar ist.
Bei der Überprüfung von seL4 wird davon ausgegangen, dass das Gerät wie angegeben funktioniert und die Spezifikation das Verhalten des Systems vollständig beschreibt. In Wirklichkeit ist das Gerät jedoch nicht fehlerfrei, was durch regelmäßig auftretende Probleme im Mechanismus der spekulativen Ausführung deutlich wird Anweisungen. Offene Hardwareplattformen machen es einfacher, sicherheitsrelevante Änderungen zu integrieren – zum Beispiel, um alle möglichen Seitenkanallecks zu blockieren, wobei es viel effizienter ist, das Problem in der Hardware zu beseitigen, als zu versuchen, Workarounds in der Software zu finden.
Denken Sie daran, dass die seL4-Architektur Verschieben von Teilen zur Verwaltung von Kernel-Ressourcen in den Benutzerbereich und Anwenden der gleichen Zugriffskontrollmittel für solche Ressourcen wie für Benutzerressourcen. Der Mikrokernel stellt keine vorgefertigten High-Level-Abstraktionen für die Verwaltung von Dateien, Prozessen, Netzwerkverbindungen und dergleichen bereit; stattdessen stellt er nur minimale Mechanismen zur Steuerung des Zugriffs auf physischen Adressraum, Interrupts und Prozessorressourcen bereit. Abstraktionen auf hoher Ebene und Treiber für die Interaktion mit der Hardware werden separat auf dem Mikrokernel in Form von Aufgaben auf Benutzerebene implementiert. Der Zugriff solcher Aufgaben auf die dem Mikrokernel zur Verfügung stehenden Ressourcen wird durch die Definition von Regeln organisiert.
RISC-V bietet ein offenes und flexibles Maschinenanweisungssystem, mit dem Mikroprozessoren für beliebige Anwendungen gebaut werden können, ohne dass Lizenzgebühren oder Bedingungen für die Nutzung erforderlich sind. Mit RISC-V können Sie vollständig offene SoCs und Prozessoren erstellen. Derzeit basierend auf der RISC-V-Spezifikation von verschiedenen Unternehmen und Communities unter verschiedenen kostenlosen Lizenzen (BSD, MIT, Apache 2.0) mehrere Dutzend Varianten von Mikroprozessorkernen, SoCs und bereits produzierten Chips. RISC-V-Unterstützung gibt es seit den Veröffentlichungen von Glibc 2.27, Binutils 2.30, GCC 7 und dem Linux-Kernel 4.15.
Source: opennet.ru