Zakończono prace nad matematyczną formalną weryfikacją niezawodności i bezpieczeństwa działania mikrojądra seL4 na systemach z architekturą zestawu instrukcji AArch64. Weryfikacja polega na matematycznym dowodzie poprawności działania seL4, co świadczy o pełnej zgodności z określonymi w formalnym języku specyfikacjami. Dowód niezawodności pozwala na użycie seL4 w systemach krytycznych opartych na procesorach ARM64, które wymagają podwyższonego poziomu bezpieczeństwa i gwarantują brak awarii.
Początkowo mikrojądro seL4 zostało zweryfikowane dla 32-bitowych procesorów ARM, a później dla 64-bitowych procesorów x86 i RISC-V. Weryfikacja gwarantuje, że w przypadku awarii w jednej części systemu, nie rozprzestrzeni się ona na resztę systemu i jego krytyczne elementy. W kontekście zapewnienia bezpieczeństwa, weryfikacja potwierdza, że jądro zapewnia właściwy poziom izolacji aplikacji, nie pozwala im na dostęp do informacji bez autoryzacji i gwarantuje, że w przypadku kompromitacji aplikacji podrzędnych, atak nie rozprzestrzeni się na krytyczne aplikacje.
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
