RISC-V қоры микроядроның жұмысын тексеру туралы RISC-V командалар жинағы архитектурасы бар жүйелерде. Тексеру төмендейді seL4 жұмысының сенімділігі, бұл ресми тілде көрсетілген техникалық сипаттамаларға толық сәйкестігін көрсетеді. Сенімділіктің дәлелі RISC-V RV4 процессорларына негізделген, сенімділіктің жоғары деңгейін талап ететін және ақаулардың болмауына кепілдік беретін маңызды жүйелерде seL64. seL4 ядросының жоғарғы жағында жұмыс істейтін бағдарламалық жасақтаманы әзірлеушілер жүйенің бір бөлігінде ақаулық орын алса, бұл ақаулық жүйенің қалған бөлігіне және, атап айтқанда, оның маңызды бөліктеріне таралмайтынына толық сенімді бола алады.
seL4 микроядросы бастапқыда 32-биттік ARM процессорлары үшін, ал кейінірек 64-биттік x86 процессорлары үшін тексерілді. Ашық RISC-V аппараттық архитектурасын ашық seL4 микроядросымен үйлестіру қауіпсіздіктің жаңа деңгейіне қол жеткізетіндігі атап өтіледі, өйткені болашақта аппараттық құрамдас бөліктерді толық тексеруге болады, бұл меншікті аппараттық архитектура үшін қол жеткізу мүмкін емес.
SeL4-ті тексеру кезінде жабдық көрсетілгендей жұмыс істейді және спецификация жүйенің әрекетін толығымен сипаттайды деп болжанады, бірақ шын мәнінде жабдық қателерден бос емес, оны алыпсатарлық орындау механизмінде үнемі пайда болатын проблемалар анық көрсетеді. нұсқаулар. Ашық аппараттық платформалар қауіпсіздікке қатысты өзгерістерді біріктіруді жеңілдетеді - мысалы, барлық ықтимал бүйірлік арнаның ағып кетуіне тосқауыл қою, бұл жерде бағдарламалық құралда уақытша шешімдер табуға тырысқаннан гөрі аппараттық құралдағы ақаулықтан құтылу әлдеқайда тиімді.
seL4 архитектурасын еске түсірейік пайдаланушы кеңістігіне ядро ресурстарын басқаруға арналған бөліктерді жылжыту және пайдаланушы ресурстары сияқты ресурстарға бірдей қол жеткізуді басқару құралдарын қолдану. Микроядро файлдарды, процестерді, желілік қосылымдарды және т.б. басқару үшін дайын жоғары деңгейлі абстракцияларды қамтамасыз етпейді, оның орнына ол физикалық мекенжай кеңістігіне, үзілістерге және процессор ресурстарына қол жеткізуді басқарудың ең аз механизмдерін ғана қамтамасыз етеді. Аппараттық құралдармен әрекеттесу үшін жоғары деңгейлі абстракциялар мен драйверлер пайдаланушы деңгейіндегі тапсырмалар түрінде микроядроның жоғарғы жағында бөлек жүзеге асырылады. Мұндай тапсырмалардың микроядроға қолжетімді ресурстарға қол жеткізуі ережелерді анықтау арқылы ұйымдастырылады.
RISC-V ашық және икемді машина нұсқау жүйесін қамтамасыз етеді, ол микропроцессорларды роялти немесе пайдалану үшін жалғанған жолдарды қажет етпестен ерікті қолданбалар үшін құруға мүмкіндік береді. RISC-V толығымен ашық SoC және процессорларды жасауға мүмкіндік береді. Қазіргі уақытта әртүрлі тегін лицензиялар бойынша (BSD, MIT, Apache 2.0) әртүрлі компаниялар мен қауымдастықтар RISC-V спецификациясына негізделген. микропроцессорлық ядролардың бірнеше ондаған нұсқалары, SoC және қазірдің өзінде шығарылған чиптер. RISC-V қолдауы Glibc 2.27, binutils 2.30, gcc 7 және Linux ядросы 4.15 шығарылымдарынан бері бар.
Ақпарат көзі: opennet.ru