Het project dat het open microkernel seL4 ontwikkelt, heeft de ACM Software System Award ontvangen, die jaarlijks wordt uitgereikt door de Association for Computing Machinery (ACM), de meest vooraanstaande internationale organisatie op het gebied van computersystemen. De prijs wordt toegekend voor prestaties op het gebied van wiskundig bewijs van de betrouwbaarheid, dat aantoont dat het volledig voldoet aan de specificaties in formele taal en erkent de gereedheid voor gebruik in kritieke toepassingen. Het seL4-project heeft aangetoond dat formele verificatie van betrouwbaarheid en veiligheid voor projecten op het niveau van industriƫle besturingssystemen niet alleen volledig kan worden uitgevoerd, maar ook zonder verlies van prestaties en veelzijdigheid.
De ACM Software System Award wordt jaarlijks uitgereikt voor de ontwikkeling van softwaresystemen die een bepalende impact op de sector hebben gehad door nieuwe concepten te introduceren of nieuwe commerciƫle toepassingen te onthullen. De prijs bedraagt 35.000 dollar. In voorgaande jaren zijn de ACM-prijzen toegekend aan projecten zoals GCC en LLVM, en hun oprichters Richard Stallman en Chris Lattner. Ook zijn projecten en technologieƫn zoals UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB en Eclipse onderscheiden.
De architectuur van de seL4-microkernel is opmerkelijk vanwege het verplaatsen van delen voor de beheersing van kernelbronnen naar de gebruikersruimte en het toepassen van dezelfde toegangscontrolemechanismen voor deze bronnen als voor gebruikersbronnen. De microkernel biedt geen kant-en-klare hoge abstracties voor het beheer van bestanden, processen, netwerkverbindingen, enzovoort; in plaats daarvan biedt het slechts minimale mechanismen voor het beheer van de toegang tot fysieke adressen, onderbrekingen en CPU-bronnen. Hoge abstracties en stuurprogramma's voor interactie met hardware worden apart boven op de microkernel geĆÆmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd. De toegang van deze taken tot de resources van de microkernel wordt georganiseerd door het definiĆ«ren van regels.
Bron: opennet.ru
