Арганізацыя RISC-V Foundation аб верыфікацыі працы мікраядра на сістэмах з архітэктурай набора каманд RISC-V. Верыфікацыя зводзіцца да надзейнасці працы seL4, якое сведчыць аб поўнай адпаведнасці зададзеным на фармальнай мове спецыфікацыям. Доказ надзейнасці seL4 у крытычна важных сістэмах на базе працэсараў RISC-V RV64, якія патрабуюць падвышанага ўзроўня надзейнасці і што гарантуюць адсутнасць збояў. Распрацоўнікі ПЗ, які працуе па-над ядром seL4, могуць быць цалкам упэўненыя, што ў выпадку збою ў адной частцы сістэмы, дадзены збой не распаўсюдзіцца на астатнюю сістэму і, у прыватнасці, яе крытычныя часткі.
Першапачаткова микроядро seL4 было верыфікавана для 32-разрадных працэсараў ARM, а пазней для 64-разрадных працэсараў x86. Адзначаецца, што камбінацыя адкрытай апаратнай архітэктуры RISC-V з адкрытым мікраядром seL4 дазволіць дамагчыся новага ўзроўня бяспекі, бо апаратныя складнікі ў даляглядзе таксама могуць быць цалкам верыфікаваныя, чаго немагчыма дамагчыся для прапрыетарных апаратных архітэктур.
Пры верыфікацыі seL4 мяркуецца, што абсталяванне працуе як заяўлена і спецыфікацыя цалкам апісвае паводзіны сістэмы, але на справе абсталяванне не пазбаўлена ад памылак, што добра дэманструецца ўсплываючымі рэгулярна праблемамі ў механізме спекулятыўнага выканання інструкцый. Адкрытыя апаратныя платформы спрашчаюць інтэграцыю звязаных з бяспекай змен - напрыклад, для блакавання ўсіх магчымых каналаў уцечкі па іншых каналах, у якіх значна больш эфектыўна пазбавіцца ад праблемы апаратна, чым спрабаваць шукаць абыходныя шляхі праграмна.
Нагадаем, што ахітэктура seL4 вынасам частак для кіравання рэсурсамі ядра ў прастору карыстальніка і прымянення для такіх рэсурсаў тых жа сродкаў размежавання доступу, як для карыстацкіх рэсурсаў. Мікраядро не падае гатовых высокаўзроўневых абстракцый для кіравання файламі, працэсамі, сеткавымі злучэннямі і да т.п., замест гэтага яно падае толькі мінімальныя механізмы для кіравання доступам да фізічнай адраснай прасторы, перапыненням і рэсурсам працэсара. Высокаўзроўневыя абстракцыі і драйверы для ўзаемадзеяння з абсталяваннем рэалізуюцца асобна-над мікраядра ў форме задач, якія выконваюцца на карыстацкім узроўні. Доступ такіх задач да наяўных у мікраядра рэсурсаў арганізуецца праз азначэнне правіл.
RISC-V падае адкрытую і гнуткую сістэму машынных інструкцый, якая дазваляе ствараць мікрапрацэсары для адвольных абласцей ужывання, не патрабуючы пры гэтым адлічэнняў і не накладаючы ўмоў на выкарыстанне. RISC-V дазваляе ствараць цалкам адчыненыя SoC і працэсары. У цяперашні час на базе спецыфікацыі RISC-V рознымі кампаніямі і супольнасцямі пад рознымі вольнымі ліцэнзіямі (BSD, MIT, Apache 2.0) некалькі дзясяткаў варыянтаў ядраў мікрапрацэсараў, SoC і ўжо вырабляных чыпаў. Падтрымка RISC-V прысутнічае пачынальна з выпускаў Glibc 2.27, binutils 2.30, gcc 7 і ядры Linux 4.15.
Крыніца: opennet.ru