RISC-V zweryfikował mikrojądro seL4 na swoich procesorach RV64

Fundacja RISC-V ogłosiła, że ​​zweryfikowała jak działa mikrojądro seL4 w systemach z architektura zestawu instrukcji RISC-V. W którym proces weryfikacji sprowadza się do matematycznego dowodu wiarygodności seL4, co wskazuje na pełną zgodność ze specyfikacjami określonymi w języku formalnym.

Testowanie niezawodności umożliwia stosowanie seL4 w krytycznych systemach opartych na procesorach RISC-V RV64co wymaga wyższego poziomu niezawodności i nie gwarantuje awarii.

Twórcy oprogramowania działający na jądrze seL4 mogą być całkowicie pewni, że w przypadku awarii jednej części systemu, awaria ta nie rozprzestrzeni się na resztę systemu, aw szczególności na jego krytyczne części.

O seL4

Architektura seL4 wyróżnia się usuwaniem części w celu zarządzania zasobami jądra w przestrzeni użytkownika i używaj tych samych metod kontroli dostępu do takich zasobów, jak do zasobów użytkowników.

Mikrojądro nie zapewnia abstrakcji wysokiego poziomu już przygotowany do zarządzania plikami, procesami, połączeniami sieciowymi itp., ale zamiast tego zapewnia jedynie minimalne mechanizmy kontroli dostępu do fizycznej przestrzeni adresowej, przerwania i zasoby procesora.

Wysokopoziomowe abstrakcje i kontrolery do interakcji z komputerem są zaimplementowane oddzielnie na szczycie mikrojądra w postaci zadań wykonywanych na poziomie użytkownika.

Dostęp takich zadań do zasobów dostępnych w mikrojądrze jest zorganizowany poprzez definicję reguł.

RISC-V zapewnia otwarty i elastyczny system instrukcji maszynowych pozwala na tworzenie mikroprocesorów do dowolnych zastosowań, bez konieczności dedukcji i bez narzucania warunków użytkowania.

RISC-V pozwala tworzyć całkowicie otwarte procesory i SoC. Obecnie w oparciu o specyfikację RISC-V kilka firm i społeczności na różnych wolnych licencjach (BSD, MIT, Apache 2.0) opracowuje kilkadziesiąt wariantów już wyprodukowanych rdzeni mikroprocesorów, układów SoC i chipów.

Obsługa RISC-V istnieje od czasu wydania Glibc 2.27, binutils 2.30, gcc 7 i jądra Linux 4.15.

O testowaniu mikrojądra seL4

Początkowo plik microkernel seL4 został zweryfikowany dla 32-bitowych procesorów ARMI później dla 86-bitowych procesorów x64.

Zaobserwowano, że połączenie otwartej architektury sprzętowej RISC-V z otwartym mikrojądrem seL4 osiągnie nowy poziom bezpieczeństwa, ponieważ przyszłe komponenty sprzętowe można również w pełni zweryfikować, co jest niemożliwe do osiągnięcia w przypadku własnościowych architektur sprzętowych.

Kiedy sprawdzamy seL4, musimy założyć, że sprzęt działa poprawnie (czyli tak, jak określono). Zakłada to przede wszystkim, że istnieje jednoznaczna specyfikacja, co nie dotyczy wszystkich urządzeń. 

Ale nawet jeśli taka specyfikacja istnieje i jest formalna (to znaczy zapisana w formalizmie matematycznym, który wspiera matematyczne rozumowanie o swoich właściwościach), skąd wiemy, że faktycznie odzwierciedla ona zachowanie sprzętu? 

W rzeczywistości możemy być całkiem pewni, że tak nie jest. Sprzęt nie różni się od oprogramowania, ponieważ oba są wadliwe.

Ale posiadanie otwartego ISA ma zalety wykraczające poza bycie wolnym od opłat licencyjnych. Jednym z nich jest to, że umożliwia implementacje sprzętu typu open source.

Podczas sprawdzania seL4 zakłada się, że sprzęt działa zgodnie ze wskazaniami, a specyfikacja w pełni opisuje zachowanie systemu, ale w rzeczywistości sprzęt nie jest wolny od błędów, co dobrze widać w problemach, które regularnie pojawiają się w mechanizmie wykonania spekulacyjnego Instrukcja .

Otwarte platformy sprzętowe upraszczają integrację zmian związane z bezpieczeństwem, na przykład blokowanie wszystkich możliwych kanałów wycieku przez kanały stron trzecich, gdzie znacznie skuteczniej jest pozbyć się problemu za pomocą sprzętu, niż próbować znaleźć rozwiązania za pomocą oprogramowania.

Wreszcie, jeśli chcesz dowiedzieć się więcej na ten temat, zapoznaj się z notatką w następujący link.