RISC-V Foundation tungkol sa pag-verify sa pagpapatakbo ng microkernel sa mga system na may RISC-V instruction set architecture. Ang pag-verify ay bumaba sa pagiging maaasahan ng operasyon ng seL4, na nagpapahiwatig ng ganap na pagsunod sa mga pagtutukoy na tinukoy sa pormal na wika. Katibayan ng pagiging maaasahan seL4 sa mga sistemang kritikal sa misyon batay sa mga processor ng RISC-V RV64 na nangangailangan ng mas mataas na antas ng pagiging maaasahan at ginagarantiyahan ang kawalan ng mga pagkabigo. Ang mga developer ng software na tumatakbo sa ibabaw ng seL4 kernel ay maaaring maging ganap na kumpiyansa na kung may pagkabigo sa isang bahagi ng system, ang pagkabigo na ito ay hindi kakalat sa iba pang bahagi ng system at, sa partikular, sa mga kritikal na bahagi nito.
Ang seL4 microkernel ay unang na-verify para sa mga 32-bit na ARM processor, at nang maglaon para sa 64-bit x86 na mga processor. Napansin na ang kumbinasyon ng bukas na arkitektura ng hardware ng RISC-V na may bukas na seL4 microkernel ay makakamit ng isang bagong antas ng seguridad, dahil ang mga bahagi ng hardware ay maaari ding ganap na ma-verify sa hinaharap, na imposibleng makamit para sa pagmamay-ari ng mga arkitektura ng hardware.
Kapag bini-verify ang seL4, ipinapalagay na ang kagamitan ay gumagana tulad ng nakasaad at ang detalye ay ganap na naglalarawan sa pag-uugali ng system, ngunit sa katotohanan ang kagamitan ay hindi malaya mula sa mga error, na malinaw na ipinapakita ng mga regular na umuusbong na mga problema sa mekanismo ng speculative execution ng mga tagubilin. Pinapadali ng mga bukas na platform ng hardware ang pagsasama-sama ng mga pagbabagong nauugnay sa seguridad - halimbawa, upang harangan ang lahat ng posibleng pagtagas sa side-channel, kung saan mas mahusay na alisin ang problema sa hardware kaysa subukang maghanap ng mga solusyon sa software.
Alalahanin na ang arkitektura ng seL4 paglipat ng mga bahagi para sa pamamahala ng mga mapagkukunan ng kernel sa espasyo ng gumagamit at paglalapat ng parehong paraan ng kontrol sa pag-access para sa mga mapagkukunan tulad ng para sa mga mapagkukunan ng gumagamit. Ang microkernel ay hindi nagbibigay ng mga nakahanda nang high-level abstraction para sa pamamahala ng mga file, proseso, koneksyon sa network, at mga katulad nito; sa halip, nagbibigay lamang ito ng mga minimal na mekanismo para sa pagkontrol ng access sa pisikal na address space, mga interrupts, at mga mapagkukunan ng processor. Ang mga high-level abstraction at driver para sa pakikipag-ugnayan sa hardware ay ipinapatupad nang hiwalay sa ibabaw ng microkernel sa anyo ng mga gawain sa antas ng user. Ang pag-access ng naturang mga gawain sa mga mapagkukunang magagamit sa microkernel ay isinaayos sa pamamagitan ng kahulugan ng mga panuntunan.
Ang RISC-V ay nagbibigay ng isang bukas at nababaluktot na sistema ng pagtuturo ng makina na nagpapahintulot sa mga microprocessor na mabuo para sa mga arbitrary na aplikasyon nang hindi nangangailangan ng mga royalty o mga string na nakakabit upang magamit. Binibigyang-daan ka ng RISC-V na lumikha ng ganap na bukas na mga SoC at processor. Kasalukuyang nakabatay sa detalye ng RISC-V ng iba't ibang kumpanya at komunidad sa ilalim ng iba't ibang libreng lisensya (BSD, MIT, Apache 2.0) ilang dosenang variant ng microprocessor cores, SoCs at nakagawa na ng mga chips. Ang suporta sa RISC-V ay naroroon na mula noong inilabas ang Glibc 2.27, binutils 2.30, gcc 7, at ang Linux kernel 4.15.
Pinagmulan: opennet.ru