Микрокернел сеЛ4 је математички верификован за РИСЦ-В архитектуру

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

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

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

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

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

Извор: опеннет.ру