Google hat die Entwicklung im Zusammenhang mit dem Projekt KataOS angekündigt, das darauf abzielt, ein sicheres Betriebssystem für eingebettete Geräte zu schaffen. Die Systemkomponenten von KataOS sind in der Programmiersprache Rust geschrieben und laufen auf dem Mikrokernel seL4, für den auf RISC-V-Systemen ein mathematischer Nachweis der Zuverlässigkeit erbracht wurde, der die vollständige Übereinstimmung des Codes mit den in einer formalen Sprache festgelegten Spezifikationen belegt. Der Code des Projekts steht unter der Lizenz Apache 2.0.
Das System unterstützt Plattformen, die auf RISC-V- und ARM64-Architekturen basieren. Für die Simulation von seL4 und der KataOS-Umgebung auf der Hardware während der Entwicklung wird das Renode-Framework verwendet. Als Referenzimplementierung wird das software-hardware System Sparrow vorgeschlagen, das KataOS mit sicheren Chips basierend auf der OpenTitan-Plattform kombiniert. Die vorgeschlagene Lösung ermöglicht es, einen logisch verifizierten Kern des Betriebssystems mit vertrauenswürdigen Hardwarekomponenten (RoT, Root of Trust) zu kombinieren, die mit der OpenTitan-Plattform und der RISC-V-Architektur erstellt wurden. Neben dem Code von KataOS ist außerdem die Öffnung aller anderen Komponenten von Sparrow, einschließlich der Hardware, in Planung.
Die Plattform wird mit Blick auf den Einsatz in spezialisierten Chips entwickelt, die für Anwendungen im Bereich des maschinellen Lernens und der Verarbeitung vertraulicher Informationen ausgelegt sind. Diese Anwendungen erfordern ein besonderes Maß an Schutz und Verifizierung, um Ausfälle zu vermeiden. Beispiele für solche Anwendungen sind Systeme, die mit Bildern von Personen und Sprachaufnahmen arbeiten. Der Einsatz von KataOS zur Überprüfung der Zuverlässigkeit gewährleistet, dass ein Ausfall in einem Teil des Systems nicht auf andere Teile, insbesondere auf den Kernel und kritische Komponenten, übergreift.
Die Architektur von seL4 zeichnet sich dadurch aus, dass Teile zur Verwaltung der Kernel-Ressourcen in den Benutzerraum ausgelagert werden. Dabei werden für diese Ressourcen dieselben Zugriffssteuerungsmechanismen verwendet wie für die Benutzerressourcen. Das Mikrokernel stellt keine sofort einsatzbereiten hochabstrakten Schnittstellen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw. bereit, sondern lediglich minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Interrupts und Prozessorressourcen. Hochabstrakte Schnittstellen und Treiber für die Interaktion mit der Hardware werden separat auf dem Mikrokernel in Form von Aufgaben umgesetzt, die auf Benutzerebene ausgeführt werden. Der Zugriff dieser Aufgaben auf die Ressourcen des Mikrokernels erfolgt durch die Festlegung von Regeln.
Um zusätzlichen Schutz zu gewährleisten, werden alle Komponenten, mit Ausnahme des Mikro-Kernels, in der Programmiersprache Rust entwickelt. Dabei kommen sichere Programmiertechniken zum Einsatz, die Speicherfehler minimieren, die zu Problemen wie Zugriff auf freigegebene Speicherbereiche, Dereferenzierung von Nullzeigern und Pufferüberläufen führen können. Unter anderem wurden in Rust der Anwendungs-Loader in der seL4 Umgebung, Systemdienste, ein Framework für die Anwendungsentwicklung, APIs für den Zugriff auf Systemaufrufe, ein Prozessmanager und Mechanismen für die dynamische Speicherverteilung implementiert. Für die verifizierte Build-Umgebung wird das CAmkES-Toolkit verwendet, das vom seL4-Projekt entwickelt wird. Komponenten für CAmkES können ebenfalls in der Programmiersprache Rust erstellt werden.
Der sichere Umgang mit Speicher wird in Rust während der Kompilierung durch die Überprüfung von Referenzen, das Nachverfolgen des Eigentums von Objekten und die Berücksichtigung der Lebensdauer von Objekten (Sichtbarkeitsbereiche) gewährleistet. Rust bietet auch Mittel zum Schutz vor ganzzahligen Überläufen, erfordert die zwingende Initialisierung von Variablenwerten vor ihrer Verwendung, wendet das Konzept der Unveränderlichkeit (immutable) für Referenzen und Variablen standardmäßig an und bietet eine starke statische Typisierung zur Minimierung logischer Fehler.
Quelle: opennet.ru
