Google камтылган аппараттык камсыздоо үчүн коопсуз операциялык системаны түзүүгө багытталган KataOS долбооруна байланыштуу иштеп чыгууларды тапканын жарыялады. KataOS тутумунун компоненттери Rust тилинде жазылган жана seL4 микроядросунун үстүндө иштейт, ал үчүн RISC-V системаларында ишенимдүүлүктүн математикалык далили берилген, бул код расмий тилде көрсөтүлгөн спецификацияларга толугу менен дал келгенин көрсөтүүдө. Долбоордун коду Apache 2.0 лицензиясы боюнча ачык.
Система RISC-V жана ARM64 архитектурасына негизделген платформаларды колдоону камсыз кылат. seL4 жана KataOS чөйрөсүнүн иштешин аппараттык жабдыктын үстүндө моделдөө үчүн, иштеп чыгуу процессинде Renode алкагы колдонулат. Маалыматтык ишке ашыруу катары КатаОСту OpenTitan платформасынын негизиндеги коопсуз чиптер менен бириктирген Sparrow программалык-аппараттык комплекси сунушталат. Сунушталган чечим логикалык жактан текшерилген операциялык системанын өзөгүн OpenTitan платформасы жана RISC-V архитектурасы аркылуу курулган ишенимдүү аппараттык компоненттери (RoT, Trust Root) менен айкалыштырууга мүмкүндүк берет. KataOS кодунан тышкары, келечекте Sparrow башка бардык компоненттерин, анын ичинде аппараттык компонентти ачуу пландаштырылууда.
Платформа машинаны үйрөнүү жана жашыруун маалыматты иштетүү үчүн тиркемелерди иштетүү үчүн иштелип чыккан атайын чиптерде колдонууну эске алуу менен иштелип чыккан, алар коргоонун өзгөчө деңгээлин жана каталардын жоктугун ырастоону талап кылат. Мындай тиркемелердин мисалдарына адамдардын сүрөттөрүн жана үн жазууларын башкарган системалар кирет. KataOSтун ишенимдүүлүгүн текшерүүнү колдонуу системанын бир бөлүгү иштен чыкса, бузулуу системанын калган бөлүгүнө, атап айтканда, өзөккө жана критикалык бөлүктөргө жайылбай тургандыгын камсыздайт.
seL4 архитектурасы ядро ресурстарын колдонуучу мейкиндигине башкаруу үчүн бөлүктөрдү жылдыруу жана колдонуучу ресурстары сыяктуу ресурстар үчүн бирдей мүмкүнчүлүктү башкаруу куралдарын колдонуу менен өзгөчөлөнөт. Микроядро файлдарды, процесстерди, тармактык байланыштарды жана башкаларды башкаруу үчүн даяр жогорку деңгээлдеги абстракцияларды камсыз кылбайт, анын ордуна физикалык дарек мейкиндигине, үзгүлтүккө жана процессор ресурстарына кирүү мүмкүнчүлүгүн көзөмөлдөө үчүн минималдуу механизмдерди гана камсыз кылат. Жогорку деңгээлдеги абстракциялар жана аппараттык каражаттар менен иштешүү үчүн драйверлер колдонуучу деңгээлиндеги тапшырмалар түрүндө микроядронун үстүндө өзүнчө ишке ашырылат. Мындай милдеттерди микроядро үчүн жеткиликтүү ресурстарга жетүү эрежелерди аныктоо аркылуу уюштурулат.
Кошумча коргоо үчүн микро ядродон башка бардык компоненттер Rust программасында коопсуз программалоо ыкмаларын колдонуу менен иштелип чыккан, бул эстутум каталарын азайтып, эстутумга бошоткондон кийин кирүү, нөл көрсөткүчтү жокко чыгаруу жана буферди ашып кетүү сыяктуу көйгөйлөргө алып келет. Rustта seL4 чөйрөсүндөгү тиркеме жүктөгүч, система кызматтары, тиркемени иштеп чыгуу үчүн фреймворк, системалык чалууларга жетүү үчүн API, процесс менеджери, эстутумду динамикалык бөлүштүрүү механизми ж.б.у.с. жазылган. Текшерилген чогултуу үчүн seL4 долбоору тарабынан иштелип чыккан CAmkES инструменттери колдонулат. CAmkES үчүн компоненттер да Rust түзүлүшү мүмкүн.
Rust компиляция учурунда эстутумдун коопсуздугун маалымдама текшерүү, объектке ээлик кылуу жана объекттин өмүр боюна көз салуу (кошумчалар) аркылуу жана иштөө учурунда эстутумга кирүүлөрдүн тууралыгын баалоо аркылуу камсыздайт. Rust ошондой эле бүтүн сандардын ашып кетишинен коргоону камсыздайт, колдонуудан мурун өзгөрүлмө маанилерди инициализациялоону талап кылат, демейки боюнча өзгөрүлгүс шилтемелер жана өзгөрмөлөр түшүнүгүн колдонот жана логикалык каталарды азайтуу үчүн күчтүү статикалык терүүнү сунуш кылат.
Source: opennet.ru