Yayasan RISC-V mengumumkan bahwa mereka telah memverifikasi bagaimana mikrokernel bekerja seL4 dalam sistem dengan arsitektur set instruksi RISC-V. Di mana proses verifikasi direduksi menjadi bukti matematis dari keandalan seL4, yang menunjukkan kepatuhan penuh dengan spesifikasi yang ditentukan dalam bahasa formal.
Pengujian keandalan memungkinkan seL4 digunakan dalam sistem kritis misi berdasarkan prosesor RISC-V RV64, yang membutuhkan tingkat keandalan yang lebih tinggi dan tidak menjamin kegagalan.
Pengembang perangkat lunak yang berjalan di atas kernel seL4 dapat sepenuhnya yakin bahwa jika terjadi kegagalan di satu bagian sistem, kegagalan ini tidak akan menyebar ke seluruh sistem dan, khususnya, ke bagian kritisnya.
Tentang seL4
Arsitektur seL4 terkenal karena menghapus bagian untuk mengelola sumber daya kernel di ruang pengguna dan menggunakan metode kontrol akses yang sama untuk sumber daya seperti untuk sumber daya pengguna.
Mikrokernel tidak memberikan abstraksi tingkat tinggi sudah siap untuk mengelola file, proses, koneksi jaringan, dll., tetapi sebaliknya hanya menyediakan mekanisme minimal untuk mengontrol akses ke ruang alamat fisik, interupsi, dan sumber daya prosesor.
Abstraksi tingkat tinggi dan driver untuk berinteraksi dengan komputer diimplementasikan secara terpisah di atas mikrokernel dalam bentuk tugas yang dilakukan di tingkat pengguna.
Akses tugas tersebut ke sumber daya yang tersedia di mikrokernel diatur melalui definisi aturan.
RISC-V menyediakan sistem yang terbuka dan fleksibel instruksi mesin itu memungkinkan untuk membuat mikroprosesor untuk aplikasi sewenang-wenang, tanpa memerlukan pemotongan dan tanpa memaksakan ketentuan penggunaan.
RISC-V memungkinkan Anda membuat prosesor dan SoC yang sepenuhnya terbuka. Saat ini, berdasarkan spesifikasi RISC-V, beberapa perusahaan dan komunitas di bawah berbagai lisensi gratis (BSD, MIT, Apache 2.0) sedang mengembangkan beberapa lusin varian inti mikroprosesor yang sudah diproduksi, SoC, dan chip.
Dukungan RISC-V telah ada sejak rilis Glibc 2.27, binutils 2.30, gcc 7, dan kernel Linux 4.15.
Tentang pengujian mikrokernel seL4
Awalnya, mikrokernel seL4 telah diverifikasi untuk prosesor ARM 32-bit, Dan kemudian untuk prosesor x86 64-bit.
Teramati bahwa kombinasi arsitektur perangkat keras terbuka RISC-V dengan mikrokernel terbuka seL4 akan mencapai tingkat keamanan baru, karena komponen perangkat keras di masa mendatang juga dapat diverifikasi sepenuhnya, yang tidak mungkin dicapai untuk arsitektur perangkat keras berpemilik.
Ketika kami memeriksa seL4, kami harus berasumsi bahwa perangkat keras bekerja dengan baik (yaitu, seperti yang ditentukan). Itu mengasumsikan ada spesifikasi yang tidak ambigu di tempat pertama, yang tidak berlaku untuk semua perangkat keras.
Tetapi bahkan ketika spesifikasi seperti itu ada, dan itu formal (yaitu, dituangkan ke dalam formalisme matematika yang mendukung penalaran matematis tentang propertinya), bagaimana kita tahu bahwa itu benar-benar menangkap perilaku perangkat keras?
Kenyataannya adalah bahwa kita cukup yakin bahwa itu tidak benar. Perangkat keras tidak berbeda dengan perangkat lunak karena keduanya memiliki bug.
Tetapi memiliki ISA terbuka memiliki keuntungan yang melampaui bebas royalti. Salah satunya adalah memungkinkan implementasi perangkat keras sumber terbuka.
Saat memeriksa seL4, diasumsikan bahwa peralatan bekerja seperti yang ditunjukkan dan spesifikasinya menggambarkan perilaku sistem secara lengkap, tetapi pada kenyataannya peralatan tersebut tidak bebas dari kesalahan, yang ditunjukkan dengan baik oleh masalah yang secara teratur muncul dalam mekanisme eksekusi spekulatif. .
Platform perangkat keras terbuka menyederhanakan integrasi perubahan terkait dengan keamanan, misalnya, untuk memblokir semua kemungkinan saluran kebocoran melalui saluran pihak ketiga, yang jauh lebih efisien untuk menyingkirkan masalah dengan perangkat keras daripada mencoba mencari solusi dengan perangkat lunak.
Terakhir, jika Anda ingin mengetahui lebih banyak tentangnya, Anda dapat melihat catatan di link berikut.
Bagi saya, prosesor ini adalah sesuatu yang sering memanggil saya. Tinggal beberapa anjing komputer gemuk untuk membuat komputer yang bisa kita beli.
Masalah ARM adalah sesuatu yang mencicit saya, Anda sudah melihat apa yang terjadi dengan Huawei dengan sanksi. Saya yakin bahwa untuk RISC-V saya, ini adalah solusi yang jauh lebih baik di semua tingkatan. Saat ini Huawei telah mengincarnya dan mungkin di masa depan mereka akan memiliki peralatan dengan mikro ini. Jika demikian, pasti akan ada lebih banyak perusahaan yang mengadopsinya dan bagi saya itu akan menjadi yang ideal dan di atas semua itu distro mendukungnya dan tidak hanya ARM seperti yang terjadi pada kebanyakan orang.
+10