Google hat die Entdeckung von Entwicklungen im Zusammenhang mit dem KataOS-Projekt bekannt gegeben, das darauf abzielt, ein sicheres Betriebssystem für eingebettete Hardware zu schaffen. KataOS-Systemkomponenten sind in Rust geschrieben und laufen auf dem seL4-Mikrokernel, für den auf RISC-V-Systemen ein mathematischer Zuverlässigkeitsnachweis erbracht wurde, der zeigt, dass der Code vollständig den in der formalen Sprache festgelegten Spezifikationen entspricht. Der Projektcode ist unter der Apache 2.0-Lizenz geöffnet.
Das System bietet Unterstützung für Plattformen, die auf RISC-V- und ARM64-Architekturen basieren. Um den Betrieb von seL4 und der KataOS-Umgebung auf der Hardware zu simulieren, wird im Entwicklungsprozess das Renode-Framework verwendet. Als Referenzimplementierung wird der Software- und Hardwarekomplex Sparrow vorgeschlagen, der KataOS mit sicheren Chips auf Basis der OpenTitan-Plattform kombiniert. Mit der vorgeschlagenen Lösung können Sie einen logisch verifizierten Betriebssystemkernel mit vertrauenswürdigen Hardwarekomponenten (RoT, Root of Trust) kombinieren, die auf der OpenTitan-Plattform und der RISC-V-Architektur basieren. Neben dem KataOS-Code ist geplant, in Zukunft auch alle anderen Sparrow-Komponenten, einschließlich der Hardware-Komponente, zu öffnen.
Die Plattform wird mit Blick auf die Anwendung in speziellen Chips entwickelt, die für die Ausführung von Anwendungen für maschinelles Lernen und die Verarbeitung vertraulicher Informationen konzipiert sind, die ein besonderes Maß an Schutz und eine Bestätigung der Fehlerfreiheit erfordern. Beispiele für solche Anwendungen sind Systeme, die Bilder von Menschen und Sprachaufzeichnungen manipulieren. Durch den Einsatz der Zuverlässigkeitsüberprüfung durch KataOS wird sichergestellt, dass sich der Fehler nicht auf den Rest des Systems und insbesondere auf den Kernel und kritische Teile ausbreitet, wenn ein Teil des Systems ausfällt.
Die seL4-Architektur zeichnet sich dadurch aus, dass sie Teile zur Verwaltung von Kernel-Ressourcen in den Benutzerbereich verlagert und für diese Ressourcen dieselben Zugriffskontrolltools anwendet 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.
Für zusätzlichen Schutz werden alle Komponenten außer dem Mikrokernel nativ in Rust unter Verwendung sicherer Programmiertechniken entwickelt, die Speicherfehler minimieren, die zu Problemen wie Speicherzugriff nach der Freigabe, Nullzeiger-Dereferenzierungen und Pufferüberläufen führen. In Rust wurden ein Anwendungslader in der seL4-Umgebung, Systemdienste, ein Framework für die Anwendungsentwicklung, eine API für den Zugriff auf Systemaufrufe, ein Prozessmanager, ein Mechanismus zur dynamischen Speicherzuweisung usw. geschrieben. Die verifizierte Baugruppe verwendet das CAmkES-Toolkit, das vom seL4-Projekt entwickelt wurde. Komponenten für CAmkES können auch in Rust erstellt werden.
Rust erzwingt die Speichersicherheit zur Kompilierungszeit durch Referenzprüfung, Objektbesitz und Objektlebensdauerverfolgung (Bereiche) sowie durch die Bewertung der Korrektheit von Speicherzugriffen zur Laufzeit. Rust bietet außerdem Schutz vor Ganzzahlüberläufen, erfordert die Initialisierung von Variablenwerten vor der Verwendung, verwendet standardmäßig das Konzept unveränderlicher Referenzen und Variablen und bietet starke statische Typisierung, um logische Fehler zu minimieren.
Source: opennet.ru