Fondaĵo RISC-V pri kontrolado de la funkciado de la mikrokerno sur sistemoj kun arkitekturo de instrukcioj RISC-V. Konfirmo venas al fidindeco de seL4 operacio, kiu indikas plenan konformecon kun la specifoj specifitaj en la formala lingvo. Pruvo de fidindeco seL4 en misi-kritikaj sistemoj bazitaj sur RISC-V RV64-procesoroj kiuj postulas pliigitan nivelon de fidindeco kaj garantias la foreston de fiaskoj. Programistoj de programaro kuranta sur la seL4-kerno povas esti tute certaj, ke se estas malsukceso en unu parto de la sistemo, ĉi tiu malsukceso ne disvastiĝos al la resto de la sistemo kaj, precipe, al ĝiaj kritikaj partoj.
La seL4-mikrokerno estis komence kontrolita por 32-bitaj ARM-procesoroj, kaj poste por 64-bitaj x86-procesoroj. Oni rimarkas, ke la kombinaĵo de la malfermita aparatara arkitekturo RISC-V kun la malferma seL4-mikrokerno atingos novan nivelon de sekureco, ĉar la aparataj komponantoj ankaŭ povas esti plene kontrolitaj en la estonteco, kio estas neeble atingi por proprietaj aparataj arkitekturoj.
Kiam oni kontrolas seL4, oni supozas, ke la ekipaĵo funkcias kiel dirite kaj la specifo plene priskribas la konduton de la sistemo, sed fakte la ekipaĵo ne estas libera de eraroj, kio estas klare pruvita per regule aperantaj problemoj en la mekanismo de spekula ekzekuto de instrukcioj. Malfermaj aparataj platformoj faciligas integri sekurec-rilatajn ŝanĝojn - ekzemple bloki ĉiujn eblajn flankajn kanalajn likojn, kie estas multe pli efike forigi la problemon en aparataro ol provi trovi solvojn en programaro.
Memoru ke la arkitekturo seL4 movi partojn por administri kernresursojn en uzantspacon kaj apliki la samajn alirkontrolrimedojn por tiaj rimedoj kiel por uzantresursoj. La mikrokerno ne disponigas pretajn altnivelajn abstraktaĵojn por administrado de dosieroj, procezoj, retkonektoj, kaj similaĵo; anstataŭe, ĝi disponigas nur minimumajn mekanismojn por kontrolado de aliro al fizika adresspaco, interrompoj, kaj procesorresursoj. Altnivelaj abstraktaĵoj kaj ŝoforoj por interagado kun aparataro estas efektivigitaj aparte aldone al la mikrokerno en la formo de uzant-nivelaj taskoj. Aliro de tiaj taskoj al la rimedoj disponeblaj al la mikrokerno estas organizita per la difino de reguloj.
RISC-V disponigas malferman kaj flekseblan maŝininstrukcisistemon kiu permesas al mikroprocesoroj esti konstruitaj por arbitraj aplikoj sen postulado de tantiemo aŭ ŝnuroj alkroĉitaj por uzi. RISC-V permesas krei tute malfermitajn SoC-ojn kaj procesorojn. Nuntempe surbaze de la RISC-V-specifo fare de malsamaj firmaoj kaj komunumoj sub diversaj liberaj licencoj (BSD, MIT, Apache 2.0) kelkdek variaĵoj de mikroprocesoraj kernoj, SoC-oj kaj jam produktitaj blatoj. RISC-V-subteno ĉeestas ekde la eldonoj de Glibc 2.27, binutils 2.30, gcc 7, kaj la Linukso-kerno 4.15.
fonto: opennet.ru