Kata OS und Project Sparrow: Google legt "beweisbar sicheres" Betriebssystem offen
In seinem Open-Source-Blog hat Google des freie Betriebssystem Kata OS vorgestellt. Ziel der Arbeiten ist es dabei, eine "beweisbar sichere Plattform" zu erstellen, die sich für den Embedded-Einsatz zum Ausführen von Machine-Learning-Anwendungen eigne. Zum aktuellen Fortschritt an Kata OS schreibt das Unternehmen in der Ankündigung: "Dies ist ein laufendes Projekt, bei dem noch viel zu tun ist, aber wir freuen uns, einige frühe Details zu teilen und andere zur Zusammenarbeit auf der Plattform einzuladen" .
Google begründet die Arbeiten mit weitreichenderen Anwendungsgebieten von smarten Geräten, "die Informationen aus ihrer Umgebung sammeln und verarbeiten" . Weiter heißt es: "Wenn den Geräten um uns herum nicht mathematisch nachgewiesen werden kann, dass sie Daten sicher aufbewahren, könnten die von ihnen gesammelten personenbezogenen Daten - wie Bilder von Personen und Aufzeichnungen ihrer Stimmen - für bösartige Software zugänglich sein."
Grundlage der Arbeiten von Kata OS ist der als beweisbar sicher beschriebene Microkernel seL4. In Kooperation mit Antmicro sind dafür außerdem Simulatoren und Frameworks entstanden. Hinzu kommen Neuimplementierungen zur Nutzung von seL4 mit der als besonders sicher geltenden Programmiersprache Rust. Dementsprechend ist auch Kata OS selbst größtenteils in Rust geschrieben. Zusätzlich zu der seL4-Bibliothek haben die Beteiligten einen alternativen Rootserver für das System geschrieben sowie dazu notwendige Kernel-Änderungen umgesetzt. Der Code dazu findet sich auf Github(öffnet im neuen Fenster) .
Darüber hinaus arbeitet Google an einer Referenzimplementierung für die Hardware unter dem Codenamen Sparrow, der auch für das Gesamtprojekt genutzt wird. Hierfür soll Kata OS mit einer sicheren Hardwareplattform kombiniert werden. Diese entsteht laut Google wiederum mit Hilfe des Root-of-Trust-Chips Open Titan, der die freie CPU-Architektur RISC-V einsetzt. Zunächst werde aber ein 64-Bit-ARM-System mit Qemu simuliert.