Google heeft aangekondigd dat het de resultaten van het KataOS-project vrijgeeft, dat gericht is op het ontwikkelen van een beveiligd besturingssysteem voor ingebedde apparatuur. De systeemcomponenten van KataOS zijn geschreven in Rust en draaien bovenop de microkernel seL4, waarvoor op RISC-V-systemen een wiskundig bewijs van betrouwbaarheid is geleverd dat aantoont dat de code volledig voldoet aan de specificaties die zijn vastgesteld in een formele taal. De code van het project is openbaar onder de Apache 2.0-licentie.
Het systeem biedt ondersteuning voor platforms gebaseerd op RISC-V en ARM64-architecturen. Voor het simuleren van de werking van seL4 en de omgeving van KataOS bovenop de hardware tijdens de ontwikkeling wordt het Renode-framework gebruikt. Als referentie-implementatie is het software-hardwarecombinatie Sparrow voorgesteld, dat KataOS combineert met beveiligde chipsets op basis van het OpenTitan-platform. De voorgestelde aanpak maakt het mogelijk om een logisch geverifieerde kern van het besturingssysteem te combineren met betrouwbare hardwarecomponenten (RoT, Root of Trust), die zijn gebouwd met behulp van het OpenTitan-platform en de RISC-V-architectuur. Naast de code van KataOS is het de bedoeling om ook alle andere componenten van Sparrow, inclusief de hardware, in de toekomst openbaar te maken.
Het platform wordt ontwikkeld met het oog op gebruik in gespecialiseerde chips die zijn ontworpen voor het uitvoeren van toepassingen voor machine learning en het verwerken van gevoelige informatie, waarop een bijzonder niveau van bescherming en een bevestiging van foutloosheid vereist is. Voorbeelden van dergelijke toepassingen zijn systemen die afbeeldingen van mensen en geluidsopnamen manipuleren. Het gebruik van verificatie van betrouwbaarheid in KataOS garandeert dat als er een fout optreedt in een deel van het systeem, deze fout niet zal verspreiden naar de rest van het systeem en met name niet naar de kern en kritische delen.
De architectuur van seL4 valt op door het verplaatsen van delen voor de resourcebeheer van de kernel naar de gebruikersruimte en het toepassen van dezelfde toegangsbeheermiddelen voor deze resources als voor gebruikersresources. De microkernel biedt geen kant-en-klare hoog-niveau abstracties voor het beheren van bestanden, processen, netwerkverbindingen, enz., maar biedt slechts minimale mechanismen voor het beheren van toegang tot de fysieke adresruimte, interrupties en CPU-resources. Hoog-niveau abstracties en stuurprogramma's voor interactie met hardware worden apart bovenop de microkernel geĆÆmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd. De toegang van deze taken tot de resources van de microkernel wordt georganiseerd via het definiĆ«ren van regels.
Voor extra bescherming worden alle componenten, behalve de microkernel, oorspronkelijk ontwikkeld in de programmeertaal Rust met behulp van veilige programmeerpraktijken die fouten bij het omgaan met geheugen minimaliseren, zoals het aanspreken van geheugen na de vrijgave, het dereferencen van null pointers en buffer overflows. Onder andere is de applicatielader in de seL4-omgeving, systeemdiensten, een framework voor applicatieontwikkeling, API's voor toegang tot systeemoproepen, procesbeheerders, dynamische geheugenallocatiemechanismen, enz. in Rust geschreven. Voor de geverifieerde constructie wordt het CAmkES-gereedschap gebruikt, dat wordt ontwikkeld door het seL4-project. Componenten voor CAmkES kunnen ook in de programmeertaal Rust worden gemaakt.
Veilig geheugenbeheer wordt in Rust tijdens de compilatie gewaarborgd door het controleren van referenties, het bijhouden van eigendom van objecten en het in overweging nemen van de levensduur van objecten (scope), evenals door de correctheid van geheugenaccess tijdens het uitvoeren van code te beoordelen. Rust biedt ook middelen ter bescherming tegen integer overflows, vereist verplichte initialisatie van variabelen vĆ³Ć³r gebruik, past het concept van ongewijzigde (immutable) referenties en variabelen standaard toe, en biedt sterke statische typechecking om logische fouten te minimaliseren.
Bron: opennet.ru
