Mae Google wedi cyhoeddi darganfyddiad datblygiadau sy'n ymwneud â phrosiect KataOS, gyda'r nod o greu system weithredu ddiogel ar gyfer caledwedd wedi'i fewnosod. Mae cydrannau system KataOS wedi'u hysgrifennu yn Rust ac yn rhedeg ar ben y microkernel seL4, y mae prawf mathemategol o ddibynadwyedd wedi'i ddarparu ar ei gyfer ar systemau RISC-V, sy'n nodi bod y cod yn cydymffurfio'n llawn â'r manylebau a nodir yn yr iaith ffurfiol. Mae cod y prosiect ar agor o dan drwydded Apache 2.0.
Mae'r system yn darparu cefnogaeth i lwyfannau sy'n seiliedig ar bensaernïaeth RISC-V ac ARM64. Er mwyn efelychu gweithrediad seL4 ac amgylchedd KataOS ar ben y caledwedd, defnyddir fframwaith Renode yn ystod y broses ddatblygu. Fel gweithrediad cyfeirio, cynigir cyfadeilad meddalwedd a chaledwedd Sparrow, gan gyfuno KataOS â sglodion diogel yn seiliedig ar lwyfan OpenTitan. Mae'r datrysiad arfaethedig yn caniatáu ichi gyfuno cnewyllyn system weithredu wedi'i wirio'n rhesymegol â chydrannau caledwedd dibynadwy (RoT, Root of Trust), a adeiladwyd gan ddefnyddio platfform OpenTitan a phensaernïaeth RISC-V. Yn ogystal â'r cod KataOS, bwriedir agor yr holl gydrannau Sparrow eraill, gan gynnwys y gydran caledwedd, yn y dyfodol.
Mae'r platfform yn cael ei ddatblygu gyda llygad ar gymhwyso mewn sglodion arbenigol sydd wedi'u cynllunio i redeg cymwysiadau ar gyfer dysgu peiriannau a phrosesu gwybodaeth gyfrinachol, sy'n gofyn am lefel arbennig o amddiffyniad a chadarnhad o absenoldeb methiannau. Mae enghreifftiau o gymwysiadau o'r fath yn cynnwys systemau sy'n trin delweddau o bobl a recordiadau llais. Mae defnydd KataOS o wirio dibynadwyedd yn sicrhau, os bydd un rhan o'r system yn methu, na fydd y methiant yn lledaenu i weddill y system ac, yn benodol, i'r cnewyllyn a'r rhannau critigol.
Mae pensaernïaeth seL4 yn nodedig am symud rhannau ar gyfer rheoli adnoddau cnewyllyn i ofod defnyddwyr a chymhwyso'r un offer rheoli mynediad ar gyfer adnoddau o'r fath ag ar gyfer adnoddau defnyddwyr. Nid yw'r microcnewyllyn yn darparu tyniadau lefel uchel parod ar gyfer rheoli ffeiliau, prosesau, cysylltiadau rhwydwaith, ac ati; yn lle hynny, dim ond ychydig iawn o fecanweithiau y mae'n eu darparu ar gyfer rheoli mynediad i ofod cyfeiriad ffisegol, ymyriadau ac adnoddau prosesydd. Mae tyniadau lefel uchel a gyrwyr ar gyfer rhyngweithio â chaledwedd yn cael eu gweithredu ar wahân ar ben y microkernel ar ffurf tasgau lefel defnyddiwr. Trefnir mynediad tasgau o'r fath i'r adnoddau sydd ar gael i'r microkernel trwy ddiffiniad rheolau.
Ar gyfer amddiffyniad ychwanegol, mae'r holl gydrannau ac eithrio'r microkernel yn cael eu datblygu'n frodorol yn Rust gan ddefnyddio technegau rhaglennu diogel sy'n lleihau gwallau cof sy'n arwain at broblemau megis mynediad cof ar ôl rhyddhau, dadgyfeiriadau pwyntydd null, a gor-redeg byffer. Ysgrifennwyd llwythwr cymhwysiad yn amgylchedd seL4, gwasanaethau system, fframwaith ar gyfer datblygu cymwysiadau, API ar gyfer cyrchu galwadau system, rheolwr proses, mecanwaith ar gyfer dyrannu cof deinamig, ac ati yn Rust. Mae'r cynulliad a ddilyswyd yn defnyddio pecyn cymorth CAMkES, a ddatblygwyd gan y prosiect seL4. Gellir creu cydrannau ar gyfer CAMkES yn Rust hefyd.
Mae Rust yn gorfodi diogelwch cof ar amser llunio trwy wirio cyfeiriadau, perchnogaeth gwrthrych ac olrhain oes gwrthrych (scopes), a thrwy werthuso cywirdeb mynediadau cof ar amser rhedeg. Mae Rust hefyd yn darparu amddiffyniad rhag gorlifiadau cyfanrif, yn ei gwneud yn ofynnol i werthoedd newidiol gael eu cychwyn cyn eu defnyddio, yn defnyddio'r cysyniad o gyfeiriadau a newidynnau na ellir eu cyfnewid yn ddiofyn, ac yn cynnig teipio statig cryf i leihau gwallau rhesymegol.
Ffynhonnell: opennet.ru