Yayasan RISC-V tentang memverifikasi pengoperasian mikrokernel pada sistem dengan arsitektur set instruksi RISC-V. Verifikasi turun ke keandalan operasi seL4, yang menunjukkan kepatuhan penuh terhadap spesifikasi yang ditentukan dalam bahasa formal. Bukti keandalan sel4 dalam sistem misi kritis berdasarkan prosesor RISC-V RV64 yang memerlukan peningkatan tingkat keandalan dan jaminan tidak adanya kegagalan. Pengembang perangkat lunak yang berjalan di atas kernel seL4 dapat sepenuhnya yakin bahwa jika terjadi kegagalan pada satu bagian sistem, kegagalan ini tidak akan menyebar ke seluruh sistem dan, khususnya, bagian kritisnya.
Mikrokernel seL4 awalnya diverifikasi untuk prosesor ARM 32-bit, dan kemudian untuk prosesor x64 86-bit. Perlu dicatat bahwa kombinasi arsitektur perangkat keras RISC-V terbuka dengan mikrokernel sel4 terbuka akan mencapai tingkat keamanan baru, karena komponen perangkat keras juga dapat diverifikasi sepenuhnya di masa depan, yang tidak mungkin dicapai untuk arsitektur perangkat keras berpemilik.
Saat memverifikasi seL4, diasumsikan bahwa peralatan berfungsi seperti yang dinyatakan dan spesifikasi sepenuhnya menggambarkan perilaku sistem, namun pada kenyataannya peralatan tersebut tidak lepas dari kesalahan, yang secara jelas ditunjukkan dengan masalah yang sering muncul dalam mekanisme eksekusi spekulatif. instruksi. Platform perangkat keras terbuka mempermudah integrasi perubahan terkait keamanan - misalnya, untuk memblokir semua kemungkinan kebocoran saluran samping, yang mana akan jauh lebih efisien untuk mengatasi masalah pada perangkat keras daripada mencoba mencari solusi melalui perangkat lunak.
Ingatlah bahwa arsitektur seL4 memindahkan bagian untuk mengelola sumber daya kernel ke dalam ruang pengguna dan menerapkan cara 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.
RISC-V menyediakan sistem instruksi mesin yang terbuka dan fleksibel yang memungkinkan mikroprosesor dibuat untuk aplikasi sewenang-wenang tanpa memerlukan royalti atau ikatan untuk menggunakannya. RISC-V memungkinkan Anda membuat SoC dan prosesor yang sepenuhnya terbuka. Saat ini berdasarkan spesifikasi RISC-V oleh berbagai perusahaan dan komunitas di bawah berbagai lisensi gratis (BSD, MIT, Apache 2.0) beberapa lusin varian inti mikroprosesor, SoC, dan chip yang sudah diproduksi. Dukungan RISC-V telah hadir sejak rilis Glibc 2.27, binutils 2.30, gcc 7, dan kernel Linux 4.15.
Sumber: opennet.ru