Gipahibalo sa Google ang pagkadiskobre sa mga kalamboan nga may kalabutan sa proyekto sa KataOS, nga gitumong sa paghimo sa usa ka luwas nga operating system alang sa embedded hardware. Ang mga sangkap sa sistema sa KataOS gisulat sa Rust ug gipadagan sa ibabaw sa seL4 microkernel, diin ang usa ka mathematical nga pruweba sa pagkakasaligan gihatag sa mga sistema sa RISC-V, nga nagpakita sa hingpit nga pagsunod sa code sa mga detalye nga gitakda sa pormal nga sinultian. Ang code sa proyekto bukas ubos sa lisensya sa Apache 2.0.
Ang sistema naghatag suporta alang sa mga plataporma base sa RISC-V ug ARM64 nga mga arkitektura. Aron masundog ang operasyon sa seL4 ug ang KataOS nga palibot sa ibabaw sa hardware, ang Renode framework gigamit sa panahon sa pag-uswag. Isip usa ka reperensiya nga pagpatuman, ang Sparrow hardware ug software system gisugyot, nga naghiusa sa KataOS nga adunay luwas nga mga chips base sa OpenTitan nga plataporma. Ang gisugyot nga solusyon nagpaposible sa paghiusa sa usa ka lohikal nga gipamatud-an nga kernel sa operating system nga adunay kasaligan nga mga sangkap sa hardware (RoT, Root of Trust) nga gitukod gamit ang OpenTitan platform ug ang RISC-V nga arkitektura. Dugang pa sa KataOS code, giplano nga ablihan ang tanan nga ubang mga sangkap sa Sparrow, lakip ang sangkap sa hardware, sa umaabot.
Ang plataporma gipalambo uban ang pagtan-aw sa mga chips nga gihimo sa katuyoan nga gidisenyo sa pagpadagan sa pagkat-on sa makina ug mga aplikasyon sa pagkapribado nga nanginahanglan usa ka piho nga lebel sa proteksyon ug kasiguruhan nga walaβy mga kapakyasan. Ang mga sistema nga nagmaniobra sa mga hulagway sa mga tawo ug mga pagrekord sa tingog gihatag isip usa ka pananglitan sa maong mga aplikasyon. Ang paggamit sa kasaligan nga pag-verify sa KataOS nagsiguro nga kung adunay kapakyasan sa usa ka bahin sa sistema, kini nga kapakyasan dili mokaylap sa nahabilin nga sistema ug, labi na, sa kernel ug kritikal nga mga bahin.
Ang seL4 nga arkitektura talagsaon alang sa paglihok sa mga bahin alang sa pagdumala sa mga kahinguhaan sa kernel ngadto sa luna sa user ug paggamit sa samang mga kontrol sa pag-access alang sa mga kapanguhaan sama sa mga kapanguhaan sa tiggamit. Ang microkernel wala maghatag ug out-of-the-box nga high-level abstraction para sa pagdumala sa mga file, proseso, koneksyon sa network, ug uban pa, sa baylo naghatag lang kini ug gamay nga mekanismo sa pagkontrolar sa access sa physical address space, interrupts, ug processor resources. Ang taas nga lebel nga abstraction ug mga drayber alang sa pagpakig-uban sa hardware gipatuman nga gilain sa ibabaw sa microkernel sa porma sa mga buluhaton sa lebel sa user. Ang pag-access sa ingon nga mga buluhaton sa mga kapanguhaan nga magamit sa microkernel giorganisar pinaagi sa kahulugan sa mga lagda.
Alang sa dugang nga proteksyon, ang tanan nga mga sangkap gawas sa microkernel sa sinugdan naugmad sa Rust gamit ang luwas nga mga teknik sa pagprograma nga nagpamenos sa mga sayup kung nagtrabaho uban ang panumduman, nga nagdala sa mga problema sama sa pag-access sa usa ka lugar sa panumduman pagkahuman kini gibuhian, pagtangtang sa mga null pointer, ug pag-overrun sa buffer. Ang loader sa aplikasyon sa palibot sa seL4, mga serbisyo sa sistema, usa ka balangkas sa pagpalambo sa aplikasyon, usa ka API alang sa pag-access sa mga tawag sa sistema, usa ka manager sa proseso, usa ka dinamikong mekanismo sa alokasyon sa memorya, ug uban pa gisulat sa Rust. Para sa napamatud-an nga asembliya, ang CAmkES toolkit nga gihimo sa seL4 nga proyekto gigamit. Ang mga sangkap alang sa CAmkES mahimo usab nga himuon sa Rust.
Ang kaluwasan sa memorya gihatag sa Rust sa oras sa pag-compile pinaagi sa pagsusi sa pakisayran, pagsubay sa pagpanag-iya sa butang ug kinabuhi sa butang (sakupan), ingon man pinaagi sa pagtimbang-timbang sa pagkahusto sa pag-access sa memorya sa panahon sa pagpatuman sa code. Naghatag usab ang Rust og proteksyon batok sa pag-awas sa integer, nanginahanglan nga magsugod ang mga variable sa dili pa gamiton, magamit ang konsepto sa dili mausab nga mga pakisayran ug mga variable nga default, ug nagtanyag kusog nga static nga pag-type aron maminusan ang mga lohikal nga sayup.
Source: opennet.ru