Google telah mengumumkan penemuan pengembangan terkait proyek KataOS, yang bertujuan untuk menciptakan sistem operasi yang aman untuk perangkat keras yang tertanam. Komponen sistem KataOS ditulis dalam Rust dan dijalankan di atas mikrokernel seL4, yang mana bukti keandalan matematis telah disediakan pada sistem RISC-V, yang menunjukkan bahwa kode tersebut sepenuhnya mematuhi spesifikasi yang ditentukan dalam bahasa formal. Kode proyek terbuka di bawah lisensi Apache 2.0.
Sistem ini menyediakan dukungan untuk platform berdasarkan arsitektur RISC-V dan ARM64. Untuk mensimulasikan pengoperasian seL4 dan lingkungan KataOS di atas perangkat keras, kerangka kerja Renode digunakan selama proses pengembangan. Sebagai implementasi referensi, kompleks perangkat lunak dan perangkat keras Sparrow diusulkan, menggabungkan KataOS dengan chip aman berdasarkan platform OpenTitan. Solusi yang diusulkan memungkinkan Anda untuk menggabungkan kernel sistem operasi yang diverifikasi secara logis dengan komponen perangkat keras yang dapat dipercaya (RoT, Root of Trust), yang dibangun menggunakan platform OpenTitan dan arsitektur RISC-V. Selain kode KataOS, rencananya akan membuka semua komponen Sparrow lainnya, termasuk komponen hardware, di masa mendatang.
Platform ini sedang dikembangkan dengan tujuan untuk diterapkan pada chip khusus yang dirancang untuk menjalankan aplikasi pembelajaran mesin dan pemrosesan informasi rahasia, yang memerlukan tingkat perlindungan khusus dan konfirmasi tidak adanya kegagalan. Contoh aplikasi tersebut mencakup sistem yang memanipulasi gambar orang dan rekaman suara. Penggunaan verifikasi keandalan KataOS memastikan bahwa jika satu bagian dari sistem gagal, kegagalan tersebut tidak akan menyebar ke seluruh sistem dan, khususnya, ke kernel dan bagian-bagian penting.
Arsitektur seL4 terkenal karena memindahkan bagian-bagian untuk mengelola sumber daya kernel ke dalam ruang pengguna dan menerapkan alat kontrol akses yang sama untuk sumber daya tersebut seperti untuk sumber daya pengguna. Mikrokernel tidak menyediakan abstraksi tingkat tinggi yang siap pakai untuk mengelola file, proses, koneksi jaringan, dan sejenisnya; sebaliknya, mikrokernel hanya menyediakan mekanisme minimal untuk mengontrol akses ke ruang alamat fisik, interupsi, dan sumber daya prosesor. Abstraksi dan driver tingkat tinggi untuk berinteraksi dengan perangkat keras diimplementasikan secara terpisah di atas mikrokernel dalam bentuk tugas tingkat pengguna. Akses tugas-tugas tersebut ke sumber daya yang tersedia untuk mikrokernel diatur melalui definisi aturan.
Untuk perlindungan tambahan, semua komponen kecuali mikrokernel dikembangkan secara asli di Rust menggunakan teknik pemrograman aman yang meminimalkan kesalahan memori yang menyebabkan masalah seperti akses memori setelah pembebasan, dereferensi penunjuk nol, dan buffer overruns. Pemuat aplikasi di lingkungan sel4, layanan sistem, kerangka kerja untuk pengembangan aplikasi, API untuk mengakses panggilan sistem, manajer proses, mekanisme alokasi memori dinamis, dll. ditulis dalam Rust. Perakitan terverifikasi menggunakan toolkit CAmkES, yang dikembangkan oleh proyek seL4. Komponen untuk CAmkES juga dapat dibuat di Rust.
Rust menegakkan keamanan memori pada waktu kompilasi melalui pemeriksaan referensi, kepemilikan objek, dan pelacakan seumur hidup objek (cakupan), dan dengan mengevaluasi kebenaran akses memori saat runtime. Rust juga memberikan perlindungan terhadap integer overflow, memerlukan inisialisasi nilai variabel sebelum digunakan, menggunakan konsep referensi dan variabel yang tidak dapat diubah secara default, dan menawarkan pengetikan statis yang kuat untuk meminimalkan kesalahan logis.
Sumber: opennet.ru