Das Unternehmen Google hat die Eröffnung von Arbeiten im Zusammenhang mit dem Projekt KataOS angekündigt, das auf die Entwicklung eines sicheren Betriebssystems für eingebettete Geräte abzielt. Die Systemkomponenten von KataOS sind in der Programmiersprache Rust geschrieben und laufen über 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 auf einer formalen Sprache spezifizierten Anforderungen belegt. Der Code des Projekts ist unter der Lizenz Apache 2.0 offen zugänglich.
Das System unterstützt Plattformen auf Basis der Architekturen RISC-V und ARM64. Zur Simulation des Betriebs von seL4 und der Umgebung von KataOS auf der Hardware wird im Entwicklungsprozess das Framework Renode verwendet. Als Referenzimplementierung wurde das Software-Hardware-System Sparrow vorgeschlagen, das KataOS mit sicheren Chips auf Basis der OpenTitan-Plattform kombiniert. Die vorgeschlagene Lösung ermöglicht die Kombination eines logisch verifizierten Betriebssystemkerns mit vertrauenswürdigen Hardwarekomponenten (RoT, Root of Trust), die unter Verwendung der OpenTitan-Plattform und der RISC-V-Architektur erstellt wurden. Neben dem Code von KataOS ist in Zukunft auch die Öffnung aller anderen Komponenten von Sparrow, einschließlich der Hardware, geplant.
Die Plattform entwickelt sich mit Blick auf den Einsatz in spezialisierten Chips, die für die Ausführung von Anwendungen für maschinelles Lernen und die Verarbeitung vertraulicher Informationen gedacht sind, die ein besonderes Maß an Schutz und einen Nachweis des Fehlens von Ausfällen erfordern. Beispiele für derartige Anwendungen sind Systeme, die mit Bildern von Menschen und Sprachaufnahmen arbeiten. Der Einsatz von Zuverlässigkeitsverifizierung in KataOS gewährleistet, dass im Falle eines Ausfalls eines Teils des Systems dieser Fehler nicht auf den Rest des Systems, insbesondere auf den Kern und kritische Teile, übergreift.
Die Architektur von seL4 zeichnet sich durch die Auslagerung von Teilen zur Verwaltung der Kernel-Ressourcen in den Benutzerraum aus und verwendet für diese Ressourcen dieselben Zugriffsregeln wie für Benutzerressourcen. Der Mikrokernel bietet keine vorgefertigten, hochabstrakten Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw., sondern stellt lediglich minimale Mechanismen zur Verwaltung des Zugriffs auf den physikalischen Adressraum, Interrupts und Prozessorressourcen bereit. Hochabstrakte Abstraktionen und Treiber zur Interaktion mit der Hardware werden getrennt oberhalb des Mikrokernels in Form von Aufgaben implementiert, die auf Benutzerebene ausgeführt werden. Der Zugriff solcher Aufgaben auf die vom Mikrokernel bereitgestellten Ressourcen wird durch die Definition von Regeln organisiert.
Zur zusätzlichen Sicherheit werden alle Komponenten, mit Ausnahme des Mikrokernels, ursprünglich in der Programmiersprache Rust entwickelt, wobei sichere Programmiertechniken verwendet werden, die Fehler bei der Speicherverwaltung minimieren, die zu Problemen wie dem Zugriff auf freigegebenen Speicher, Dereferenzierung von Nullzeigern und Pufferüberläufen führen können. Unter anderem wurde in Rust der Anwendungsbootloader für die seL4-Umgebung, die Systemdienste, das Framework zur Anwendungsentwicklung, die API zum Zugriff auf Systemaufrufe, der Prozessmanager, der Mechanismus zur dynamischen Speicherzuweisung usw. geschrieben. Für den verifizierten Build wird das CAmkES-Toolset verwendet, das vom seL4-Projekt entwickelt wird. Komponenten für CAmkES können ebenfalls in Rust geschrieben werden.
Die sichere Speicherverwaltung wird in Rust während der Kompilierung durch Überprüfung von Referenzen, Nachverfolgung des Eigentums an Objekten und Berücksichtigung der Lebensdauer von Objekten (Gültigkeitsbereich) sowie durch die Bewertung der Zugriffsberechtigung zur Laufzeit des Codes sichergestellt. Rust bietet zudem Werkzeuge zum Schutz vor ganzzahligen Überläufen, verlangt die obligatorische Initialisierung von Variablenwerten vor der 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
