RISC-V Foundation um að sannreyna virkni örkjarnans á kerfum með RISC-V kennslusettaarkitektúr. Staðfesting kemur niður á áreiðanleika seL4 aðgerða, sem gefur til kynna að fullu samræmi við forskriftirnar sem tilgreindar eru á formlegu tungumáli. Sönnun um áreiðanleika seL4 í mikilvægum kerfum sem byggja á RISC-V RV64 örgjörvum sem krefjast aukins áreiðanleika og tryggja að bilanir séu ekki til staðar. Hönnuðir hugbúnaðar sem keyrir ofan á seL4 kjarnanum geta verið fullvissir um að ef bilun er í einum hluta kerfisins mun þessi bilun ekki breiðast út í restina af kerfinu og sérstaklega mikilvægum hlutum þess.
seL4 örkjarnan var upphaflega staðfestur fyrir 32 bita ARM örgjörva og síðar fyrir 64 bita x86 örgjörva. Það er tekið fram að samsetning opna RISC-V vélbúnaðararkitektúrsins og opna seL4 örkjarnans mun ná nýju öryggisstigi, þar sem einnig er hægt að sannreyna vélbúnaðaríhlutina að fullu í framtíðinni, sem er ómögulegt að ná fyrir sértækan vélbúnaðararkitektúr.
Þegar seL4 er sannprófað er gert ráð fyrir að búnaðurinn virki eins og tilgreint er og forskriftin lýsir að fullu hegðun kerfisins, en í raun er búnaðurinn ekki laus við villur, sem er greinilega sýnt fram á reglulega vandamál sem koma upp í kerfi spákaupmennsku. leiðbeiningar. Opnir vélbúnaðarvettvangar gera það auðveldara að samþætta öryggistengdar breytingar - til dæmis að loka fyrir alla mögulega hliðarrásarleka, þar sem mun skilvirkara er að losna við vandamálið í vélbúnaði en að reyna að finna lausnir í hugbúnaði.
Mundu að seL4 arkitektúrinn færa hluta til að stjórna kjarnaauðlindum inn í notendarými og beita sömu aðgangsstýringaraðferðum fyrir slík auðlind og fyrir notendaauðlindir. Örkjarninn býður ekki upp á tilbúnar útdrætti á háu stigi til að stjórna skrám, ferlum, nettengingum og þess háttar; í staðinn veitir hann aðeins lágmarksaðferðir til að stjórna aðgangi að líkamlegu heimilisfangarými, truflunum og örgjörvaauðlindum. Útdrættir á háu stigi og rekla fyrir samskipti við vélbúnað eru útfærð sérstaklega ofan á örkjarnanum í formi verkefna á notendastigi. Aðgangur slíkra verkefna að þeim auðlindum sem örkjarnan hefur tiltækt er skipulagður með skilgreiningu reglna.
RISC-V býður upp á opið og sveigjanlegt vélaleiðbeiningarkerfi sem gerir kleift að smíða örgjörva fyrir handahófskenndar umsóknir án þess að krefjast þóknana eða strengja tengdum notkun. RISC-V gerir þér kleift að búa til alveg opna SoCs og örgjörva. Sem stendur byggt á RISC-V forskriftinni frá mismunandi fyrirtækjum og samfélögum undir ýmsum ókeypis leyfum (BSD, MIT, Apache 2.0) nokkrir tugir afbrigða af örgjörvakjarna, SoCs og þegar framleiddum flögum. RISC-V stuðningur hefur verið til staðar frá útgáfum af Glibc 2.27, binutils 2.30, gcc 7 og Linux kjarna 4.15.
Heimild: opennet.ru