Firma Google ogłosiła otwarcie prac związanych z projektem KataOS, który ma na celu stworzenie zabezpieczonego systemu operacyjnego dla wbudowanego sprzętu. Komponenty systemowe KataOS są napisane w języku Rust i działają na mikrojądrze seL4, dla którego na systemach RISC-V dostarczono matematyczne dowody niezawodności, potwierdzające pełną zgodność kodu z wymaganiami określonymi w formalnym języku. Kod projektu jest udostępniany na licencji Apache 2.0.
System zapewnia wsparcie dla platform opartych na architekturach RISC-V i ARM64. W celu symulacji działania seL4 i środowiska KataOS na sprzęcie w trakcie rozwoju wykorzystuje się framework Renode. Jako wzorcowa implementacja zaproponowano system sprzętowo-programowy Sparrow, łączący KataOS z zabezpieczonymi chipami na platformie OpenTitan. Proponowane rozwiązanie umożliwia połączenie logicznie zweryfikowanego jądra systemu operacyjnego z zaufanymi komponentami sprzętowymi (RoT, Root of Trust), zbudowanymi z wykorzystaniem platformy OpenTitan i architektury RISC-V. Oprócz kodu KataOS planowane jest również otwarcie wszystkich pozostałych komponentów Sparrow, w tym części sprzętowej.
Platforma rozwija się z myślą o zastosowaniu w specjalistycznych chipach zaprojektowanych do uruchamiania aplikacji do uczenia maszynowego i przetwarzania poufnych informacji, które wymagają szczególnego poziomu zabezpieczeń i potwierdzenia braku awarii. Przykładami takich aplikacji są systemy manipulujące obrazami ludzi oraz nagraniami głosowymi. Wykorzystanie w KataOS weryfikacji niezawodności gwarantuje, że w przypadku awarii w jednej części systemu, nie rozprzestrzeni się ona na pozostałą część systemu i, w szczególności, na jądro oraz krytyczne miejsca.
Architektura seL4 wyróżnia się wydzieleniem 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, co dla zasobów użytkownika. Mikrojądro nie oferuje gotowych abstrahacji wysokiego poziomu do zarządzania plikami, procesami, połączeniami sieciowymi itd., zamiast tego dostarcza jedynie minimalne mechanizmy do zarządzania dostępem do fizycznej przestrzeni adresowej, przerwaniami i zasobami procesora. Wysokopoziomowe abstrakcje oraz sterowniki do interakcji z sprzętem są realizowane oddzielnie na poziomie użytkownika w postaci zadań. Dostęp tych zadań do zasobów mikrojądra jest organizowany poprzez określenie reguł.
Dla dodatkowej ochrony wszystkie komponenty, z wyjątkiem mikrojądra, są pierwotnie rozwijane w języku Rust z wykorzystaniem bezpiecznych praktyk programistycznych, minimalizujących błędy związane z operacjami na pamięci, prowadzące do takich problemów jak dostęp do obszaru pamięci po jej zwolnieniu, dereferencja wskaźników null i przekroczenie granic bufora. W Rust napisano również ładowarkę aplikacji w środowisku seL4, usługi systemowe, framework do tworzenia aplikacji, API do dostępu do wywołań systemowych, menedżera procesów, mechanizm dynamicznej alokacji pamięci itd. Do zweryfikowanej budowy wykorzystywane jest narzędzie CAmkES, rozwijane przez projekt seL4. Komponenty dla CAmkES również mogą być tworzone w języku Rust.
Bezpieczne operacje na pamięci są zapewnione w Rust podczas kompilacji dzięki sprawdzaniu wskaźników, śledzeniu własności obiektów oraz uwzględnianiu czasu życia obiektów (zakresu widoczności), a także dzięki ocenie poprawności dostępu do pamięci podczas wykonywania kodu. Rust oferuje również środki ochrony przed przepełnieniem liczb całkowitych, wymaga obowiązkowej inicjalizacji wartości zmiennych przed ich użyciem, stosuje koncepcję niemodyfikowalności (immutable) wskaźników i zmiennych domyślnie oraz oferuje silne statyczne typowanie, by zminimalizować błędy logiczne.
Źródło: opennet.ru
