seL4 микро ядросу RISC-V архитектурасы үчүн математикалык жактан текшерилген

RISC-V Foundation билдирди микро ядронун иштешин текшерүү жөнүндө 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 релизинен бери бар.

Source: opennet.ru

Комментарий кошуу