Projekt rozwijający otwarte mikrojądro seL4 otrzymał nagrodę ACM Software System Award, corocznie przyznawaną przez Stowarzyszenie Obliczeniowe (ACM), najbardziej prestiżową międzynarodową organizację w dziedzinie systemów komputerowych. Nagroda została przyznana za osiągnięcia w zakresie matematycznego dowodu niezawodności pracy, który świadczy o pełnym zgodności z wymaganiami określonymi w formalnych specyfikacjach i uznaje gotowość do stosowania w krytycznych zastosowaniach. Projekt seL4 wykazał, że można nie tylko w pełni przeprowadzić formalną weryfikację niezawodności i bezpieczeństwa dla projektów na poziomie przemysłowych systemów operacyjnych, ale też osiągnąć to bez uszczerbku na wydajności i wszechstronności.
Nagroda ACM Software System Award jest corocznie przyznawana za rozwój systemów oprogramowania, które miały decydujący wpływ na branżę, wprowadzając nowe koncepcje lub odkrywając nowe obszary zastosowań komercyjnych. Wartość nagrody wynosi 35 tysięcy dolarów amerykańskich. W poprzednich latach nagrody ACM przyznano projektom GCC i LLVM, a także ich twórcom Richardowi Stallmanowi i Chrisowi Lattnerowi. Nagrodzono również takie projekty i technologie jak 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ę przeniesieniem części odpowiedzialnych za zarządzanie zasobami jądra do przestrzeni użytkownika oraz zastosowaniem tych samych środków ochrony dostępu dla tych zasobów, jak dla zasobów użytkownika. Mikrojądro nie dostarcza gotowych wysokopoziomowych abstrakcji do zarządzania plikami, procesami, połączeniami sieciowymi itp., zamiast tego oferuje jedynie minimalne mechanizmy do zarządzania dostępem do fizycznej przestrzeni adresowej, przerwaniami i zasobami procesora. Wysokopoziomowe abstrakcje oraz sterowniki do interakcji ze sprzętem są realizowane osobno na bazie mikrojądra w postaci zadań wykonywanych na poziomie użytkownika. Dostęp tych zadań do zasobów mikrojądra organizowany jest poprzez określenie reguł.
Źródło: opennet.ru
