Google telah mengumumkan penemuan perkembangan yang berkaitan dengan projek KataOS, bertujuan untuk mencipta sistem pengendalian yang selamat untuk perkakasan terbenam. Komponen sistem KataOS ditulis dalam Rust dan dijalankan di atas mikrokernel seL4, yang mana bukti kebolehpercayaan matematik telah disediakan pada sistem RISC-V, menunjukkan bahawa kod tersebut mematuhi sepenuhnya spesifikasi yang dinyatakan dalam bahasa formal. Kod projek dibuka di bawah lesen Apache 2.0.
Sistem ini menyediakan sokongan untuk platform berdasarkan seni bina RISC-V dan ARM64. Untuk mensimulasikan operasi seL4 dan persekitaran KataOS di atas perkakasan, rangka kerja Renode digunakan semasa proses pembangunan. Sebagai pelaksanaan rujukan, kompleks perisian dan perkakasan Sparrow dicadangkan, menggabungkan KataOS dengan cip selamat berdasarkan platform OpenTitan. Penyelesaian yang dicadangkan membolehkan anda menggabungkan kernel sistem pengendalian yang disahkan secara logik dengan komponen perkakasan yang boleh dipercayai (RoT, Root of Trust), dibina menggunakan platform OpenTitan dan seni bina RISC-V. Sebagai tambahan kepada kod KataOS, ia dirancang untuk membuka semua komponen Sparrow lain, termasuk komponen perkakasan, pada masa hadapan.
Platform ini sedang dibangunkan dengan fokus kepada aplikasi dalam cip khusus yang direka untuk menjalankan aplikasi untuk pembelajaran mesin dan memproses maklumat sulit, yang memerlukan tahap perlindungan khas dan pengesahan ketiadaan kegagalan. Contoh aplikasi sedemikian termasuk sistem yang memanipulasi imej orang dan rakaman suara. Penggunaan pengesahan kebolehpercayaan KataOS memastikan bahawa jika satu bahagian sistem gagal, kegagalan tidak akan merebak ke seluruh sistem dan, khususnya, ke kernel dan bahagian kritikal.
Seni bina seL4 terkenal kerana memindahkan bahagian untuk mengurus sumber kernel ke dalam ruang pengguna dan menggunakan alat kawalan akses yang sama untuk sumber tersebut seperti sumber pengguna. Mikrokernel tidak menyediakan abstraksi peringkat tinggi siap sedia untuk mengurus fail, proses, sambungan rangkaian dan seumpamanya; sebaliknya, ia hanya menyediakan mekanisme minimum untuk mengawal akses kepada ruang alamat fizikal, gangguan dan sumber pemproses. Abstraksi peringkat tinggi dan pemacu untuk berinteraksi dengan perkakasan dilaksanakan secara berasingan di atas mikrokernel dalam bentuk tugas peringkat pengguna. Akses tugas sedemikian kepada sumber yang tersedia untuk mikrokernel diatur melalui definisi peraturan.
Untuk perlindungan tambahan, semua komponen kecuali mikrokernel dibangunkan secara asli dalam Rust menggunakan teknik pengaturcaraan selamat yang meminimumkan ralat ingatan yang membawa kepada masalah seperti capaian memori selepas dibebaskan, penyimpangan penuding nol dan overrun penimbal. Pemuat aplikasi dalam persekitaran seL4, perkhidmatan sistem, rangka kerja untuk pembangunan aplikasi, API untuk mengakses panggilan sistem, pengurus proses, mekanisme untuk peruntukan memori dinamik, dll. telah ditulis dalam Rust. Pemasangan yang disahkan menggunakan kit alat CAmkES, yang dibangunkan oleh projek seL4. Komponen untuk CAmkES juga boleh dibuat dalam Rust.
Rust menguatkuasakan keselamatan ingatan pada masa penyusunan melalui semakan rujukan, pemilikan objek dan penjejakan seumur hidup objek (skop), dan dengan menilai ketepatan akses memori pada masa jalan. Rust juga menyediakan perlindungan terhadap limpahan integer, memerlukan nilai pembolehubah untuk dimulakan sebelum digunakan, menggunakan konsep rujukan tidak berubah dan pembolehubah secara lalai, dan menawarkan penaipan statik yang kuat untuk meminimumkan ralat logik.
Sumber: opennet.ru