Google hat ein komplettes Software-Hardware-System namens Open Se Cura vorgestellt, das darauf abzielt, die Entwicklung von sicheren Chips für Anwendungen im Bereich maschinelles Lernen und künstliche Intelligenz zu vereinfachen. Das Projekt umfasst das Betriebssystem CantripOS sowie Hardware, die auf der OpenTitan-Plattform und einer Prozessorarchitektur auf Basis von RISC-V basiert. Während der Entwicklung trugen Open Se Cura und CantripOS die Codenamen Sparrow und KataOS, doch um Überschneidungen mit anderen Projekten zu vermeiden, wurden die finalen Produkte umbenannt. Die Ergebnisse des Projekts, einschließlich des Quellcodes für Systemdienste und RTL-Schemata (Register Transfer Level), werden unter der Apache 2.0-Lizenz veröffentlicht.
Das Betriebssystem CantripOS basiert auf dem Mikrokernel seL4, über dem eine Systemumgebung, die in Rust geschrieben ist, läuft. Für den Mikrokernel seL4 liegt ein mathematischer Beweis der Zuverlässigkeit vor, der die vollständige Übereinstimmung des Codes mit den Spezifikationen, die in einer formalen Sprache definiert sind, belegt, insbesondere für RISC-V-Systeme. Die Architektur seL4 zeichnet sich dadurch aus, dass Teile zur Verwaltung von Kernel-Ressourcen in den Benutzermodus verlagert werden und dieselben Mittel zur Zugriffskontrolle für diese Ressourcen verwendet werden wie für Benutzerräume.
Der Mikrokernel bietet keine vorgefertigten hochrangigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw. Stattdessen stellt er lediglich minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Interrupts und Prozessorressourcen bereit. Hochrangige Abstraktionen und Treiber zur Interaktion mit der Hardware werden separat über dem Mikrokernel in Form von Aufgaben, die auf Benutzerebene ausgeführt werden, realisiert. Der Zugang dieser Aufgaben zu den Ressourcen des Mikrokernels wird durch die Festlegung von Regeln organisiert.
Alle Komponenten des Betriebssystems, mit Ausnahme des Mikrokerns, sind ursprünglich in der Programmiersprache Rust geschrieben, wobei sichere Programmiertechniken verwendet werden, die Fehler im Umgang mit dem Speicher minimieren. Unter anderem sind in Rust der Anwendungs-Loader in der Umgebung seL4, Systemdienste, ein Framework zur Anwendungsentwicklung, eine API für den Zugriff auf Systemaufrufe, der Prozessmanager und der Mechanismus für die dynamische Speicherzuweisung geschrieben.
Für den verifizierten Build wird das CAmkES-Toolkit verwendet, das vom seL4-Projekt entwickelt wird. Für die Entwicklung von Endanwendungen, die von Systemdiensten dynamisch geladen werden können, wird das SDK AmbiML empfohlen, und zur Ausführung von Modellen des maschinellen Lernens wird das Toolkit IREE (Intermediate Representation Execution Environment) angeboten. Komponenten in Rust und Systemdienste wurden unter Verwendung der Cantrip-Frameworks entwickelt.
Die Einsatzbereiche der Plattform umfassen spezialisierte Chips, die ein besonderes Maß an Schutz und Bestätigung der Fehlertoleranz erfordern. Beispielsweise kann die Plattform in Produkten für maschinelles Lernen eingesetzt werden, die mit der Verarbeitung vertraulicher Informationen verbunden sind, wie etwa in Systemen zur Gesichtserkennung und der Verarbeitung von Sprachaufnahmen. Die Kombination eines logisch verifizierten Kernels des Betriebssystems mit vertrauenswürdigen Hardwarekomponenten (RoT, Root of Trust) gewährleistet, dass im Falle eines Fehlers in einem Teil des Systems dieser Fehler nicht auf das gesamte System, insbesondere nicht auf den Kernel und kritische Teile, übergreift.
Neben Google waren an der Entwicklung von Werkzeugen und Infrastrukturkomponenten die gemeinnützige Organisation lowRISC, die die Entwicklung eines offenen Mikroprozessors auf Basis der RISC-V-Architektur überwacht, sowie die Unternehmen Antmicro und VeriSilicon beteiligt. Der von lowRISC entwickelte Prozessor wurde als Kern für die Erstellung vertrauenswürdiger Hardwarekomponenten (RoT, Root of Trust) verwendet. Das Unternehmen Antmicro stellte dem Projekt den Simulator Renode zur Verfügung, mit dem CantripOS und das Mikro-Kernel seL4 ohne echte Hardware getestet werden können. VeriSilicon teilte seine Erfahrungen in der Chipentwicklung und der Erstellung von BSP (Board Support Package).
Quelle: opennet.ru
