Google ogłosiło odkrycie rozwiązań związanych z projektem KataOS, mającym na celu stworzenie bezpiecznego systemu operacyjnego dla sprzętu wbudowanego. Komponenty systemu KataOS są napisane w języku Rust i działają na mikrojądrze seL4, dla którego zapewniono matematyczny dowód niezawodności na systemach RISC-V, wskazujący, że kod jest w pełni zgodny ze specyfikacjami określonymi w języku formalnym. Kod projektu jest otwarty na licencji Apache 2.0.
System zapewnia obsługę platform opartych na architekturach RISC-V i ARM64. Aby symulować działanie seL4 i środowiska KataOS na sprzęcie, w procesie programowania wykorzystywana jest platforma Renode. Jako implementację referencyjną zaproponowano kompleks programowo-sprzętowy Sparrow, łączący KataOS z bezpiecznymi chipami opartymi na platformie OpenTitan. Proponowane rozwiązanie pozwala na połączenie logicznie zweryfikowanego jądra systemu operacyjnego z godnymi zaufania komponentami sprzętowymi (RoT, Root of Trust), zbudowanymi w oparciu o platformę OpenTitan i architekturę RISC-V. Oprócz kodu KataOS planowane jest w przyszłości otwarcie wszystkich pozostałych komponentów Sparrow, w tym komponentu sprzętowego.
Platforma rozwijana jest z myślą o zastosowaniu w wyspecjalizowanych chipach przeznaczonych do uruchamiania aplikacji do uczenia maszynowego i przetwarzania poufnych informacji, które wymagają szczególnego poziomu ochrony i potwierdzania braku awarii. Przykładami takich aplikacji są systemy manipulujące obrazami ludzi i nagraniami głosowymi. Stosowanie w KataOS weryfikacji niezawodności gwarantuje, że w przypadku awarii jednej części systemu, awaria nie rozprzestrzeni się na resztę systemu, a w szczególności na jądro i części krytyczne.
Architektura seL4 wyróżnia się przeniesieniem części do zarządzania zasobami jądra do przestrzeni użytkownika i zastosowaniem tych samych narzędzi 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ł.
Aby zapewnić dodatkową ochronę, wszystkie komponenty z wyjątkiem mikrojądra zostały natywnie opracowane w Rust przy użyciu bezpiecznych technik programowania, które minimalizują błędy pamięci prowadzące do problemów, takich jak dostęp do pamięci po zwolnieniu, wyłuskiwanie wskaźników zerowych i przepełnienie bufora. W Rust napisano moduł ładujący aplikacje w środowisku seL4, usługi systemowe, framework do tworzenia aplikacji, API dostępu do wywołań systemowych, menedżer procesów, mechanizm dynamicznej alokacji pamięci itp. W zweryfikowanym złożeniu wykorzystano zestaw narzędzi CAmkES opracowany w ramach projektu seL4. Komponenty dla CAmkES można także tworzyć w Rust.
Rust wymusza bezpieczeństwo pamięci w czasie kompilacji poprzez sprawdzanie referencji, własność obiektu i śledzenie czasu życia obiektu (zakresy) oraz ocenę poprawności dostępu do pamięci w czasie wykonywania. Rust zapewnia również ochronę przed przepełnieniem liczb całkowitych, wymaga inicjacji wartości zmiennych przed użyciem, domyślnie wykorzystuje koncepcję niezmiennych referencji i zmiennych oraz oferuje silne typowanie statyczne w celu zminimalizowania błędów logicznych.
Źródło: opennet.ru