Google wis ngumumake panemuan pangembangan sing ana gandhengane karo proyek KataOS, kanthi tujuan nggawe sistem operasi sing aman kanggo hardware sing dipasang. Komponen sistem KataOS ditulis ing Rust lan mbukak ing ndhuwur microkernel seL4, sing bukti matematika linuwih wis kasedhiya ing sistem RISC-V, nuduhake yen kode kebak tundhuk karo specifications kasebut ing basa formal. Kode proyek mbukak miturut lisensi Apache 2.0.
Sistem kasebut nyedhiyakake dhukungan kanggo platform adhedhasar arsitektur RISC-V lan ARM64. Kanggo simulasi operasi seL4 lan lingkungan KataOS ing ndhuwur hardware, framework Renode digunakake sak proses pembangunan. Minangka implementasi referensi, piranti lunak Sparrow lan kompleks hardware diusulake, nggabungake KataOS karo chip aman adhedhasar platform OpenTitan. Solusi sing diusulake ngidini sampeyan nggabungake kernel sistem operasi sing diverifikasi kanthi logis karo komponen hardware sing bisa dipercaya (RoT, Root of Trust), dibangun nggunakake platform OpenTitan lan arsitektur RISC-V. Saliyane kode KataOS, direncanakake mbukak kabeh komponen Sparrow liyane, kalebu komponen hardware, ing mangsa ngarep.
Platform kasebut dikembangake kanthi mripat kanggo aplikasi ing chip khusus sing dirancang kanggo mbukak aplikasi kanggo sinau mesin lan ngolah informasi rahasia, sing mbutuhake tingkat perlindungan khusus lan konfirmasi ora ana kegagalan. Conto aplikasi kasebut kalebu sistem sing ngapusi gambar wong lan rekaman swara. Panggunaan verifikasi linuwih saka KataOS mesthekake yen salah sawijining bagean saka sistem gagal, kegagalan kasebut ora bakal nyebar menyang sistem liyane lan, utamane, menyang kernel lan bagean kritis.
Arsitèktur seL4 misuwur kanggo mindhah bagéan kanggo ngatur sumber daya kernel menyang ruang panganggo lan nglamar alat kontrol akses sing padha kanggo sumber daya kaya kanggo sumber daya pangguna. Mikrokernel ora nyedhiyakake abstraksi tingkat dhuwur sing wis siap kanggo ngatur file, proses, sambungan jaringan, lan liya-liyane; nanging mung nyedhiyakake mekanisme minimal kanggo ngontrol akses menyang papan alamat fisik, interupsi, lan sumber daya prosesor. Abstraksi lan driver tingkat dhuwur kanggo sesambungan karo hardware diimplementasikake kanthi kapisah ing ndhuwur microkernel ing wangun tugas tingkat pangguna. Akses tugas kasebut menyang sumber daya sing kasedhiya kanggo microkernel diatur liwat definisi aturan.
Kanggo pangayoman tambahan, kabeh komponen kajaba microkernel dikembangaké native ing Rust nggunakake Techniques program aman sing nyilikake kasalahan memori sing mimpin kanggo masalah kayata akses memori sawise freeing, null pointer dereferences, lan buffer overruns. Loader aplikasi ing lingkungan seL4, layanan sistem, framework kanggo pangembangan aplikasi, API kanggo ngakses telpon sistem, manager proses, mekanisme kanggo alokasi memori dinamis, etc.. ditulis ing Rust. Déwan sing wis diverifikasi nggunakake toolkit CAmkES, sing dikembangake dening proyek seL4. Komponen kanggo CAmkES uga bisa digawe ing Rust.
Rust ngetrapake safety memori ing wektu kompilasi liwat mriksa referensi, kepemilikan obyek lan pelacakan umur obyek (skop), lan kanthi ngevaluasi akurasi akses memori nalika runtime. Rust uga menehi pangayoman marang overflows integer, mbutuhake nilai variabel kanggo diinisialisasi sadurunge digunakake, nggunakake konsep referensi lan variabel sing ora bisa diganti kanthi standar, lan nawakake ngetik statis sing kuat kanggo nyilikake kesalahan logis.
Source: opennet.ru