Микро ядрои seL4 барои меъмории RISC-V аз ҷиҳати математикӣ санҷида шудааст

Бунёди RISC-V хабар дод дар бораи тафтиши кори микро ядро seL4 дар системаҳои дорои меъмории маҷмӯи дастурҳои 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

Илова Эзоҳ