KataOS, een embedded hardware-beveiligingsgericht besturingssysteem.
Het nieuws werd vrijgegeven dat Google heeft de release aangekondigd van de broncode van ontwikkelingen met betrekking tot het project Kata OS, wiens doel het is om een veilig besturingssysteem voor embedded hardware.
Het systeem biedt ondersteuning voor platforms op basis van RISC-V- en ARM64-architecturen. Om tijdens de ontwikkeling de werking van seL4 en de KataOS-omgeving op hardware te simuleren, wordt het Renode-framework gebruikt.
Als referentie-implementatie wordt het Sparrow-software- en hardwarecomplex voorgesteld, dat KataOS combineert met veilige chips op basis van het OpenTitan-platform. De voorgestelde oplossing hHet is mogelijk om een kernel te combineren logisch geverifieerd besturingssysteem met ingebouwde Root of Trust (RoT) hardwarecomponenten met behulp van het OpenTitan-platform en de RISC-V-architectuur.
Naast de KataOS-code is het de bedoeling om in de toekomst alle andere Sparrow-componenten, inclusief de hardwarecomponent, open te stellen.
Als basis voor dit nieuwe besturingssysteem hebben we seL4 gekozen als de microkernel omdat het veiligheid voorop stelt; het is wiskundig bewezen dat het veilig is, met gegarandeerde vertrouwelijkheid, integriteit en beschikbaarheid. Via het seL4 CAmkES-framework kunnen we ook statisch gedefinieerde en parseerbare systeemcomponenten leveren. KataOS biedt een verifieerbaar veilig platform dat de privacy van gebruikers beschermt, omdat het logischerwijs onmogelijk is voor toepassingen om de hardwarebeveiliging van de kernel en verifieerbare veilige systeemcomponenten te schenden.
Het platform wordt ontwikkeld met chips in gedachten vooral ontworpen om privacy- en machine learning-applicaties uit te voeren die een specifiek beschermingsniveau vereisen en garanderen dat er geen storingen zijn. Als voorbeeld van dergelijke toepassingen worden systemen gegeven die afbeeldingen van mensen en spraakopnamen manipuleren. Het gebruik van betrouwbaarheidscontrole in KataOS zorgt ervoor dat in het geval van een storing in een deel van het systeem, deze storing zich niet verspreidt naar de rest van het systeem en in het bijzonder naar de kernel en kritische delen.
architectuur seL4 blinkt uit in bewegende delen om kernelbronnen te beheren in gebruikersruimte en pas dezelfde toegangscontrole toe voor die bronnen als voor gebruikersbronnen.
De microkernel biedt geen abstracties op hoog niveau kant-en-klaar om bestanden, processen, netwerkverbindingen en dergelijke te beheren, maar biedt slechts minimale mechanismen voor het regelen van toegang tot fysieke adresruimte, interrupts en processorbronnen. Abstracties op hoog niveau en stuurprogramma's voor interactie met de hardware worden afzonderlijk bovenop de microkernel geïmplementeerd in de vorm van taken op gebruikersniveau. De toegang van dergelijke taken tot de bronnen die beschikbaar zijn voor de microkernel wordt georganiseerd door de definitie van regels.
Voor extra bescherming, alle componenten behalve de microkernel zijn in eerste instantie ontwikkeld in Rust het gebruik van veilige programmeertechnieken die fouten minimaliseren bij het werken met geheugen, wat leidt tot problemen zoals toegang tot een geheugengebied nadat het is vrijgemaakt, verwijzing naar null-pointers en bufferoverloop.
De applicatielader in de seL4-omgeving, systeemservices, een applicatieontwikkelingsraamwerk, een API om toegang te krijgen tot systeemaanroepen, een procesmanager, een dynamisch geheugentoewijzingsmechanisme, enz. ze zijn geschreven in Rust. Voor de geverifieerde montage wordt de door het seL4-project ontwikkelde CAmkES-toolkit gebruikt. Componenten voor CAmkES kunnen ook in Rust worden gemaakt.
Geheugenbeveiliging is voorzien in Rust tijdens het compileren door referenties te controleren, objecteigendom en objectlevensduur (scope) bij te houden, evenals door de juistheid van geheugentoegang tijdens code-uitvoering te evalueren. Rust biedt ook integer overloopbeveiliging, vereist dat variabelen vóór gebruik worden geïnitialiseerd, dwingt het concept van onveranderlijke variabelen en verwijzingen standaard af en biedt sterk statisch typen om logische fouten te minimaliseren.
Tot slot, voor de geïnteresseerden, moet je weten dat de componenten van het KataOS-systeem zijn geschreven in Rust en draaien op de seL4-microkernel, waarvoor een wiskundig bewijs van betrouwbaarheid in RISC-V-systemen wordt geleverd, wat aangeeft dat de code volledig voldoet aan de specificaties gespecificeerd in de formele taal.
De projectcode is open onder de Apache 2.0-licentie, u kunt er meer informatie over raadplegen in de volgende link.