Das Projekt seL4 erhält den ACM Software System Award

Das Projekt, das den offenen Mikrokernel seL4 entwickelt, erhielt den ACM Software System Award, der jährlich von der Association for Computing Machinery (ACM), der angesehensten internationalen Organisation im Bereich Computersysteme, verliehen wird. Der Preis wurde für Errungenschaften im Bereich des mathematischen Beweises der Zuverlässigkeit verliehen, der die vollständige Übereinstimmung mit den in formaler Sprache formulierten Spezifikationen belegt und die Einsatzbereitschaft in sicherheitskritischen Anwendungen anerkennt. Das Projekt seL4 hat gezeigt, dass es nicht nur möglich ist, eine vollständige formale Verifikation der Zuverlässigkeit und Sicherheit für Projekte auf dem Niveau industrieller Betriebssysteme durchzuführen, sondern dies auch ohne Einbußen bei der Leistung und Vielseitigkeit zu erreichen.

Der ACM Software System Award wird jährlich für die Entwicklung von Software-Systemen verliehen, die eine maßgebliche Wirkung auf die Branche hatten, indem sie neue Konzepte eingeführt oder neue Anwendungsbereiche im kommerziellen Sektor erschlossen haben. Die Höhe des Preises beträgt 35.000 US-Dollar. In den vergangenen Jahren wurden die ACM-Preise an die Projekte GCC und LLVM sowie an deren Gründer Richard Stallman und Chris Lattner verliehen. Ausgezeichnet wurden auch Projekte und Technologien wie UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB und Eclipse.

Die Architektur des Mikrokerns seL4 zeichnet sich durch die Auslagerung von Teilen zur Ressourcenverwaltung des Kerns in den Benutzermodus aus und der Anwendung derselben Zugriffssteuerungsmechanismen für diese Ressourcen wie für Benutzerressourcen. Der Mikrokern bietet keine fertigen hochgradigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw., sondern stellt lediglich minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Unterbrechungen und Prozessorressourcen zur Verfügung. Hochgradige Abstraktionen und Treiber für die Interaktion mit der Hardware werden separat auf Basis des Mikrokerns in Form von Aufgaben, die im Benutzermodus ausgeführt werden, implementiert. Der Zugriff dieser Aufgaben auf die beim Mikrokern vorhandenen Ressourcen wird durch die Festlegung von Regeln organisiert.

Quelle: opennet.ru