Google te anonse dekouvèt devlopman ki gen rapò ak pwojè KataOS, ki vize a kreye yon sistèm operasyon an sekirite pou pyès ki nan konpitè entegre. Konpozan sistèm KataOS yo ekri nan Rust epi yo kouri sou tèt mikrokernel seL4 la, pou sa yo te bay yon prèv matematik sou fyab sou sistèm RISC-V, ki endike ke kòd la konplètman konfòm ak espesifikasyon yo espesifye nan lang fòmèl la. Kòd pwojè a louvri anba lisans Apache 2.0.
Sistèm nan bay sipò pou platfòm ki baze sou achitekti RISC-V ak ARM64. Pou simulation operasyon an nan seL4 ak anviwònman an KataOS sou tèt pyès ki nan konpitè, yo itilize fondasyon Renode pandan pwosesis devlopman an. Kòm yon aplikasyon referans, Sparrow lojisyèl ak pyès ki nan konpitè konplèks yo pwopoze, konbine KataOS ak chips an sekirite ki baze sou platfòm OpenTitan la. Solisyon yo pwopoze a pèmèt ou konbine yon nwayo sistèm opere lojikman verifye ak konpozan kenkayri ou fè konfyans (RoT, Root of Trust), ki te konstwi lè l sèvi avèk platfòm OpenTitan ak achitekti RISC-V. Anplis kòd KataOS la, li planifye pou louvri tout lòt konpozan Sparrow, ki gen ladan eleman pyès ki nan konpitè, alavni.
Platfòm nan ap devlope ak yon je nan aplikasyon nan chips espesyalize ki fèt pou kouri aplikasyon pou aprantisaj machin ak trete enfòmasyon konfidansyèl, ki mande pou yon nivo espesyal nan pwoteksyon ak konfimasyon nan absans la nan echèk. Egzanp aplikasyon sa yo enkli sistèm ki manipile imaj moun ak anrejistreman vwa. KataOS sèvi ak verifikasyon fyab asire ke si yon pati nan sistèm nan echwe, echèk la pa pral gaye nan rès la nan sistèm nan ak, an patikilye, nan nwayo a ak pati kritik yo.
Achitekti seL4 remakab pou deplase pati pou jere resous nwayo nan espas itilizatè yo epi aplike menm zouti kontwòl aksè pou resous sa yo tankou pou resous itilizatè yo. Mikrokernel la pa bay abstraksyon wo nivo pare pou jere fichye, pwosesis, koneksyon rezo, ak lòt bagay; olye de sa, li bay sèlman mekanis minim pou kontwole aksè nan espas adrès fizik, entèwonp, ak resous processeur. Abstraksyon wo nivo ak chofè pou kominike avèk pyès ki nan konpitè yo aplike separeman sou tèt mikrokernel la nan fòm travay nan nivo itilizatè. Aksè travay sa yo nan resous ki disponib nan mikrokernel la òganize atravè definisyon règ yo.
Pou plis pwoteksyon, tout eleman eksepte mikrokernel yo devlope natif natal nan Rust lè l sèvi avèk teknik pwogramasyon ki an sekirite ki minimize erè memwa ki mennen nan pwoblèm tankou aksè memwa apre yo fin libere, dereferans pointer nil, ak depase tanpon. Yon chajè aplikasyon nan anviwònman an seL4, sèvis sistèm, yon fondasyon pou devlopman aplikasyon, yon API pou jwenn aksè nan apèl sistèm, yon manadjè pwosesis, yon mekanis pou alokasyon memwa dinamik, elatriye yo te ekri nan Rust. Asanble verifye a sèvi ak zouti CAmkES, pwojè seL4 devlope. Konpozan pou CAmkES ka kreye tou nan Rust.
Rust ranfòse sekirite memwa nan moman konpile atravè tcheke referans, pwopriyetè objè ak swiv objè pou tout lavi (dimansyon), epi pa evalye kòrèkteman nan aksè memwa nan ègzekutabl. Rust tou bay pwoteksyon kont debòde nonb antye relatif, mande pou valè varyab yo dwe inisyalize anvan ou itilize, sèvi ak konsèp nan referans imuiabl ak varyab pa default, epi li ofri fò sezisman estatik pou minimize erè lojik.
Sous: opennet.ru