Het seL4 open microkernel-project heeft de ACM Software System Award ontvangen, een jaarlijkse onderscheiding die wordt uitgereikt door de Association for Computing Machinery (ACM), de meest gerespecteerde internationale organisatie op het gebied van computersystemen. De onderscheiding wordt toegekend voor prestaties op het gebied van wiskundig bewijs van werking, wat aangeeft dat volledig wordt voldaan aan de specificaties in een formele taal en dat het gereed is voor gebruik in missiekritieke toepassingen. Het seL4-project heeft aangetoond dat het niet alleen mogelijk is om de betrouwbaarheid en veiligheid van projecten volledig formeel te verifiëren op het niveau van industriële besturingssystemen, maar ook om dit te bereiken zonder concessies te doen aan prestaties en veelzijdigheid.
De ACM Software System Award wordt jaarlijks uitgereikt ter erkenning van de ontwikkeling van softwaresystemen die een bepalende invloed hebben gehad op de industrie, door nieuwe concepten te introduceren of nieuwe commerciële toepassingen te openen. Het bedrag van de onderscheiding is 35 duizend dollar. In de afgelopen jaren zijn ACM-prijzen uitgereikt aan de GCC- en LLVM-projecten en hun oprichters Richard Stallman en Chris Latner. Andere erkende projecten en technologieën zijn UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB en Eclipse.
De architectuur van de seL4-microkernel valt op door het verwijderen van onderdelen voor het beheer van kernelbronnen in de gebruikersruimte en door het toepassen van dezelfde middelen voor toegangscontrole voor dergelijke bronnen als voor gebruikersbronnen. De microkernel biedt geen out-of-the-box abstracties op hoog niveau voor het beheer van bestanden, processen, netwerkverbindingen en dergelijke, maar biedt slechts minimale mechanismen voor het controleren van de toegang tot de fysieke adresruimte, interrupts en processorbronnen. Abstracties op hoog niveau en stuurprogramma's voor interactie met hardware worden afzonderlijk bovenop de microkernel geïmplementeerd in de vorm van taken op gebruikersniveau. De toegang van dergelijke taken tot de bronnen die beschikbaar zijn voor de microkernel wordt georganiseerd door het definiëren van regels.
Bron: opennet.ru