РИСЦ-В је верификовао микро језгро сеЛ4 на својим РВ64 процесорима

Фондација РИСЦ-В саопштила је да је верификовала како микројезгро функционише сеЛ4 у системима са архитектура скупа инструкција РИСЦ-В. У коме се поступак верификације своди на математички тест поузданости сеЛ4, што указује на потпуну усклађеност са спецификацијама наведеним у формалном језику.

Тестирање поузданости омогућава употребу сеЛ4 у критичним системима заснованим на РИСЦ-В процесорима РВКСНУМКС, који захтева виши ниво поузданости и не гарантује неуспех.

Програмери софтвера који раде на врху сеЛ4 језгра могу бити потпуно уверени да се у случају квара на једном делу система, овај квар неће проширити на остатак система, а посебно на његове критичне делове.

О сеЛ4

Архитектура сеЛ4 је познат по уклањању делова за управљање ресурсима језгра у корисничком простору и користите исте методе контроле приступа за такве ресурсе као и за корисничке ресурсе.

Микрокернел не пружа апстракције на високом нивоу већ припремљен за управљање датотекама, процесима, мрежним везама итд., али уместо тога пружа само минималне механизме за контролу приступа физичком адресном простору, прекиди и ресурси процесора.

Апстракције на високом нивоу и контролери за интеракцију са рачунаром имплементирани су одвојено на врх микрокера у облику задатака извршених на нивоу корисника.

Приступ таквих задатака ресурсима који су доступни у микро језгри организован је кроз дефинисање правила.

РИСЦ-В пружа отворен и флексибилан систем машинских упутстава која омогућава стварање микропроцесора за произвољне апликације, без потребе за одбитцима и без наметања услова употребе.

РИСЦ-В вам омогућава да креирате потпуно отворене процесоре и СоЦ-ове. Тренутно, на основу РИСЦ-В спецификације, неколико компанија и заједница под разним бесплатним лиценцама (БСД, МИТ, Апацхе 2.0) развија неколико десетина варијанти већ произведених микропроцесорских језгара, СоЦ-ова и чипова.

Подршка за РИСЦ-В постоји од издавања Глибц 2.27, бинутилс 2.30, гцц 7 и језгра Линук 4.15.

О сеЛ4 тестирању микрокера

У почетку, микрокера сеЛ4 је верификован за 32-битне АРМ процесоре, И касније за к86 64-битне процесоре.

Примећено је да комбинација РИСЦ-В отворене хардверске архитектуре са отвореним микројезром сеЛ4 ће постићи нови ниво сигурности, јер се хардверске компоненте у будућности такође могу у потпуности верификовати, што је немогуће постићи за власничке хардверске архитектуре.

Када проверимо сеЛ4, морамо претпоставити да хардвер исправно ради (односно, како је наведено). То претпоставља да на првом месту постоји недвосмислена спецификација, што није случај са свим хардвером. 

Али чак и када таква спецификација постоји, а формална је (то јест, претворена у математички формализам који подржава математичко резоновање о њеним својствима), како да знамо да она заправо бележи понашање хардвера? 

Реалност је таква да можемо бити прилично сигурни да није. Хардвер се не разликује од софтвера по томе што је и један и други баги.

Али имати отворени ИСА има предности које превазилазе могућност бесплатности. Један је тај што омогућава имплементацију хардвера отвореног кода.

Приликом провере сеЛ4, претпоставља се да опрема ради како је назначено и спецификација у потпуности описује понашање система, али у ствари опрема не садржи грешке, што добро показују проблеми који се редовно јављају у упутствима за спекулативни механизам извршења .

Отворене хардверске платформе поједностављују интеграцију промена везано за безбедност, на пример, за блокирање свих могућих канала цурења путем независних канала, где је много ефикасније хардверским путем решити проблем него покушати пронаћи решења софтверским путем.

Коначно, ако желите да сазнате више о томе, можете погледати напомену у следећи линк.