Google ngumumkeun panemuan kamajuan anu aya hubunganana sareng proyék KataOS, anu ditujukeun pikeun nyiptakeun sistem operasi anu aman pikeun hardware anu dipasang. Komponén sistem KataOS ditulis dina Rust tur dijalankeun dina luhureun mikrokernel seL4, nu hiji bukti matematis reliabiliti disadiakeun dina sistem RISC-V, nunjukkeun minuhan pinuh kode jeung spésifikasi dieusian dina basa formal. Kodeu proyék dibuka dina lisénsi Apache 2.0.
Sistem ieu nyayogikeun dukungan pikeun platform dumasar kana arsitéktur RISC-V sareng ARM64. Pikeun simulate operasi seL4 sareng lingkungan KataOS di luhur hardware, kerangka Renode dianggo nalika pangwangunan. Salaku palaksanaan rujukan, diusulkeun Sparrow hardware jeung software sistem, nu ngagabungkeun KataOS kalawan chip aman dumasar kana platform OpenTitan. Solusi anu diusulkeun ngamungkinkeun pikeun ngagabungkeun kernel sistem operasi anu diverifikasi sacara logis sareng komponén hardware anu dipercaya (RoT, Root of Trust) diwangun nganggo platform OpenTitan sareng arsitektur RISC-V. Salian kodeu KataOS, rencanana pikeun muka sadaya komponén Sparrow anu sanés, kalebet komponén hardware, di hareup.
Platform ieu dikembangkeun kalayan merhatikeun chip anu didamel khusus anu dirancang pikeun ngajalankeun pembelajaran mesin sareng aplikasi privasi anu meryogikeun tingkat panyalindungan khusus sareng jaminan yén teu aya anu gagal. Sistem anu ngamanipulasi gambar jalma sareng rékaman sora dirumuskeun salaku conto aplikasi sapertos kitu. Pamakéan verifikasi reliabilitas dina KataOS mastikeun yén upami aya kagagalan dina hiji bagian sistem, kagagalan ieu henteu sumebar ka sistem anu sanés sareng, khususna, ka kernel sareng bagian kritis.
Arsitéktur seL4 kasohor pikeun mindahkeun bagian pikeun ngatur sumber kernel kana rohangan pangguna sareng nerapkeun kadali aksés anu sami pikeun sumber daya sapertos sumberdaya pangguna. Mikrokernel teu nyadiakeun kaluar-of-the-box abstraksi tingkat luhur pikeun ngatur file, prosés, sambungan jaringan, jeung sajabana, malah nyadiakeun ngan mékanisme minimal keur ngadalikeun aksés ka spasi alamat fisik, interrupts, sarta sumberdaya processor. Abstraksi tingkat luhur sareng supir pikeun berinteraksi sareng hardware dilaksanakeun sacara misah di luhur mikrokernel dina bentuk tugas tingkat pangguna. Aksés tugas sapertos kana sumber daya anu aya pikeun mikrokernel dikelompokeun ngaliwatan definisi aturan.
Pikeun panangtayungan tambahan, sakabéh komponén iwal microkernel mimitina dimekarkeun dina Rust ngagunakeun téhnik programming aman nu ngaleutikan kasalahan nalika gawé bareng memori, ngarah kana masalah kayaning ngakses wewengkon memori sanggeus dibébaskeun, dereferencing null pointers, sarta overruns panyangga. Karat dipaké, antara séjén, pikeun loader aplikasi dina lingkungan seL4, jasa sistem, hiji kerangka ngembangkeun aplikasi, hiji API pikeun nelepon sistem aksés, manajer prosés, mékanisme pikeun alokasi memori dinamis, jsb. Pikeun rakitan anu diverifikasi, toolkit CAmkES anu dikembangkeun ku proyék seL4 dianggo. Komponén pikeun CAmkES ogé tiasa didamel dina Rust.
Kasalametan memori disadiakeun dina Rust dina waktos compile ngaliwatan mariksa rujukan, ngalacak kapamilikan obyék sarta hirupna objék (wengkuan), kitu ogé ngaliwatan evaluasi correctness aksés memori salila palaksanaan kode. Karat ogé nyadiakeun panyalindungan ngalawan overflows integer, merlukeun variabel bisa initialized saméméh pamakéan, nerapkeun konsép rujukan immutable sarta variabel sacara standar, sarta nawarkeun ketikan statik kuat pikeun ngaleutikan kasalahan logis.
sumber: opennet.ru