RISC-V verifikasi seL4 microkernel ing prosesor RV64

Yayasan RISC-V ngumumake manawa wis diverifikasi cara kerja mikrokernel seL4 ing sistem karo arsitektur pesawat instruksi RISC-V. Ing endi proses verifikasi dikurangi dadi bukti matematika linuwih seL4, sing nuduhake kepatuhan lengkap karo spesifikasi sing ditemtokake ing basa resmi.

Tes reliabilitas nggawe seL4 digunakake ing sistem kritis misi adhedhasar prosesor RISC-V RV64, sing mbutuhake tingkat reliabilitas sing luwih dhuwur lan ora njamin kegagalan.

Pangembang piranti lunak sing mlaku ing ndhuwur kernel seL4 bisa yakin manawa ana kegagalan ing salah sawijining bagean saka sistem, kegagalan iki ora bakal nyebar menyang sistem liyane, lan utamane ing bagean kritis.

Babagan seL4

Arsitektur seL4 misuwur amarga mbusak bagean kanggo ngatur sumber daya kernel ing ruang pangguna lan nggunakake cara kontrol akses sing padha kanggo sumber daya kayata sumber daya pangguna.

Mikrokernel ora nyedhiyakake abstraksi tingkat dhuwur wis siyap ngatur file, proses, sambungan jaringan, lsp mung nyedhiyakake mekanisme minimal kanggo ngontrol akses menyang ruang alamat fisik, ngganggu, lan sumber daya prosesor.

Abstraksi lan kontrol tingkat dhuwur kanggo sesambungan karo komputer dileksanakake kanthi kapisah ing ndhuwur mikrokernel kanthi wujud tugas sing ditindakake ing level pangguna.

Akses tugas kasebut menyang sumber daya sing kasedhiya ing mikrokernel diatur liwat definisi aturan.

RISC-V nyedhiyakake sistem sing mbukak lan fleksibel instruksi mesin sing ngidini nggawe mikroprosesor kanggo aplikasi sing kasepakatan, tanpa mbutuhake nyuda lan tanpa ngetrapake kahanan panggunaan.

RISC-V ngidini sampeyan nggawe prosesor lan SoC sing mbukak kabeh. Saiki, adhedhasar spesifikasi RISC-V, sawetara perusahaan lan komunitas kanthi lisensi gratis (BSD, MIT, Apache 2.0) ngembangake sawetara lusin varian intine mikroprosesor, SoC, lan chip sing wis diproduksi.

Dhukungan RISC-V wis ana wiwit dirilis Glibc 2.27, binutils 2.30, gcc 7, lan kernel Linux 4.15.

Babagan tes seL4 mikrokernel

Wiwitane, mikrokernel seL4 diverifikasi kanggo pemroses ARM 32-bitlan mengko kanggo prosesor x86 64-bit.

Ditliti manawa kombinasi arsitektur perangkat keras mbukak RISC-V karo mikrokernel terbuka seL4 bakal entuk level keamanan anyar, amarga komponen perangkat keras mbesuk uga bisa diverifikasi kanthi lengkap, sing ora bisa ditindakake kanggo arsitektur hardware kepemilikan.

Nalika mriksa seL4, kita kudu nganggep manawa hardware bisa digunakake kanthi bener (yaiku, kaya sing wis ditemtokake). Sing nganggep ana spesifikasi sing jelas ing wiwitan, sing ora kalebu kabeh perangkat keras. 

Nanging sanajan ana spesifikasi kasebut, lan iku formal (yaiku, ritus ing formalisme matématika sing ndhukung penalaran matématika babagan sifat-sifat kasebut), kepiye kita ngerti manawa sejatine bisa nyekel prilaku hardware? 

Kasunyatane yaiku kita bisa yakin manawa ora kaya ngono. Hardware ora beda karo piranti lunak amarga kaloro barang kasebut.

Nanging duwe ISA sing mbukak duwe kaluwihan sing bebas saka royalti. Salah sijine yaiku ngidini implementasi perangkat keras open source.

Nalika mriksa seL4, bisa dianggep manawa alat kasebut digunakake kaya sing wis dituduhake lan spesifikasi kasebut nggambarake solah bawane sistem, nanging nyatane peralatan kasebut ora bebas kesalahan, sing uga dituduhake kanthi masalah sing sacara rutin muncul ing Instruksi mekanisme eksekusi spekulatif .

Platform hardware mbukak nyederhanakake integrasi pangowahan kayata, gegandhengan karo keamanan, kanggo mblokir kabeh saluran bocor sing bisa liwat saluran pihak katelu, sing luwih efisien kanggo nyingkirake masalah kanthi piranti keras tinimbang nyoba golek solusi kanthi piranti lunak.

Pungkasan, yen sampeyan pengin ngerti luwih lengkap babagan iki, sampeyan bisa mriksa cathetan kasebut ing link ing ngisor iki.