Yayasan RISC-V mengumumkan bahawa ia telah mengesahkan fungsi mikrokernel seL4 pada sistem dengan seni bina set arahan RISC-V . Proses pengesahan dikurangkan kepada bukti matematik kebolehpercayaan seL4, yang menunjukkan pematuhan penuh dengan spesifikasi yang ditakrifkan dalam bahasa formal.
Ujian kebolehpercayaan membolehkan penggunaan seL4 dalam sistem kritikal misi berdasarkan pemproses RV64 RISC-V , yang memerlukan tahap kebolehpercayaan yang lebih tinggi dan tidak menjamin kegagalan.
Pembangun perisian yang berjalan di atas kernel seL4 dapat yakin sepenuhnya bahawa sekiranya berlaku kegagalan pada satu bahagian sistem, kegagalan ini tidak akan merebak ke seluruh sistem dan, khususnya, ke bahagian kritikalnya.
Mengenai seL4
Seni bina seL4 terkenal kerana mengalih keluar bahagian untuk mengurus sumber kernel daripada ruang pengguna dan menggunakan kaedah kawalan akses yang sama untuk sumber tersebut seperti untuk sumber pengguna.
Mikrokernel tidak menyediakan abstraksi peringkat tinggi yang sedia ada untuk mengurus fail, proses, sambungan rangkaian, dan sebagainya, tetapi hanya menyediakan mekanisme minimum untuk mengawal akses kepada ruang alamat fizikal , gangguan dan sumber pemproses.
Pengabstrakan dan pemacu tahap tinggi untuk berinteraksi dengan komputer dilaksanakan secara berasingan di atas mikrokernel dalam bentuk tugas yang dilakukan di peringkat pengguna.
Akses tugas seperti itu ke sumber yang ada di mikrokernel diatur melalui definisi peraturan.
RISC-V menyediakan sistem arahan mesin yang terbuka dan fleksibel yang membolehkan penciptaan mikropemproses untuk aplikasi sewenang-wenangnya, tanpa memerlukan potongan dan tanpa mengenakan syarat penggunaan.
RISC-V membolehkan anda membuat pemproses dan SoC yang terbuka sepenuhnya. Pada masa ini, berdasarkan spesifikasi RISC-V, beberapa syarikat dan komuniti di bawah pelbagai lesen percuma (BSD, MIT, Apache 2.0) sedang mengembangkan beberapa belasan varian teras mikropemproses, SoC dan cip yang sudah dihasilkan.
Sokongan RISC-V sudah ada sejak pelepasan kernel Glibc 2.27, binutils 2.30, gcc 7, dan kernel Linux 4.15.
Mengenai ujian mikrokernel seL4
Pada mulanya, mikrokernel seL4 telah disahkan untuk pemproses ARM 32-bit , dan kemudian untuk pemproses x86 64-bit.
Diperhatikan bahawa gabungan seni bina perkakasan RISC-V terbuka dengan mikrokernel seL4 terbuka akan mencapai tahap keselamatan yang baharu , memandangkan komponen perkakasan pada masa hadapan juga boleh disahkan sepenuhnya, yang mustahil untuk dicapai untuk seni bina perkakasan proprietari.
Semasa kita memeriksa seL4, kita mesti menganggap bahawa perkakasan berfungsi dengan baik (iaitu, seperti yang dinyatakan). Ini mengandaikan ada spesifikasi yang jelas, yang tidak berlaku untuk semua perkakasan.
Tetapi walaupun spesifikasi seperti itu ada, dan bersifat formal (iaitu, dimasukkan ke dalam formalisme matematik yang menyokong penaakulan matematik mengenai sifatnya), bagaimana kita tahu bahawa ia benar-benar menangkap tingkah laku perkakasan?
Kenyataannya adalah bahawa kita boleh yakin bahawa tidak. Perkakasan tidak berbeza dengan perisian kerana kedua-duanya kereta.
Tetapi mempunyai ISA terbuka mempunyai kelebihan yang melebihi bebas royalti. Salah satunya ialah ia membenarkan pelaksanaan perkakasan sumber terbuka.
Semasa memeriksa seL4, diasumsikan bahawa peralatan berfungsi seperti yang ditunjukkan dan spesifikasi menjelaskan sepenuhnya perilaku sistem, tetapi sebenarnya peralatan tersebut tidak bebas dari kesalahan, yang ditunjukkan dengan baik oleh masalah yang selalu timbul dalam Arahan mekanisme pelaksanaan spekulatif.
Platform perkakasan terbuka memudahkan penyepaduan perubahan berkaitan keselamatan, contohnya, untuk menyekat semua saluran kebocoran yang mungkin melalui saluran pihak ketiga, yang mana ia jauh lebih cekap untuk menyingkirkan masalah melalui perkakasan daripada cuba mencari penyelesaian melalui perisian.
Akhir sekali, jika anda ingin mengetahui lebih lanjut mengenainya, anda boleh merujuk artikel di pautan berikut.