Mikrokernel seL4 diverifikasi sacara matematis pikeun arsitektur RISC-V

Yayasan RISC-V dilaporkeun ngeunaan verifying operasi microkernel nu seL4 dina sistem sareng arsitéktur set instruksi RISC-V. Verifikasi asalna handap pikeun bukti matematis reliabiliti operasi seL4, nu nunjukkeun minuhan pinuh ku spésifikasi dieusian dina basa formal. Buktina reliabilitas ngidinan Anjeun pikeun ngagunakeun seL4 dina sistem misi-kritis dumasar kana prosesor RISC-V RV64 anu merlukeun tingkat ngaronjat reliabiliti sarta ngajamin henteuna gagal. Pamekar parangkat lunak anu dijalankeun dina luhureun kernel seL4 tiasa leres-leres yakin yén upami aya kagagalan dina hiji bagian sistem, kagagalan ieu moal sumebar ka sesa sistem sareng, khususna, bagian kritis na.

Mikrokernel seL4 mimitina diverifikasi pikeun prosesor ARM 32-bit, teras pikeun prosesor 64-bit x86. Perhatikeun yén kombinasi arsitéktur hardware RISC-V kabuka sareng mikrokernel seL4 kabuka bakal ngahontal tingkat kaamanan anyar, sabab komponén hardware ogé tiasa diverifikasi sapinuhna di hareup, anu mustahil pikeun arsitéktur hardware proprietary.

Nalika pariksa seL4, dianggap yén alat-alatna jalan sakumaha anu dinyatakeun sareng spésifikasi pinuh ngajelaskeun paripolah sistem, tapi kanyataanna alat-alatna henteu leupas tina kasalahan, anu jelas-jelas dibuktikeun ku masalah anu sering muncul dina mékanisme palaksanaan spekulatif. parentah. Platform hardware kabuka ngagampangkeun pikeun ngahijikeun parobihan anu aya hubunganana sareng kaamanan - contona, pikeun meungpeuk sadaya kamungkinan bocor saluran sisi, dimana éta langkung éfisién pikeun ngaleungitkeun masalah dina hardware tibatan nyobian milarian solusi dina parangkat lunak.

Ngelingan yén arsitéktur seL4 luar biasa pindah bagian pikeun ngatur sumberdaya kernel kana spasi pamaké sarta nerapkeun sarana kontrol aksés sarua pikeun sumberdaya misalna pikeun sumberdaya pamaké. Mikrokernel henteu nyayogikeun abstraksi tingkat luhur anu siap-siap pikeun ngatur file, prosés, sambungan jaringan, sareng anu sanésna; tibatan, éta ngan ukur nyayogikeun mékanisme minimal pikeun ngadalikeun aksés ka rohangan alamat fisik, interrupts, sareng sumber prosesor. Abstraksi tingkat luhur sareng supir pikeun berinteraksi sareng hardware dilaksanakeun sacara misah di luhur mikrokernel dina bentuk tugas tingkat pangguna. Aksés tugas-tugas sapertos kitu kana sumber daya anu sayogi pikeun mikrokernel diatur ngaliwatan definisi aturan.

RISC-V nyadiakeun sistem instruksi mesin kabuka sarta fléksibel anu ngamungkinkeun microprocessors bisa diwangun pikeun aplikasi sawenang tanpa merlukeun royalti atawa string napel pamakéan. RISC-V ngamungkinkeun anjeun nyiptakeun SoC sareng prosesor anu lengkep. Ayeuna dumasar kana spésifikasi RISC-V ku perusahaan sareng komunitas anu béda dina sababaraha lisénsi gratis (BSD, MIT, Apache 2.0) ngembang sababaraha belasan varian cores microprocessor, SoCs sarta geus dihasilkeun chip. Pangrojong RISC-V parantos aya ti saprak sékrési Glibc 2.27, binutils 2.30, gcc 7, sareng kernel Linux 4.15.

sumber: opennet.ru