Inanunsyo ng RISC-V Foundation na na-verify na nito kung paano gumagana ang microkernel seL4 sa mga system na may itinuro ang arkitektura RISC-V. Kung saan ang proseso ng pag-verify ay nabawasan sa patunay ng matematika ng pagiging maaasahan ng seL4, na nagpapahiwatig ng buong pagsunod sa mga pagtutukoy na tinukoy sa isang pormal na wika.
Ang pagsubok sa pagiging maaasahan ay nagbibigay-daan sa seL4 na magamit sa mga kritikal na sistema ng misyon batay sa mga prosesor ng RISC-V RV64, na nangangailangan ng isang mas mataas na antas ng pagiging maaasahan at hindi ginagarantiyahan ang pagkabigo.
Ang mga developer ng software na tumatakbo sa tuktok ng seL4 kernel ay maaaring maging ganap na sigurado na sa kaganapan ng pagkabigo sa isang bahagi ng system, ang kabiguang ito ay hindi kumalat sa natitirang bahagi ng system at, lalo na, sa mga kritikal na bahagi nito.
Tungkol sa seL4
Ang seL4 na arkitektura ay kapansin-pansin para sa pag-alis ng mga bahagi upang pamahalaan ang mga mapagkukunan ng kernel sa puwang ng gumagamit at gumamit ng parehong mga paraan ng pagkontrol sa pag-access para sa mga naturang mapagkukunan tulad ng para sa mga mapagkukunan ng gumagamit.
Ang microkernel ay hindi nagbibigay ng mataas na antas na mga abstraction handa na upang pamahalaan ang mga file, proseso, koneksyon sa network, atbp, ngunit sa halip nagbibigay lamang ng kaunting mga mekanismo upang makontrol ang pag-access sa puwang ng pisikal na address, nakakagambala, at mga mapagkukunan ng processor.
Ang mga mataas na antas na abstraction at driver para sa pakikipag-ugnay sa computer ay ipinatupad nang magkahiwalay sa tuktok ng microkernel sa anyo ng mga gawain na isinagawa sa antas ng gumagamit.
Ang pag-access ng mga naturang gawain sa mga mapagkukunang magagamit sa microkernel ay isinaayos sa pamamagitan ng kahulugan ng mga patakaran.
Nagbibigay ang RISC-V ng isang bukas at kakayahang umangkop na system ng mga tagubilin sa makina na pinapayagan na lumikha ng mga microprocessor para sa di-makatwirang mga aplikasyon, nang hindi nangangailangan ng mga pagbawas at nang walang pagpapataw ng mga kundisyon ng paggamit.
Pinapayagan ka ng RISC-V na lumikha ng ganap na bukas na mga SoC at processor. Sa kasalukuyan, batay sa pagtutukoy ng RISC-V, maraming mga kumpanya at pamayanan sa ilalim ng iba't ibang mga libreng lisensya (BSD, MIT, Apache 2.0) ay nagkakaroon ng ilang dosenang mga pagkakaiba-iba ng mga nagawa na microprocessor core, SoCs at chips.
Ang suporta ng RISC-V ay nasa paligid mula nang mailabas ang Glibc 2.27, binutils 2.30, gcc 7, at ang Linux 4.15 kernel.
Tungkol sa seL4 microkernel na pagsubok
Sa una, ang microkernel ang seL4 ay na-verify para sa 32-bit na mga processor ng ARM, At mamaya para sa x86 64-bit na mga processor.
Napansin na ang kombinasyon ng RISC-V bukas na arkitektura ng hardware na may bukas na microkernel makakamit ng seL4 ang isang bagong antas ng seguridad, tulad ng mga bahagi ng hardware sa hinaharap ay maaari ding ganap na ma-verify, na imposibleng makamit para sa pagmamay-ari ng mga arkitektura ng hardware.
Kapag sinuri namin ang seL4, dapat nating ipalagay na ang hardware ay gumagana nang maayos (iyon ay, tulad ng tinukoy). Ipinapalagay na mayroong isang hindi malinaw na pagtutukoy sa una, na hindi ang kaso para sa lahat ng hardware.
Ngunit kahit na mayroon ang gayong pagtutukoy, at ito ay pormal (iyon ay, na-rite sa isang pormalismo ng matematika na sumusuporta sa pangangatwirang matematika tungkol sa mga katangian nito), paano natin malalaman na talagang kinukuha nito ang pag-uugali ng hardware?
Ang katotohanan ay makasisiguro tayo na hindi ito. Ang hardware ay hindi naiiba mula sa software na pareho ang buggy.
Ngunit ang pagkakaroon ng bukas na ISA ay may mga kalamangan na lampas sa pagiging royal-free. Ang isa ay pinapayagan nito ang mga pagpapatupad ng bukas na mapagkukunan ng hardware.
Kapag sinuri ang seL4, ipinapalagay na ang kagamitan ay gumagana tulad ng ipinahiwatig at ang detalye ay ganap na naglalarawan sa pag-uugali ng system, ngunit sa katunayan ang kagamitan ay hindi libre sa pagkakamali, na kung saan ay mahusay na ipinakita ng mga problema na regular na lumitaw sa ispekulatibong pagpapatupad ng Mga Tagubilin.
Buksan ang mga platform ng hardware na pinasimple ang pagsasama ng mga pagbabago na may kaugnayan sa seguridad, halimbawa, upang harangan ang lahat ng mga posibleng leak channel sa pamamagitan ng mga third-party na channel, kung saan mas mahusay ang pagtanggal ng isang problema sa pamamagitan ng hardware kaysa subukan na makahanap ng mga solusyon sa pamamagitan ng software.
Panghuli, kung nais mong malaman ang tungkol dito, maaari kang kumunsulta sa tala sa sumusunod na link.
Para sa akin, ang processor na ito ay isang bagay na tumatawag sa akin ng marami. Nananatili lamang ito para sa ilang taba ng aso ng computer upang makagawa ng isang computer na maaari nating bilhin.
Ang isyu sa ARM ay isang bagay na humihimok sa akin, nakita mo na kung ano ang nangyari sa Huawei sa mga parusa. Malinaw ko na para sa aking RISC-V ito ay isang mas mahusay na solusyon sa lahat ng mga antas. Sa ngayon ay nakatingin na ang Huawei dito at marahil sa hinaharap magkakaroon sila ng kagamitan sa micro na ito. Kung gayon, tiyak na magkakaroon ng maraming mga kumpanya na gumagamit nito at para sa akin na iyon ang magiging perpekto at higit sa lahat suportado ito ng mga distrito at hindi lamang ang ARM na nangyayari sa karamihan.
+ 10