Organizacja RISC-V Foundation o weryfikacji działania mikrojądra na systemach z architekturą zestawu instrukcji RISC-V. Weryfikacja sprowadza się do niezawodności działania seL4, co świadczy o pełnej zgodności z wymaganiami określonymi w formalnych specyfikacjach językowych. Dowód niezawodności seL4 w systemach krytycznych opartych na procesorach RISC-V RV64, wymagających wysokiego poziomu niezawodności i gwarantujących brak awarii. Programiści oprogramowania działającego na rdzeniu seL4 mogą być całkowicie pewni, że w przypadku awarii w jednej części systemu, awaria ta nie rozprzestrzeni się na pozostałą część systemu, w tym na jego krytyczne elementy.
Początkowo mikrojądro seL4 zostało zweryfikowane dla 32-bitowych procesorów ARM, a później dla 64-bitowych procesorów x86. Zauważa się, że połączenie otwartej architektury sprzętowej RISC-V z otwartym mikrojądrem seL4 pozwoli osiągnąć nowy poziom bezpieczeństwa, ponieważ komponenty sprzętowe w przyszłości również mogą być w pełni weryfikowane, co nie jest możliwe w przypadku zamkniętych architektur sprzętowych.
Podczas weryfikacji seL4 zakłada się, że sprzęt działa zgodnie z deklaracjami, a specyfikacja w pełni opisuje zachowanie systemu, ale w rzeczywistości sprzęt nie jest wolny od błędów, co dobrze udowadnia regularne występowanie problemów w mechanizmie spekulacyjnego wykonywania instrukcji. Otwarte platformy sprzętowe ułatwiają integrację zmian związanych z bezpieczeństwem — na przykład blokowanie wszelkich potencjalnych kanałów wycieku przez kanały boczne, w których znacznie efektywniejsze jest rozwiązanie problemu sprzętowo, niż próby jego obejścia programowo.
Przypominamy, że architektura seL4 przeniesieniem elementów do zarządzania zasobami jądra do przestrzeni użytkownika oraz zastosowaniem dla tych zasobów tych samych środków ograniczania dostępu, co dla zasobów użytkownika. Mikrojądro nie zapewnia gotowych wysokopoziomowych abstrakcji do zarządzania plikami, procesami, połączeniami sieciowymi itp., zamiast tego dostarcza jedynie minimalne mechanizmy do zarządzania dostępem do fizycznej przestrzeni adresowej, przerwaniami i zasobami procesora. Wysokopoziomowe abstrakcje i sterowniki do interakcji z sprzętem są realizowane osobno na mikrojądrem w formie zadań wykonywanych na poziomie użytkownika. Dostęp tych zadań do zasobów mikrojądra jest organizowany poprzez określenie reguł.
RISC-V oferuje otwarty i elastyczny system instrukcji maszynowych, umożliwiający tworzenie mikroprocesorów do dowolnych zastosowań, nie wymagając przy tym opłat i nie nakładając warunków na użytkowanie. RISC-V pozwala na tworzenie w pełni otwartych SoC i procesorów. Obecnie na podstawie specyfikacji RISC-V różne firmy i społeczności tworzą pod różnymi wolnymi licencjami (BSD, MIT, Apache 2.0) kilkadziesiąt wariantów rdzeni mikroprocesorów, SoC i już produkowanych chipów. Wsparcie dla RISC-V jest obecne od wydań Glibc 2.27, binutils 2.30, gcc 7 i jądra Linux 4.15.
Źródło: opennet.ru
