Yayasan RISC-V tentang mengesahkan operasi mikrokernel pada sistem dengan seni bina set arahan RISC-V. Pengesahan datang ke kebolehpercayaan operasi seL4, yang menunjukkan pematuhan penuh dengan spesifikasi yang dinyatakan dalam bahasa formal. Bukti kebolehpercayaan seL4 dalam sistem kritikal misi berdasarkan pemproses RISC-V RV64 yang memerlukan tahap kebolehpercayaan yang lebih tinggi dan menjamin ketiadaan kegagalan. Pembangun perisian yang berjalan di atas kernel seL4 boleh yakin sepenuhnya bahawa jika terdapat kegagalan dalam satu bahagian sistem, kegagalan ini tidak akan merebak ke seluruh sistem dan, khususnya, bahagian kritikalnya.
Kernel mikro seL4 pada mulanya disahkan untuk pemproses ARM 32-bit, dan kemudian untuk pemproses x64 86-bit. Adalah diperhatikan bahawa gabungan seni bina perkakasan RISC-V terbuka dengan mikrokernel seL4 terbuka akan mencapai tahap keselamatan baharu, memandangkan komponen perkakasan juga boleh disahkan sepenuhnya pada masa hadapan, yang mustahil dicapai untuk seni bina perkakasan proprietari.
Apabila mengesahkan seL4, diandaikan bahawa peralatan berfungsi seperti yang dinyatakan dan spesifikasi menerangkan sepenuhnya kelakuan sistem, tetapi pada hakikatnya peralatan itu tidak bebas daripada ralat, yang jelas ditunjukkan oleh masalah yang kerap muncul dalam mekanisme pelaksanaan spekulatif arahan. Platform perkakasan terbuka menjadikannya lebih mudah untuk menyepadukan perubahan berkaitan keselamatan - contohnya, untuk menyekat semua kemungkinan kebocoran saluran sisi, di mana ia adalah lebih cekap untuk menyingkirkan masalah dalam perkakasan daripada cuba mencari penyelesaian dalam perisian.
Ingat bahawa seni bina seL4 memindahkan bahagian untuk mengurus sumber kernel ke dalam ruang pengguna dan menggunakan cara kawalan capaian 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.
RISC-V menyediakan sistem arahan mesin terbuka dan fleksibel yang membolehkan mikropemproses dibina untuk aplikasi sewenang-wenangnya tanpa memerlukan royalti atau rentetan yang dilampirkan untuk digunakan. RISC-V membolehkan anda mencipta SoC dan pemproses terbuka sepenuhnya. Pada masa ini berdasarkan spesifikasi RISC-V oleh syarikat dan komuniti yang berbeza di bawah pelbagai lesen percuma (BSD, MIT, Apache 2.0) beberapa dozen varian teras mikropemproses, SoC dan cip yang telah dihasilkan. Sokongan RISC-V telah wujud sejak keluaran Glibc 2.27, binutils 2.30, gcc 7 dan kernel Linux 4.15.
Sumber: opennet.ru