Fundacja RISC-V o weryfikacji działania mikrojądra w systemach z architekturą zestawu instrukcji RISC-V. Weryfikacja sprowadza się do niezawodność działania seL4, która wskazuje na pełną zgodność ze specyfikacjami określonymi w języku formalnym. Dowód niezawodności seL4 w systemach o znaczeniu krytycznym opartych na procesorach RISC-V RV64, które wymagają zwiększonego poziomu niezawodności i gwarantują brak awarii. Twórcy oprogramowania działającego na jądrze seL4 mogą być całkowicie pewni, że jeśli wystąpi awaria w jednej części systemu, awaria ta nie rozprzestrzeni się na resztę systemu, a w szczególności na jego krytyczne części.
Mikrojądro seL4 zostało początkowo zweryfikowane dla 32-bitowych procesorów ARM, a później dla 64-bitowych procesorów x86. Należy zauważyć, ż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 będą mogły być w pełni weryfikowane także w przyszłości, co jest niemożliwe do osiągnięcia w przypadku zastrzeżonych architektur sprzętowych.
Przy weryfikacji seL4 zakłada się, że sprzęt działa zgodnie z założeniami i specyfikacja w pełni opisuje zachowanie systemu, jednak w rzeczywistości sprzęt nie jest wolny od błędów, o czym wyraźnie świadczą regularnie pojawiające się problemy w mechanizmie spekulatywnej realizacji instrukcje. Otwarte platformy sprzętowe ułatwiają integrację zmian związanych z bezpieczeństwem – na przykład blokowanie wszelkich możliwych wycieków z kanału bocznego, gdzie znacznie skuteczniej jest pozbyć się problemu sprzętowego, niż próbować znaleźć obejścia w oprogramowaniu.
Przypomnijmy, że architektura seL4 przenoszenie części do zarządzania zasobami jądra do przestrzeni użytkownika i stosowanie 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. Abstrakcje wysokiego poziomu i sterowniki do interakcji ze sprzętem są implementowane oddzielnie na mikrojądrze w formie zadań na poziomie użytkownika. Dostęp takich zadań do zasobów dostępnych mikrojądro jest zorganizowany poprzez zdefiniowanie reguł.
RISC-V zapewnia otwarty i elastyczny system instrukcji maszynowych, który umożliwia budowanie mikroprocesorów do dowolnych zastosowań bez konieczności płacenia opłat licencyjnych lub dodatkowych obowiązków związanych z ich użytkowaniem. RISC-V pozwala na tworzenie całkowicie otwartych SoC i procesorów. Obecnie w oparciu o specyfikację RISC-V różnych firm i społeczności w ramach różnych wolnych licencji (BSD, MIT, Apache 2.0) kilkadziesiąt wariantów rdzeni mikroprocesorów, SoC i już wyprodukowanych chipów. Obsługa RISC-V jest dostępna od wydania Glibc 2.27, binutils 2.30, gcc 7 i jądra Linuksa 4.15.
Źródło: opennet.ru