Das Unternehmen Google hat die Er\u00f6ffnung von Arbeiten im Zusammenhang mit dem Projekt KataOS angek\u00fcndigt, das auf die Entwicklung eines sicheren Betriebssystems f\u00fcr eingebettete Ger\u00e4te abzielt. Die Systemkomponenten von KataOS sind in der Programmiersprache Rust geschrieben und laufen \u00fcber dem Mikrokernel seL4, f\u00fcr den auf RISC-V-Systemen ein mathematischer Nachweis der Zuverl\u00e4ssigkeit erbracht wurde, der die vollst\u00e4ndige \u00dcbereinstimmung des Codes mit den auf einer formalen Sprache spezifizierten Anforderungen belegt. Der Code des Projekts ist unter der Lizenz Apache 2.0 offen zug\u00e4nglich. <\/p>\n
Das System unterst\u00fctzt 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\u00f6sung erm\u00f6glicht die Kombination eines logisch verifizierten Betriebssystemkerns mit vertrauensw\u00fcrdigen 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 \u00d6ffnung aller anderen Komponenten von Sparrow, einschlie\u00dflich der Hardware, geplant. <\/p>\n
Die Plattform entwickelt sich mit Blick auf den Einsatz in spezialisierten Chips, die f\u00fcr die Ausf\u00fchrung von Anwendungen f\u00fcr maschinelles Lernen und die Verarbeitung vertraulicher Informationen gedacht sind, die ein besonderes Ma\u00df an Schutz und einen Nachweis des Fehlens von Ausf\u00e4llen erfordern. Beispiele f\u00fcr derartige Anwendungen sind Systeme, die mit Bildern von Menschen und Sprachaufnahmen arbeiten. Der Einsatz von Zuverl\u00e4ssigkeitsverifizierung in KataOS gew\u00e4hrleistet, dass im Falle eines Ausfalls eines Teils des Systems dieser Fehler nicht auf den Rest des Systems, insbesondere auf den Kern und kritische Teile, \u00fcbergreift. <\/p>\n
Die Architektur von seL4 zeichnet sich durch die Auslagerung von Teilen zur Verwaltung der Kernel-Ressourcen in den Benutzerraum aus und verwendet f\u00fcr diese Ressourcen dieselben Zugriffsregeln wie f\u00fcr 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\u00fchrt werden. Der Zugriff solcher Aufgaben auf die vom Mikrokernel bereitgestellten Ressourcen wird durch die Definition von Regeln organisiert. <\/p>\n
Zur zus\u00e4tzlichen Sicherheit werden alle Komponenten, mit Ausnahme des Mikrokernels, urspr\u00fcnglich 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\u00fcberl\u00e4ufen f\u00fchren k\u00f6nnen. Unter anderem wurde in Rust der Anwendungsbootloader f\u00fcr 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\u00fcr den verifizierten Build wird das CAmkES-Toolset verwendet, das vom seL4-Projekt entwickelt wird. Komponenten f\u00fcr CAmkES k\u00f6nnen ebenfalls in Rust geschrieben werden. <\/p>\n