Fondazzjoni RISC-V dwar il-verifika tat-tħaddim tal-mikrokernel fuq sistemi b'arkitettura ta' sett ta' struzzjonijiet RISC-V. Il-verifika tasal għal affidabbiltà tal-operazzjoni seL4, li tindika konformità sħiħa mal-ispeċifikazzjonijiet speċifikati fil-lingwa formali. Prova ta' affidabbiltà seL4 f'sistemi kritiċi għall-missjoni bbażati fuq proċessuri RISC-V RV64 li jeħtieġu livell akbar ta 'affidabilità u jiggarantixxu n-nuqqas ta' fallimenti. L-iżviluppaturi ta 'softwer li jaħdem fuq il-qalba seL4 jistgħu jkunu kompletament kunfidenti li jekk ikun hemm falliment f'parti waħda tas-sistema, dan in-nuqqas ma jinfirex mal-bqija tas-sistema u, b'mod partikolari, il-partijiet kritiċi tagħha.
Il-mikrokernel seL4 ġie vverifikat inizjalment għal proċessuri ARM ta '32 bit, u aktar tard għal proċessuri x64 ta' 86 bit. Huwa nnutat li l-kombinazzjoni tal-arkitettura tal-ħardwer RISC-V miftuħa mal-mikrokernel seL4 miftuħ se tikseb livell ġdid ta 'sigurtà, peress li l-komponenti tal-ħardwer jistgħu wkoll jiġu vverifikati bis-sħiħ fil-futur, li huwa impossibbli li jinkiseb għall-arkitetturi tal-hardware proprjetarji.
Meta tivverifika seL4, huwa preżunt li t-tagħmir jaħdem kif iddikjarat u l-ispeċifikazzjoni tiddeskrivi bis-sħiħ l-imġieba tas-sistema, iżda fir-realtà t-tagħmir mhuwiex ħieles minn żbalji, li huwa muri b'mod ċar minn problemi emerġenti regolarment fil-mekkaniżmu ta 'eżekuzzjoni spekulattiva ta' istruzzjonijiet. Pjattaformi tal-ħardwer miftuħa jagħmluha aktar faċli biex jiġu integrati bidliet relatati mas-sigurtà - pereżempju, li jimblokka t-tnixxija kollha possibbli tal-kanali tal-ġenb, fejn huwa ħafna aktar effiċjenti li teħles mill-problema fil-ħardwer milli li tipprova ssib soluzzjonijiet ta' soluzzjoni fis-softwer.
Ifakkar li l-arkitettura seL4 partijiet li jiċċaqilqu għall-ġestjoni tar-riżorsi tal-qalba fl-ispazju tal-utent u l-applikazzjoni tal-istess mezzi ta' kontroll tal-aċċess għal tali riżorsi bħal dawk għar-riżorsi tal-utent. Il-mikrokernel ma jipprovdix astrazzjonijiet ta’ livell għoli lesti għall-ġestjoni ta’ fajls, proċessi, konnessjonijiet tan-netwerk, u affarijiet simili; minflok, jipprovdi biss mekkaniżmi minimi għall-kontroll tal-aċċess għall-ispazju tal-indirizz fiżiku, interruzzjonijiet u riżorsi tal-proċessur. Astrazzjonijiet ta 'livell għoli u sewwieqa għall-interazzjoni mal-ħardwer huma implimentati separatament fuq il-mikrokernel fil-forma ta' kompiti fil-livell tal-utent. L-aċċess ta' tali kompiti għar-riżorsi disponibbli għall-mikrokernel huwa organizzat permezz tad-definizzjoni tar-regoli.
RISC-V jipprovdi sistema ta 'struzzjoni tal-magni miftuħa u flessibbli li tippermetti li jinbnew mikroproċessuri għal applikazzjonijiet arbitrarji mingħajr ma jeħtieġu royalties jew kordi mwaħħla għall-użu. RISC-V jippermettilek toħloq SoCs u proċessuri kompletament miftuħa. Bħalissa bbażata fuq l-ispeċifikazzjoni RISC-V minn kumpaniji u komunitajiet differenti taħt diversi liċenzji ħielsa (BSD, MIT, Apache 2.0) diversi għexieren ta 'varjanti ta' qlub ta 'mikroproċessuri, SoCs u ċipep diġà prodotti. L-appoġġ RISC-V ilu preżenti mill-ħruġ ta 'Glibc 2.27, binutils 2.30, gcc 7, u l-kernel Linux 4.15.
Sors: opennet.ru