Google ngeculake kode sumber proyek KataOS

Kabar iki dirilis sing Google ngumumake release kode sumber saka pembangunan related kanggo project Kata OS, sing tujuane nggawe sistem operasi aman kanggo hardware ditempelake.

Sistem kasebut nyedhiyakake dhukungan kanggo platform adhedhasar arsitektur RISC-V lan ARM64. Kanggo simulasi operasi seL4 lan lingkungan KataOS ing hardware sak pembangunan, framework Renode digunakake.

Minangka implementasi referensi, piranti lunak Sparrow lan kompleks hardware diusulake, sing nggabungake KataOS karo chip aman adhedhasar platform OpenTitan. Solusi sing diusulake hSampeyan bisa gabungke kernel sistem operasi logis diverifikasi karo ROOT saka Trust (RoT) komponen hardware dibangun nggunakake platform OpenTitan lan arsitektur RISC-V.

Saliyane kode KataOS, direncanakake bakal mbukak kabeh komponen Sparrow liyane, kalebu komponen hardware, ing mangsa ngarep.

Minangka basis kanggo sistem operasi anyar iki, kita milih seL4 minangka microkernel amarga ndadekake keamanan ngarep lan tengah; wis kabukten kanthi matematis aman, kanthi rahasia, integritas, lan kasedhiyan dijamin. Liwat kerangka seL4 CAmkES, kita uga bisa nyedhiyakake komponen sistem sing ditetepake kanthi statis lan parsable. KataOS nyedhiyakake platform aman sing bisa diverifikasi sing nglindhungi privasi pangguna amarga ora mungkin aplikasi nglanggar proteksi keamanan hardware kernel lan komponen sistem aman sing bisa diverifikasi.

Platform kasebut dikembangake kanthi mikir babagan chip utamane dirancang kanggo mbukak privasi lan aplikasi machine learning sing mbutuhake tingkat pangayoman tartamtu lan njamin yen ora ana kegagalan. Sistem sing ngapusi gambar wong lan rekaman swara diwenehi minangka conto aplikasi kasebut. Panggunaan mriksa linuwih ing KataOS njamin yen ana kegagalan ing salah sawijining bagean sistem, kegagalan iki ora nyebar menyang sistem liyane lan utamane menyang kernel lan bagean kritis.

Arsitektur seL4 unggul ing bagean obah kanggo ngatur sumber daya kernel ing ruang pangguna lan aplikasi kontrol akses sing padha kanggo sumber daya kasebut kanggo sumber daya pangguna.

Mikrokernel ora nyedhiyakake abstraksi tingkat dhuwur out-of-the-box kanggo ngatur file, proses, sambungan jaringan, lan liya-liyane, nanging mung nyedhiyakake mekanisme minimal kanggo ngontrol akses menyang papan alamat fisik, interrupts, 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 perlindungan ekstra, kabeh komponen kajaba microkernel pisanan dikembangaké ing Rust nggunakake teknik pemrograman sing aman sing nyilikake kesalahan nalika nggarap memori, sing nyebabake masalah kayata ngakses area memori sawise dibebasake, dereferensi null pointer, lan buffer overflow.

Pemuat aplikasi ing lingkungan seL4, layanan sistem, kerangka pangembangan aplikasi, API kanggo ngakses panggilan sistem, manajer proses, mekanisme alokasi memori dinamis, lsp. padha ditulis ing Rust. Kanggo perakitan sing wis diverifikasi, toolkit CAmkES sing dikembangake dening proyek seL4 digunakake. Komponen kanggo CAmkES uga bisa digawe ing Rust.

Keamanan memori diwenehake ing Rust ing wektu kompilasi kanthi mriksa referensi, nelusuri kepemilikan obyek, lan umur obyek (ruang lingkup), uga kanthi ngevaluasi kabeneran akses memori sajrone eksekusi kode. Rust uga menehi proteksi overflow integer, mbutuhake variabel diinisialisasi sadurunge digunakake, ngetrapake konsep variabel lan referensi sing ora bisa diganti kanthi standar, lan nyedhiyakake ngetik statis sing kuat kanggo nyilikake kesalahan logika.

Pungkasan kanggo sing kasengsem, sampeyan kudu ngerti manawa komponen sistem KataOS ditulis ing Rust lan mbukak ing mikrokernel seL4, sing menehi bukti linuwih matematika ing sistem RISC-V, sing nuduhake kode kasebut tundhuk karo spesifikasi. ditetepake ing basa resmi.

Kode proyek mbukak ing lisensi Apache 2.0, sampeyan bisa takon rincian liyane babagan ing link ing ngisor iki.