Yayasan RISC-V mengumumkan bahawa ia telah mengesahkan bagaimana mikrokernel berfungsi seL4 dalam sistem dengan seni bina set arahan RISC-V. Di mana proses verifikasi dikurangkan menjadi bukti matematik kebolehpercayaan seL4, yang menunjukkan kepatuhan penuh dengan spesifikasi yang ditentukan dalam bahasa formal.
Ujian kebolehpercayaan membolehkan seL4 digunakan dalam sistem kritikal misi berdasarkan pemproses RISC-V RV64, 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
Senibina seL4 terkenal kerana membuang bahagian untuk menguruskan sumber kernel di ruang pengguna dan gunakan kaedah kawalan akses yang sama untuk sumber seperti sumber pengguna.
Mikrokernel tidak memberikan abstraksi tahap tinggi sudah bersedia untuk menguruskan fail, proses, sambungan rangkaian, dan lain-lain, tetapi sebaliknya hanya menyediakan mekanisme minimum untuk mengawal akses ke 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 terbuka dan fleksibel arahan mesin yang memungkinkan untuk membuat mikropemproses untuk aplikasi sewenang-wenangnya, tanpa memerlukan pemotongan 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 86-bit x64.
Diperhatikan bahawa gabungan seni bina perkakasan terbuka RISC-V dengan mikrokernel terbuka seL4 akan mencapai tahap keselamatan yang baru, kerana komponen perkakasan pada masa akan datang juga dapat disahkan sepenuhnya, yang mustahil 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 penyatuan perubahan yang berkaitan dengan keselamatan, misalnya, untuk menyekat semua kemungkinan kebocoran saluran melalui saluran pihak ketiga, di mana jauh lebih efisien untuk menyingkirkan masalah dengan perkakasan daripada berusaha mencari penyelesaian dengan perisian.
Akhirnya, jika anda ingin mengetahui lebih lanjut mengenainya, anda boleh melihat nota di pautan berikut.
Bagi saya, pemproses ini adalah sesuatu yang sangat memanggil saya. Hanya tinggal sebilangan anjing anjing gemuk yang membuat komputer yang boleh kita beli.
Isu ARM adalah sesuatu yang menjengkelkan saya, anda sudah melihat apa yang berlaku dengan Huawei dengan sekatan tersebut. Saya jelas bahawa untuk RISC-V saya adalah penyelesaian yang jauh lebih baik di semua peringkat. Pada masa ini Huawei telah mengawasinya dan mungkin di masa depan mereka akan mempunyai peralatan dengan mikro ini. Sekiranya demikian, pasti akan ada lebih banyak syarikat yang menggunakannya dan bagi saya itulah yang paling ideal dan yang paling penting ialah distro menyokongnya dan bukan hanya ARM seperti yang berlaku dengan kebanyakan.
+10