Google het die ontdekking aangekondig van ontwikkelings wat verband hou met die KataOS-projek, wat daarop gemik is om 'n veilige bedryfstelsel vir ingebedde hardeware te skep. KataOS-stelselkomponente is in Rust geskryf en loop bo-op die seL4-mikrokern, waarvoor 'n wiskundige bewys van betroubaarheid op RISC-V-stelsels verskaf is, wat aandui dat die kode ten volle voldoen aan die spesifikasies wat in die formele taal gespesifiseer word. Die projekkode is oop onder die Apache 2.0-lisensie.
Die stelsel bied ondersteuning vir platforms gebaseer op RISC-V- en ARM64-argitekture. Om die werking van seL4 en die KataOS-omgewing bo-op die hardeware te simuleer, word die Renode-raamwerk tydens die ontwikkelingsproses gebruik. As 'n verwysingsimplementering word die Sparrow-sagteware- en hardewarekompleks voorgestel, wat KataOS kombineer met veilige skyfies gebaseer op die OpenTitan-platform. Die voorgestelde oplossing laat jou toe om 'n logies geverifieerde bedryfstelselkern te kombineer met betroubare hardeware-komponente (RoT, Root of Trust), gebou met behulp van die OpenTitan-platform en RISC-V-argitektuur. Benewens die KataOS-kode, word beplan om alle ander Sparrow-komponente, insluitend die hardeware-komponent, in die toekoms oop te maak.
Die platform word ontwikkel met die oog op toepassing in gespesialiseerde skyfies wat ontwerp is om toepassings vir masjienleer en die verwerking van vertroulike inligting uit te voer, wat 'n spesiale vlak van beskerming en bevestiging van die afwesigheid van mislukkings vereis. Voorbeelde van sulke toepassings sluit in stelsels wat beelde van mense en stemopnames manipuleer. KataOS se gebruik van betroubaarheidsverifikasie verseker dat as een deel van die stelsel misluk, die mislukking nie na die res van die stelsel sal versprei nie en veral na die kern en kritieke dele.
Die seL4-argitektuur is opvallend vir bewegende dele vir die bestuur van kernhulpbronne in gebruikersruimte en die toepassing van dieselfde toegangsbeheernutsmiddels vir sulke hulpbronne as vir gebruikershulpbronne. Die mikrokern verskaf nie klaargemaakte hoëvlak-abstraksies vir die bestuur van lêers, prosesse, netwerkverbindings en dies meer nie; in plaas daarvan bied dit slegs minimale meganismes vir die beheer van toegang tot fisiese adresruimte, onderbrekings en verwerkerhulpbronne. Hoëvlak-abstraksies en drywers vir interaksie met hardeware word afsonderlik bo-op die mikrokern geïmplementeer in die vorm van gebruikersvlaktake. Toegang van sulke take tot die hulpbronne beskikbaar vir die mikrokern word georganiseer deur die definisie van reëls.
Vir bykomende beskerming word alle komponente behalwe die mikrokern inheems in Rust ontwikkel deur veilige programmeringstegnieke te gebruik wat geheuefoute verminder wat lei tot probleme soos geheuetoegang na vrystelling, nulwyserverwysings en bufferoorskryding. 'n Toepassingslaaier in die seL4-omgewing, stelseldienste, 'n raamwerk vir toepassingsontwikkeling, 'n API vir toegang tot stelseloproepe, 'n prosesbestuurder, 'n meganisme vir dinamiese geheuetoewysing, ens. is in Rust geskryf. Die geverifieerde samestelling gebruik die CAmkES-gereedskapstel, ontwikkel deur die seL4-projek. Komponente vir CAmkES kan ook in Rust geskep word.
Rust dwing geheueveiligheid af tydens samestellingstyd deur verwysingkontrolering, objekeienaarskap en objekleeftydnasporing (bestekke), en deur die korrektheid van geheuetoegange tydens looptyd te evalueer. Roes bied ook beskerming teen heelgetal oorvloei, vereis dat veranderlike waardes geïnisialiseer word voor gebruik, gebruik die konsep van onveranderlike verwysings en veranderlikes by verstek, en bied sterk statiese tik om logiese foute te minimaliseer.
Bron: opennet.ru