Google heeft de ontdekking aangekondigd van ontwikkelingen gerelateerd aan het KataOS-project, gericht op het creëren van een veilig besturingssysteem voor embedded hardware. KataOS-systeemcomponenten zijn geschreven in Rust en draaien bovenop de seL4-microkernel, waarvoor een wiskundig bewijs van betrouwbaarheid is geleverd op RISC-V-systemen, wat aangeeft dat de code volledig voldoet aan de specificaties gespecificeerd in de formele taal. De projectcode is geopend onder de Apache 2.0-licentie.
Het systeem biedt ondersteuning voor platforms gebaseerd op RISC-V- en ARM64-architecturen. Om de werking van seL4 en de KataOS-omgeving bovenop de hardware te simuleren, wordt tijdens het ontwikkelproces gebruik gemaakt van het Renode-framework. Als referentie-implementatie wordt het Sparrow software- en hardwarecomplex voorgesteld, waarbij KataOS wordt gecombineerd met veilige chips op basis van het OpenTitan-platform. Met de voorgestelde oplossing kunt u een logisch geverifieerde besturingssysteemkernel combineren met betrouwbare hardwarecomponenten (RoT, Root of Trust), gebouwd met behulp van het OpenTitan-platform en RISC-V-architectuur. Het is de bedoeling dat naast de KataOS-code in de toekomst alle andere Sparrow-componenten, inclusief de hardwarecomponent, worden geopend.
Het platform wordt ontwikkeld met het oog op toepassing in gespecialiseerde chips die zijn ontworpen voor het uitvoeren van toepassingen voor machinaal leren en het verwerken van vertrouwelijke informatie, die een speciaal niveau van bescherming en bevestiging van de afwezigheid van fouten vereisen. Voorbeelden van dergelijke toepassingen zijn systemen die afbeeldingen van mensen en stemopnames manipuleren. Het gebruik van betrouwbaarheidsverificatie door KataOS zorgt ervoor dat als een deel van het systeem uitvalt, de fout zich niet zal verspreiden naar de rest van het systeem en in het bijzonder naar de kernel en kritieke delen.
De seL4-architectuur valt op door het verplaatsen van onderdelen voor het beheren van kernelbronnen naar de gebruikersruimte en het toepassen van dezelfde toegangscontroletools voor dergelijke bronnen als voor gebruikersbronnen. De microkernel biedt geen kant-en-klare abstracties op hoog niveau voor het beheren van bestanden, processen, netwerkverbindingen en dergelijke; in plaats daarvan biedt het slechts minimale mechanismen voor het controleren van de toegang tot fysieke adresruimte, interrupts en processorbronnen. Abstracties op hoog niveau en stuurprogramma's voor interactie met 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 het definiëren van regels.
Voor extra bescherming zijn alle componenten behalve de microkernel native ontwikkeld in Rust met behulp van veilige programmeertechnieken die geheugenfouten minimaliseren die leiden tot problemen zoals geheugentoegang na het vrijmaken, null pointer-dereferenties en bufferoverruns. Een applicatielader in de seL4-omgeving, systeemdiensten, een raamwerk voor applicatieontwikkeling, een API voor toegang tot systeemoproepen, een procesmanager, een mechanisme voor dynamische geheugentoewijzing, enz. Zijn geschreven in Rust. De geverifieerde assemblage maakt gebruik van de CAmkES-toolkit, ontwikkeld door het seL4-project. Componenten voor CAmkES kunnen ook in Rust worden gemaakt.
Rust dwingt de geheugenveiligheid af tijdens het compileren door referentiecontrole, objecteigendom en het volgen van de levensduur van objecten (scopes), en door de juistheid van geheugentoegang tijdens runtime te evalueren. Rust biedt ook bescherming tegen overflows van gehele getallen, vereist dat variabelewaarden vóór gebruik worden geïnitialiseerd, gebruikt standaard het concept van onveranderlijke referenties en variabelen en biedt sterke statische typering om logische fouten te minimaliseren.
Bron: opennet.ru