Projekt open microkernel seL4 otrzymał nagrodę ACM Software System Award, coroczną nagrodę przyznawaną przez Association for Computing Machinery (ACM), najbardziej szanowaną międzynarodową organizację w dziedzinie systemów komputerowych. Nagroda przyznawana jest za osiągnięcia w dziedzinie matematycznego dowodu działania, który wskazuje na pełną zgodność ze specyfikacjami podanymi w języku formalnym oraz uznaje gotowość do użycia w aplikacjach o znaczeniu krytycznym. Projekt seL4 pokazał, że możliwa jest nie tylko pełna formalna weryfikacja niezawodności i bezpieczeństwa projektów na poziomie przemysłowych systemów operacyjnych, ale także osiągnięcie tego bez utraty wydajności i wszechstronności.
Nagroda ACM Software System Award jest przyznawana corocznie w celu uznania rozwoju systemów oprogramowania, które wywarły decydujący wpływ na branżę, wprowadzając nowe koncepcje lub otwierając nowe aplikacje komercyjne. Wysokość nagrody wynosi 35 tysięcy dolarów amerykańskich. W poprzednich latach nagrody ACM przyznawane były projektom GCC i LLVM oraz ich założycielom Richardowi Stallmanowi i Chrisowi Latnerowi. Inne nagrodzone projekty i technologie to UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB i Eclipse .
Architektura mikrojądra seL4 wyróżnia się usunięciem części do zarządzania zasobami jądra w przestrzeni użytkownika i zastosowaniem tych samych środków kontroli dostępu do takich zasobów, jak do zasobów użytkownika. Mikrojądro nie zapewnia gotowych abstrakcji wysokiego poziomu do zarządzania plikami, procesami, połączeniami sieciowymi itp., Zamiast tego zapewnia jedynie minimalne mechanizmy kontrolowania dostępu do fizycznej przestrzeni adresowej, przerwań i zasobów procesora. Wysokopoziomowe abstrakcje i sterowniki do interakcji ze sprzętem są implementowane oddzielnie na szczycie mikrojądra w postaci zadań na poziomie użytkownika. Dostęp takich zadań do zasobów dostępnych dla mikrojądra jest zorganizowany poprzez zdefiniowanie reguł.
Źródło: opennet.ru