KataOS & Sparrow: Googles Betriebssystem ist beweisbar sicher konzipiert

Wie Google auf seinem Open Source Blog ankündigt, soll KataOS als beweisbar sicheres Betriebssystem auf Basis des Microkernel seL4 für smarte Geräte und solche aus dem Embedded-Bereich konzipiert worden sein. Das Projekt Sparrow soll die Referenzhardware, KataOS und RISC-V zu einer sicheren Plattform vereinen.

Google will Daten mit KataOS besser schützen

Die Grundlage für das „smarte“ Embedded-Betriebssystem von Google bildet der beweisbar sichere Microkernel seL4, was zu einer ebenso beweisbar sicheren Plattform zum Ausführen von Anwendungen für das maschinelle Lernen (ML) auf smarten Geräten führen soll. Damit sollen insbesondere die aus der Umgebung des Endverbrauchers aufgezeichneten Informationen geschützt werden.

Insbesondere smarte Assistenzsysteme, wie sie im Bereich Smart Home aber auch auf Smartphones und anderen smarten Geräten des täglichen Lebens zum Einsatz kommen, sammeln massenhaft personenbezogene Daten. Diese möchte Google zukünftig mit KataOS besser schützen.

Wenn Geräten um uns herum nicht mathematisch nachgewiesen werden kann, dass sie die Daten sicher aufbewahren können, können die von ihnen gesammelten personenbezogenen Daten, wie Bilder von Personen und Aufzeichnungen ihrer Stimmen, für bösartige Software möglicherweise zugänglich sein.

Google

seL4 und Rust für garantierte Vertraulichkeit

Auf Basis des seL4-Microkernel und in Kooperation mit Antmicro, das auf Industrielösungen für AI, ML, Cloud und Edge spezialisiert ist, wurden außerdem entsprechende Simulatoren und Frameworks entwickelt. Zudem wurde die als besonders sicher geltende Programmiersprache Rust implementiert.

Als Grundlage für dieses neue Betriebssystem haben wir seL4 als Mikrokernel gewählt, weil es die Sicherheit in den Vordergrund stellt; es ist mathematisch erwiesen sicher, mit garantierter Vertraulichkeit, Integrität und Verfügbarkeit.

Google

KataOS selbst wurde in weiten Teilen in Rust geschrieben und soll in Kombination mit dem seL4-Kernel dafür sorgen, dass Angriffsszenarien wie beispielsweise ein Off-by-one-Error oder ein Pufferüberlauf ausgeschlossen sind.

OpenTitan, Arm64 und RISC-V für Sparrow

Zusätzlich zum logisch sicheren Betriebssystem-Kernel enthält das Projekt mit Sparrow eine ebenso logisch sichere Hardware als Vertrauensbasis, die mit dem Open Source Silicon Root of Trust (RoT) OpenTitan auf einer RISC-V-Architektur basieren wird. Die erste Version soll indes noch auf Arm64 setzen.

Um ein sicheres Umgebungssystem in seiner Gesamtheit zu testen, bauen wir auch eine Referenzimplementierung für KataOS namens Sparrow, die KataOS mit einer sicheren Hardware-Plattform kombiniert.

Zusätzlich zum logisch sicheren Betriebssystem-Kernel enthält Sparrow eine logisch sichere Vertrauensbasis, die mit OpenTitan auf einer RISC-V-Architektur aufgebaut ist. In unserer ersten Version zielen wir jedoch auf eine standardmäßige 64-Bit-ARM-Plattform ab, die in der Simulation mit QEMU läuft.

In der finalen Version sollen sowohl KataOS als auch der Hardware-Stack Sparrow vollständig Open Source und für jedermann zugänglich sein. Den aktuellen Stand der Entwicklung dokumentiert die Projektseite auf der Entwicklerplattform GitHub.

Weitere Informationen zum beweisbar sicheren Betriebssystem-Kernel liefert die offizielle Website der seL4-Foundation.