Stichting RISC-V oer it ferifiearjen fan de wurking fan 'e mikrokernel op systemen mei RISC-V ynstruksje set arsjitektuer. Ferifikaasje komt del op betrouberens fan seL4 operaasje, dat jout folsleine neilibjen fan de spesifikaasjes oantsjutte yn de formele taal. Bewiis fan betrouberens seL4 yn missy-krityske systemen basearre op RISC-V RV64-processors dy't in ferhege nivo fan betrouberens fereaskje en it ûntbrekken fan mislearrings garandearje. Untwikkelders fan software dy't boppe op 'e seL4-kernel rinne, kinne folslein wis wêze dat as d'r in flater is yn ien diel fan it systeem, dizze mislearring net ferspraat sil nei de rest fan it systeem en, yn it bysûnder, syn krityske dielen.
De seL4-mikrokernel waard yn earste ynstânsje ferifiearre foar 32-bit ARM-processors, en letter foar 64-bit x86-prosessor. It wurdt opmurken dat de kombinaasje fan 'e iepen RISC-V-hardware-arsjitektuer mei de iepen seL4-mikrokernel in nij nivo fan feiligens sil berikke, om't de hardware-komponinten ek yn' e takomst folslein kinne wurde ferifiearre, wat ûnmooglik is te berikken foar proprietêre hardware-arsjitektuer.
By it ferifiearjen fan seL4 wurdt oannommen dat de apparatuer wurket lykas sein en de spesifikaasje beskriuwt it gedrach fan it systeem folslein, mar yn 'e realiteit is de apparatuer net frij fan flaters, wat dúdlik wurdt oantoand troch regelmjittich opkommende problemen yn it meganisme fan spekulative útfiering fan ynstruksjes. Iepen hardware-platfoarms meitsje it makliker om feiligens-relatearre feroarings te yntegrearjen - bygelyks om alle mooglike side-kanaal-lekken te blokkearjen, wêr't it folle effisjinter is om it probleem yn hardware kwyt te reitsjen dan om te besykjen om oplossingen te finen yn software.
Tink derom dat de seL4-arsjitektuer ferpleatse dielen foar it behearen fan kernelboarnen yn brûkersromte en it tapassen fan deselde tagongskontrôlemiddels foar sokke boarnen as foar brûkersboarnen. De mikrokernel leveret gjin klearmakke abstraksjes op heech nivo foar it behearen fan bestannen, prosessen, netwurkferbiningen, en sa; Ynstee dêrfan leveret it allinich minimale meganismen foar it kontrolearjen fan tagong ta fysike adresromte, interrupts en prosessorboarnen. Abstraksjes op hege nivo en bestjoerders foar ynteraksje mei hardware wurde apart boppe op 'e mikrokernel ymplementearre yn' e foarm fan taken op brûkersnivo. Tagong fan sokke taken ta de boarnen beskikber foar de mikrokernel wurdt organisearre troch de definysje fan regels.
RISC-V biedt in iepen en fleksibele masine-ynstruksjesysteem wêrmei mikroprocessors kinne wurde boud foar willekeurige tapassingen sûnder royalty's of snaren taheakke te brûken. RISC-V lit jo folslein iepen SoC's en processors meitsje. Op it stuit basearre op de RISC-V-spesifikaasje troch ferskate bedriuwen en mienskippen ûnder ferskate fergese lisinsjes (BSD, MIT, Apache 2.0) ferskate tsientallen farianten fan microprocessor kearnen, SoCs en al produsearre chips. RISC-V-stipe is oanwêzich sûnt de releases fan Glibc 2.27, binutils 2.30, gcc 7, en de Linux kernel 4.15.
Boarne: opennet.ru