Die RISC-V Foundation gab bekannt, dass sie dies überprüft hat wie der Mikrokernel funktioniert seL4 in Systemen mit die Befehlssatzarchitektur RISC-V. Dabei wird der Verifizierungsprozess auf den mathematischen Nachweis der Zuverlässigkeit von seL4 reduziert, der die vollständige Einhaltung der in einer formalen Sprache angegebenen Spezifikationen anzeigt.
Durch Zuverlässigkeitstests kann seL4 in geschäftskritischen Systemen verwendet werden, die auf RISC-V-Prozessoren basieren RV64Dies erfordert ein höheres Maß an Zuverlässigkeit und garantiert keinen Ausfall.
Softwareentwickler, die auf dem seL4-Kernel ausgeführt werden, können absolut sicher sein, dass sich dieser Fehler im Falle eines Fehlers in einem Teil des Systems nicht auf den Rest des Systems und insbesondere auf seine kritischen Teile ausbreitet. .
Über seL4
Die seL4-Architektur eignet sich zum Entfernen von Teilen, um Kernelressourcen im Benutzerbereich zu verwalten und verwenden Sie für solche Ressourcen dieselben Zugriffssteuerungsmethoden wie für Benutzerressourcen.
Der Mikrokernel bietet keine Abstraktionen auf hoher Ebene bereits vorbereitet, um Dateien, Prozesse, Netzwerkverbindungen usw. zu verwalten, aber stattdessen bietet nur minimale Mechanismen zur Steuerung des Zugriffs auf den physischen Adressraum, Interrupts und Prozessorressourcen.
Übergeordnete Abstraktionen und Controller für die Interaktion mit dem Computer werden separat über dem Mikrokern in Form von Aufgaben implementiert, die auf Benutzerebene ausgeführt werden.
Der Zugriff solcher Aufgaben auf die im Mikrokernel verfügbaren Ressourcen wird durch die Definition von Regeln organisiert.
RISC-V bietet ein offenes und flexibles System von Maschinenanweisungen, die ermöglicht die Erstellung von Mikroprozessoren für beliebige Anwendungen, ohne dass Abzüge erforderlich sind und ohne Nutzungsbedingungen aufzuerlegen.
Mit RISC-V können Sie vollständig geöffnete SoCs und Prozessoren erstellen. Derzeit entwickeln auf der Grundlage der RISC-V-Spezifikation mehrere Unternehmen und Communities unter verschiedenen kostenlosen Lizenzen (BSD, MIT, Apache 2.0) mehrere Dutzend Varianten bereits produzierter Mikroprozessorkerne, SoCs und Chips.
RISC-V-Unterstützung gibt es seit der Veröffentlichung von Glibc 2.27, binutils 2.30, gcc 7 und dem Linux 4.15-Kernel.
Informationen zum Testen des seL4-Mikrokernels
Zunächst der Mikrokernel seL4 wurde für 32-Bit-ARM-Prozessoren verifiziertUnd später für x86 64-Bit-Prozessoren.
Es wird beobachtet, dass die Kombination der offenen RISC-V-Hardwarearchitektur mit dem offenen Mikrokernel seL4 wird ein neues Sicherheitsniveau erreichenda die Hardwarekomponenten in Zukunft auch vollständig verifiziert werden können, was für proprietäre Hardwarearchitekturen unmöglich zu erreichen ist.
Wenn wir seL4 überprüfen, müssen wir davon ausgehen, dass die Hardware ordnungsgemäß funktioniert (dh wie angegeben). Dies setzt voraus, dass es überhaupt eine eindeutige Spezifikation gibt, was nicht für alle Hardware der Fall ist.
Aber selbst wenn eine solche Spezifikation existiert und formal ist (dh in einem mathematischen Formalismus verankert ist, der das mathematische Denken über seine Eigenschaften unterstützt), woher wissen wir, dass sie tatsächlich das Verhalten der Hardware erfasst?
Die Realität ist, dass wir ziemlich sicher sein können, dass dies nicht der Fall ist. Hardware unterscheidet sich nicht von Software darin, dass beide fehlerhaft sind.
Ein offener ISA hat jedoch Vorteile, die über die Lizenzfreiheit hinausgehen. Zum einen ermöglicht es Open-Source-Hardware-Implementierungen.
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. Tatsächlich ist das Gerät jedoch nicht fehlerfrei, was durch Probleme, die regelmäßig im spekulativen Ausführungsmechanismus auftreten, gut belegt wird Anleitung.
Offene Hardwareplattformen vereinfachen die Integration von Änderungen im Zusammenhang mit der Sicherheit, zum Beispiel, um alle möglichen Leckkanäle über Kanäle von Drittanbietern zu blockieren, wo es viel effizienter ist, ein Problem durch Hardware zu beseitigen, als zu versuchen, Lösungen durch Software zu finden.
Wenn Sie mehr darüber erfahren möchten, können Sie den Hinweis in der folgenden Link
Für mich ist dieser Prozessor etwas, das mich sehr anruft. Es bleibt nur einem fetten Computerhund, einen Computer herzustellen, den wir kaufen können.
Das ARM-Problem ist etwas, das mich quietscht. Sie haben bereits gesehen, was mit Huawei mit den Sanktionen passiert ist. Ich bin mir sicher, dass mein RISC-V auf allen Ebenen eine viel bessere Lösung ist. Im Moment hat Huawei bereits ein Auge darauf geworfen und vielleicht werden sie in Zukunft Geräte mit diesem Mikro haben. Wenn ja, wird es sicherlich mehr Unternehmen geben, die es übernehmen, und für mich wäre das das Ideal und vor allem, dass die Distributionen Unterstützung bieten und nicht nur ARM, wie es bei den meisten passiert.
+10