Yayasan RISC-V babagan verifikasi operasi microkernel ing sistem kanthi arsitektur set instruksi RISC-V. Verifikasi rawuh mudhun kanggo linuwih saka operasi seL4, kang nuduhake selaras lengkap karo specifications kasebut ing basa formal. Bukti linuwih seL4 ing sistem kritis misi adhedhasar pemroses RISC-V RV64 sing mbutuhake tingkat linuwih lan njamin ora ana kegagalan. Pangembang piranti lunak sing mlaku ing ndhuwur kernel seL4 bisa yakin yen ana kegagalan ing salah sawijining bagean sistem, kegagalan iki ora bakal nyebar menyang sistem liyane lan, utamane, bagean kritis.
Mikrokernel seL4 wiwitane diverifikasi kanggo pemroses ARM 32-bit, lan mengko kanggo pemroses x64 86-bit. Kacathet yen kombinasi arsitektur hardware RISC-V sing mbukak karo mikrokernel seL4 mbukak bakal entuk tingkat keamanan anyar, amarga komponen hardware uga bisa diverifikasi kanthi lengkap ing mangsa ngarep, sing ora bisa digayuh kanggo arsitektur hardware eksklusif.
Nalika verifikasi seL4, dianggep peralatan kasebut bisa digunakake kaya sing wis kasebut lan spesifikasi kasebut kanthi lengkap nggambarake prilaku sistem kasebut, nanging sejatine peralatan kasebut ora luput saka kesalahan, sing dituduhake kanthi jelas kanthi masalah sing terus-terusan muncul ing mekanisme eksekusi spekulatif. instruksi. Platform hardware mbukak luwih gampang kanggo nggabungake owah-owahan sing gegandhengan karo keamanan - contone, kanggo mblokir kabeh bocor saluran sisih, sing luwih efisien kanggo nyisihake masalah ing hardware tinimbang nyoba golek solusi ing piranti lunak.
Elinga yen arsitektur seL4 bagean obah kanggo ngatur sumber daya kernel menyang ruang panganggo lan nglamar sarana kontrol akses padha kanggo sumber daya kanggo sumber daya pangguna. Mikrokernel ora nyedhiyakake abstraksi tingkat dhuwur sing wis siap kanggo ngatur file, proses, sambungan jaringan, lan liya-liyane; nanging mung nyedhiyakake mekanisme minimal kanggo ngontrol akses menyang ruang alamat fisik, interupsi, lan sumber daya prosesor. Abstraksi lan driver tingkat dhuwur kanggo sesambungan karo hardware diimplementasikake kanthi kapisah ing ndhuwur microkernel ing wangun tugas tingkat pangguna. Akses tugas kasebut menyang sumber daya sing kasedhiya kanggo microkernel diatur liwat definisi aturan.
RISC-V nyedhiyakake sistem instruksi mesin sing mbukak lan fleksibel sing ngidini mikroprosesor bisa dibangun kanggo aplikasi sewenang-wenang tanpa mbutuhake royalti utawa senar sing digunakake. RISC-V ngidini sampeyan nggawe SoC lan prosesor sing mbukak. Saiki adhedhasar spesifikasi RISC-V dening macem-macem perusahaan lan komunitas ing macem-macem lisensi gratis (BSD, MIT, Apache 2.0) sawetara rolas varian saka inti mikroprosesor, SoC lan wis diprodhuksi Kripik. Dhukungan RISC-V wis ana wiwit rilis Glibc 2.27, binutils 2.30, gcc 7, lan kernel Linux 4.15.
Source: opennet.ru