Die Firma Google hat das Software-Hardware-Komplex Open Se Cura vorgestellt, das darauf abzielt, die Erstellung von sicheren Chips zu vereinfachen, die für Aufgaben im Zusammenhang mit maschinellem Lernen und künstlicher Intelligenz vorgesehen sind. Das Projekt umfasst ein Betriebssystem namens CantripOS und Hardware, die auf der OpenTitan-Plattform und einer Prozessorarchitektur mit RISC-V-Kern basiert. Während der Entwicklung trugen Open Se Cura und CantripOS die Namen Sparrow und KataOS, aber um Überschneidungen mit anderen Projekten zu vermeiden, wurden die Endprodukte umbenannt. Die Ergebnisse des Projekts, einschließlich Quelltexte der Systemdienste und RTL-Schemata (Register Transfer Level), werden unter der Lizenz Apache 2.0 veröffentlicht.
Das Betriebssystem CantripOS basiert auf dem Mikrokernel seL4, über dem eine Systemumgebung geschrieben ist, die in Rust implementiert wurde. Für das Mikrokernel seL4 wurde auf RISC-V-Systemen ein mathematischer Nachweis der Zuverlässigkeit erbracht, der bescheinigt, dass der Code vollständig den in formalen Sprachen festgelegten Spezifikationen entspricht. Die Architektur von seL4 zeichnet sich dadurch aus, dass Teile zur Verwaltung der Ressourcen des Kernels in den Benutzerspeicher ausgelagert werden und dieselben Zugangskontrollmechanismen für diese Ressourcen verwendet werden, die auch für Benutzerressourcen gelten.
Der Mikrokernel bietet keine fertigen Hochsprachenabstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw., sondern nur minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Interrupts und CPU-Ressourcen. Hochsprachenabstraktionen und Treiber zur Interaktion mit der Hardware werden separat oberhalb des Mikrokernels in Form von Aufgaben umgesetzt, die auf Benutzerebene ausgeführt werden. Der Zugriff dieser Aufgaben auf die dem Mikrokernel zur Verfügung stehenden Ressourcen wird durch die Definition von Regeln organisiert.
Alle Komponenten des Betriebssystems, außer dem Mikrokernel, sind ursprünglich in Rust geschrieben, wobei sichere Programmiertechniken verwendet werden, die Fehler bei der Arbeit mit Speicher minimieren. Unter anderem wurde in Rust der Anwendungsloader für die Umgebung seL4, Systemdienste, ein Framework zur Anwendungsentwicklung, eine API für den Zugriff auf Systemaufrufe, ein Prozessmanager und ein Mechanismus zur dynamischen Speicherzuweisung verfasst.
Für die verifizierte Implementierung wird das von dem seL4-Projekt entwickelte Tool CAmkES eingesetzt. Für die Entwicklung von Endanwendungen, die von Systemdiensten dynamisch geladen werden können, wird das SDK AmbiML empfohlen, während für die Ausführung von Modellen des maschinellen Lernens das Werkzeug IREE (Intermediate Representation Execution Environment) zur Verfügung steht. Komponenten in Rust und Systemdienste wurden mit den Frameworks Cantrip entwickelt.
Die Anwendungsmöglichkeiten der Plattform umfassen spezialisierte Chips, die ein besonderes Schutzniveau und die Bestätigung der Fehlerfreiheit erfordern. Beispielsweise kann die Plattform in Produkten des maschinellen Lernens eingesetzt werden, die mit der Verarbeitung vertraulicher Informationen in Verbindung stehen, wie z.B. Systeme zur Gesichts- und Sprachverarbeitung. Die Kombination eines logisch verifizierten Betriebssystemkerns 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 übrige System, insbesondere den Kern und kritische Komponenten, übergreifen kann.
Neben Google waren auch die gemeinnützige Organisation lowRISC, die die Entwicklung eines freien Mikroprozessors auf Basis der RISC-V-Architektur betreut, sowie die Unternehmen Antmicro und VeriSilicon an der Entwicklung des Werkzeugs und der Infrastruktur beteiligt. Der von lowRISC entwickelte Prozessor wurde als Kern für den Aufbau vertrauenswürdiger Hardwarekomponenten (RoT, Root of Trust) verwendet. Das Unternehmen Antmicro stellte dem Projekt den Simulator Renode zur Verfügung, der die Tests von CantripOS und dem Mikrokern seL4 ohne reale Hardware ermöglicht. VeriSilicon teilte seine Erfahrungen im Bereich der Chipentwicklung und der Erstellung von BSP (Board Support Package).
Quelle: opennet.ru
