Das offene Mikrokernel-Projekt seL4 wurde mit dem ACM Software System Award ausgezeichnet, einer jährlichen Auszeichnung der Association for Computing Machinery (ACM), der angesehensten internationalen Organisation auf dem Gebiet der Computersysteme. Die Auszeichnung wird für Leistungen auf dem Gebiet des mathematischen Betriebsnachweises verliehen, der die vollständige Einhaltung der in einer formalen Sprache gegebenen Spezifikationen belegt und die Einsatzbereitschaft für geschäftskritische Anwendungen anerkennt. Das seL4-Projekt hat gezeigt, dass es nicht nur möglich ist, Zuverlässigkeit und Sicherheit für Projekte auf der Ebene industrieller Betriebssysteme vollständig formal zu verifizieren, sondern dies auch ohne Einbußen bei Leistung und Vielseitigkeit zu erreichen.
Der ACM Software System Award wird jährlich verliehen, um die Entwicklung von Softwaresystemen zu würdigen, die einen entscheidenden Einfluss auf die Branche hatten, indem sie neue Konzepte einführten oder neue kommerzielle Anwendungen eröffneten. Die Höhe der Auszeichnung beträgt 35 US-Dollar. In den vergangenen Jahren wurden ACM-Auszeichnungen an die Projekte GCC und LLVM sowie an ihre Gründer Richard Stallman und Chris Latner verliehen. Weitere Projekte und Technologien, die ebenfalls ausgezeichnet wurden, waren 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 Mikrokernels seL4 zeichnet sich dadurch aus, dass Teile zur Verwaltung der Kernel-Ressourcen im Benutzerbereich entfernt wurden und für diese Ressourcen dieselben Mittel zur Zugriffskontrolle wie für Benutzerressourcen angewendet wurden. Der Mikrokernel bietet keine sofort einsatzbereiten High-Level-Abstraktionen für die Verwaltung von Dateien, Prozessen, Netzwerkverbindungen und dergleichen, sondern nur minimale Mechanismen zur Steuerung des Zugriffs auf den physischen Adressraum, Interrupts und Prozessorressourcen. Abstraktionen auf hoher Ebene und Treiber für die Interaktion mit der Hardware werden separat auf dem Mikrokernel in Form von Aufgaben auf Benutzerebene implementiert. Der Zugriff solcher Aufgaben auf die dem Mikrokernel zur Verfügung stehenden Ressourcen wird durch die Definition von Regeln organisiert.
Source: opennet.ru