Das Projekt zur Entwicklung des offenen Mikrokernels seL4 wurde mit dem ACM Software System Award ausgezeichnet, der jährlich von der Association for Computing Machinery (ACM), der renommiertesten internationalen Organisation im Bereich der Computersysteme, vergeben wird. Die Auszeichnung wurde für die Erfolge im Bereich des mathematischen Nachweises der Zuverlässigkeit verliehen, der die vollständige Übereinstimmung mit formal festgelegten Spezifikationen belegt und die Einsatzbereitschaft in kritischen Anwendungen anerkennt. Das seL4-Projekt hat gezeigt, dass eine vollständige formale Verifikation der Zuverlässigkeit und Sicherheit für Projekte auf dem Niveau industrieller Betriebssysteme möglich ist, ohne dabei Abstriche bei Leistung und Flexibilität zu machen.
Der ACM Software System Award wird jährlich für die Entwicklung von Software-Systemen verliehen, die einen wesentlichen Einfluss auf die Branche gehabt haben, indem sie neue Konzepte eingeführt oder neue kommerzielle Anwendungsbereiche erschlossen haben. Die Prämie beträgt 35.000 US-Dollar. In den vergangenen Jahren wurden die ACM-Preise unter anderem an die Projekte GCC und LLVM sowie an deren Gründer Richard Stallman und Chris Lattner verliehen. 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 wurden ausgezeichnet.
Die Architektur des Mikro-Kernels seL4 zeichnet sich dadurch aus, dass Teile zur Verwaltung der Kernressourcen in den Benutzermodus ausgelagert werden, und dass dieselben Zugriffsteuerungsmechanismen für diese Ressourcen verwendet werden wie für Benutzerräume. Der Mikro-Kernel bietet keine fertigen, hochrangigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw.; stattdessen stellt er lediglich minimale Mechanismen zur Verfügung, um den Zugriff auf den physischen Adressraum, Interrupts und CPU-Ressourcen zu steuern. Hochrangige Abstraktionen und Treiber zur Interaktion mit der Hardware werden separat über dem Mikro-Kernel in Form von Aufgaben implementiert, die im Benutzermodus ausgeführt werden. Der Zugriff dieser Aufgaben auf die Ressourcen des Mikro-Kernels erfolgt durch die Festlegung von Regeln.
Quelle: opennet.ru
