RISC-V өздерінің RV4 процессорларында seL64 микро ядроларын тексерді

RISC-V қоры растағанын хабарлады микро ядроның қалай жұмыс істейтіні жүйелеріндегі seL4 нұсқаулар жиынтығының архитектурасы RISC-V. Мұнда тексеру процесі seL4 сенімділігінің математикалық сынағына дейін азаяды, бұл ресми тілде көрсетілген сипаттамаларға толық сәйкес келетіндігін көрсетеді.

Сенімділікті тексеру seL4-ті RISC-V процессорларына негізделген маңызды жүйелерде пайдалануға мүмкіндік береді RV64, бұл сенімділіктің жоғарырақ деңгейін талап етеді және істен шығуға кепілдік бермейді.

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 ядросы шыққаннан бері бар.

SeL4 микро ядроларын сынау туралы

Бастапқыда микро ядролар seL4 32 биттік ARM процессорлары үшін тексерілдіжәне кейінірек x86 64 биттік процессорлар үшін.

RISC-V ашық аппаратураның архитектурасы мен ашық микро ядролы үйлесімділігі байқалады seL4 қауіпсіздіктің жаңа деңгейіне жетеді, өйткені болашақта аппараттық компоненттер толығымен тексерілуі мүмкін, бұл меншікті аппараттық архитектура үшін қол жеткізу мүмкін емес.

Біз seL4-ті тексерген кезде, біз аппараттық құрал дұрыс жұмыс істеп тұр деп ойлауымыз керек (яғни көрсетілгендей). Бұл бірінші кезекте бірыңғай сипаттама бар деп болжайды, бұл барлық аппараттық құралдарға сәйкес келмейді. 

Бірақ мұндай спецификация болған кезде де және ол формальды болғанда да (яғни оның қасиеттері туралы математикалық пайымдауларды қолдайтын математикалық формализмге айналған), біз оның аппараттық құралдардың іс-әрекетін шынымен ұстап тұрғанын қайдан білеміз? 

Шындығында, олай емес екеніне сенімді бола аламыз. Аппараттық құралдардың бағдарламалық жасақтамадан айырмашылығы жоқ, өйткені екеуі де арбалар.

Бірақ ашық АХС-тың роялтиден тыс артықшылықтары бар. Біреуі - бұл ашық бастапқы жабдықты іске асыруға мүмкіндік береді.

SeL4-ті тексерген кезде жабдық көрсетілгендей жұмыс істейді және спецификация жүйенің жұмысын толығымен сипаттайды деп есептеледі, бірақ іс жүзінде жабдық қателіктерден босатылмайды, бұл спекулятивті орындау механизмінде үнемі туындайтын мәселелермен жақсы көрінеді. .

Ашық аппараттық платформалар өзгерістерді біріктіруді жеңілдетеді қауіпсіздікке байланысты, мысалы, бөгде арналар арқылы барлық мүмкін ағып жатқан арналарды бұғаттау, мұнда бағдарламалық жасақтама арқылы шешімдер табудан гөрі аппараттық құралдармен проблемадан құтылу әлдеқайда тиімді.

Сонымен, егер сіз бұл туралы көбірек білгіңіз келсе, ішіндегі жазбадан кеңес ала аласыз келесі сілтеме.


Мақаланың мазмұны біздің ұстанымдарымызды ұстанады редакторлық этика. Қате туралы хабарлау үшін нұқыңыз Мұнда.

2 пікір, өз пікіріңізді қалдырыңыз

Пікіріңізді қалдырыңыз

Сіздің электрондық пошта мекен-жайы емес жарияланады. Міндетті өрістер таңбаланған *

*

*

  1. Деректерге жауапты: Мигель Анхель Гатан
  2. Деректердің мақсаты: СПАМ-ны басқару, түсініктемелерді басқару.
  3. Заңдылық: Сіздің келісіміңіз
  4. Деректер туралы ақпарат: заңды міндеттемелерді қоспағанда, деректер үшінші тұлғаларға жіберілмейді.
  5. Деректерді сақтау: Occentus Networks (ЕО) орналастырған мәліметтер базасы
  6. Құқықтар: Сіз кез-келген уақытта ақпаратты шектей, қалпына келтіре және жоя аласыз.

  1.   біреуі дижо

    Мен үшін бұл процессор мені қатты шақыратын нәрсе. Біз сатып алатын компьютерді жасау тек кейбір майлы компьютер иттері үшін қалады.

    ARM мәселесі - мені сықырлататын нәрсе, біз Huawei-мен санкциялармен не болғанын көрдік. Менің RISC-V үшін бұл барлық деңгейлерде әлдеқайда жақсы шешім екендігі анық. Қазіргі уақытта Huawei бұған назар аударып отыр, мүмкін болашақта оларда осындай микро бар жабдықтар болады. Егер солай болса, оны қабылдайтын компаниялардың саны арта түсетіні сөзсіз, ал мен үшін бұл дистрибьюторлар тек ARM ғана емес, сонымен қатар көптеген адамдар үшін қолдау көрсететін идеал болады.

    1.    Григорий Рос дижо

      + 10