Mfumo wa uendeshaji salama wa chanzo huria wa Google KataOS

Google imetangaza ugunduzi wa maendeleo yanayohusiana na mradi wa KataOS, unaolenga kuunda mfumo salama wa uendeshaji wa maunzi yaliyopachikwa. Vipengee vya mfumo wa KataOS vimeandikwa kwa Kutu na huendeshwa juu ya kipaza sauti cha seL4, ambacho uthibitisho wa kihisabati wa kutegemewa umetolewa kwenye mifumo ya RISC-V, ikionyesha kuwa msimbo unatii kikamilifu vipimo vilivyobainishwa katika lugha rasmi. Nambari ya mradi imefunguliwa chini ya leseni ya Apache 2.0.

Mfumo hutoa usaidizi kwa majukwaa kulingana na usanifu wa RISC-V na ARM64. Ili kuiga utendakazi wa seL4 na mazingira ya KataOS juu ya maunzi, mfumo wa Renode hutumiwa wakati wa mchakato wa ukuzaji. Kama utekelezaji wa marejeleo, programu ya Sparrow na changamano ya maunzi inapendekezwa, ikichanganya KataOS na chipsi salama kulingana na jukwaa la OpenTitan. Suluhisho lililopendekezwa linakuwezesha kuchanganya kernel ya mfumo wa uendeshaji iliyothibitishwa kimantiki na vipengele vya kuaminika vya vifaa (RoT, Root of Trust), iliyojengwa kwa kutumia jukwaa la OpenTitan na usanifu wa RISC-V. Mbali na msimbo wa KataOS, imepangwa kufungua vipengele vingine vyote vya Sparrow, ikiwa ni pamoja na sehemu ya vifaa, katika siku zijazo.

Jukwaa linatengenezwa kwa jicho la utumiaji katika chipsi maalum iliyoundwa kutekeleza maombi ya kujifunza kwa mashine na kuchakata habari za siri, ambazo zinahitaji kiwango maalum cha ulinzi na uthibitisho wa kutokuwepo kwa mapungufu. Mifano ya programu kama hizi ni pamoja na mifumo inayodhibiti picha za watu na rekodi za sauti. Utumiaji wa uthibitishaji wa kuegemea wa KataOS huhakikisha kwamba ikiwa sehemu moja ya mfumo itashindwa, kutofaulu hakutaenea kwa mfumo wote na, haswa, kwa kernel na sehemu muhimu.

Usanifu wa seL4 unajulikana kwa kuhamisha sehemu za kudhibiti rasilimali za kernel kwenye nafasi ya mtumiaji na kutumia zana sawa za udhibiti wa ufikiaji kwa rasilimali kama vile rasilimali za watumiaji. Microkernel haitoi vifupisho vya kiwango cha juu vilivyotengenezwa tayari vya kudhibiti faili, michakato, miunganisho ya mtandao, na kadhalika; badala yake, hutoa njia ndogo tu za kudhibiti ufikiaji wa nafasi ya anwani halisi, kukatizwa na rasilimali za kichakataji. Vidokezo vya hali ya juu na viendeshaji vya kuingiliana na maunzi hutekelezwa kando juu ya maikrofoni kwa namna ya kazi za kiwango cha mtumiaji. Upatikanaji wa kazi hizo kwa rasilimali zinazopatikana kwa microkernel hupangwa kupitia ufafanuzi wa sheria.

Kwa ulinzi wa ziada, vijenzi vyote isipokuwa kipaza sauti hutengenezwa kiasili katika Kutu kwa kutumia mbinu salama za utayarishaji ambazo hupunguza hitilafu za kumbukumbu ambazo husababisha matatizo kama vile ufikiaji wa kumbukumbu baada ya kufungia, vielekezi visivyofaa vya vielekezi, na ziada ya bafa. Kipakiaji cha programu katika mazingira ya seL4, huduma za mfumo, mfumo wa ukuzaji wa programu, API ya kufikia simu za mfumo, meneja wa mchakato, utaratibu wa ugawaji kumbukumbu wa nguvu, n.k. ziliandikwa kwa Rust. Kusanyiko lililothibitishwa linatumia zana ya zana za CAmkES, iliyotengenezwa na mradi wa seL4. Vipengee vya CAmkES vinaweza pia kuundwa katika Rust.

Rust hutekeleza usalama wa kumbukumbu wakati wa kukusanya kupitia ukaguzi wa marejeleo, umiliki wa kitu na ufuatiliaji wa maisha ya kitu (wigo), na kwa kutathmini usahihi wa ufikiaji wa kumbukumbu wakati wa utekelezaji. Kutu pia hutoa ulinzi dhidi ya mafuriko kamili, inahitaji thamani tofauti kuanzishwa kabla ya matumizi, hutumia dhana ya marejeleo yasiyobadilika na vigeu kwa chaguomsingi, na hutoa uchapaji thabiti wa tuli ili kupunguza makosa ya kimantiki.

Chanzo: opennet.ru

Kuongeza maoni