Google енгізілген аппараттық құралдар үшін қауіпсіз операциялық жүйені құруға бағытталған KataOS жобасына қатысты әзірлемелердің ашылғанын жариялады. KataOS жүйесінің құрамдас бөліктері Rust тілінде жазылған және seL4 микроядросының үстінде жұмыс істейді, ол үшін RISC-V жүйелерінде сенімділіктің математикалық дәлелі берілген, бұл код ресми тілде көрсетілген сипаттамаларға толығымен сәйкес келетінін көрсетеді. Жоба коды Apache 2.0 лицензиясы бойынша ашық.
Жүйе RISC-V және ARM64 архитектурасына негізделген платформаларға қолдау көрсетеді. Аппараттық құралдың жоғарғы жағындағы seL4 және KataOS ортасының жұмысын имитациялау үшін әзірлеу процесінде Renode құрылымы пайдаланылады. Анықтамалық іске асыру ретінде KataOS жүйесін OpenTitan платформасына негізделген қауіпсіз чиптермен біріктіретін Sparrow аппараттық-бағдарламалық кешені ұсынылады. Ұсынылған шешім логикалық тексерілген операциялық жүйе ядросын OpenTitan платформасы мен RISC-V архитектурасы арқылы құрастырылған сенімді аппараттық құрамдастармен (RoT, Root of Trust) біріктіруге мүмкіндік береді. Болашақта KataOS кодынан басқа Sparrow барлық басқа компоненттерін, соның ішінде аппараттық компонентті ашу жоспарлануда.
Платформа арнайы қорғау деңгейін және ақаулардың жоқтығын растауды талап ететін құпия ақпаратты машиналық оқытуға және өңдеуге арналған қосымшаларды іске қосуға арналған мамандандырылған чиптерде қолдануды ескере отырып әзірленуде. Мұндай қолданбалардың мысалдарына адамдардың кескіндері мен дауыстық жазбаларды басқаратын жүйелер жатады. KataOS сенімділігін тексеруді қолдану жүйенің бір бөлігі істен шыққан жағдайда, ақаулық жүйенің қалған бөлігіне және, атап айтқанда, ядроға және маңызды бөліктерге таралмауын қамтамасыз етеді.
seL4 архитектурасы ядро ресурстарын басқаруға арналған бөліктерді пайдаланушы кеңістігіне жылжытумен және пайдаланушы ресурстары сияқты ресурстарға бірдей қатынасты басқару құралдарын қолданумен ерекшеленеді. Микроядро файлдарды, процестерді, желілік қосылымдарды және т.б. басқару үшін дайын жоғары деңгейлі абстракцияларды қамтамасыз етпейді, оның орнына ол физикалық мекенжай кеңістігіне, үзілістерге және процессор ресурстарына қол жеткізуді басқарудың ең аз механизмдерін ғана қамтамасыз етеді. Аппараттық құралдармен әрекеттесу үшін жоғары деңгейлі абстракциялар мен драйверлер пайдаланушы деңгейіндегі тапсырмалар түрінде микроядроның жоғарғы жағында бөлек жүзеге асырылады. Мұндай тапсырмалардың микроядроға қолжетімді ресурстарға қол жеткізуі ережелерді анықтау арқылы ұйымдастырылады.
Қосымша қорғау үшін микроядродан басқа барлық құрамдас бөліктер Rust бағдарламасында қауіпсіз бағдарламалау әдістерін қолдана отырып әзірленеді, бұл босатудан кейін жадқа қол жеткізу, нөлдік көрсеткіш сілтемелері және буфердің асып кетуі сияқты мәселелерге әкелетін жад қателерін азайтады. Rust тілінде seL4 ортасындағы қолданбаларды жүктеуші, жүйелік қызметтер, қолданбаларды әзірлеуге арналған фреймворк, жүйелік шақыруларға қол жеткізу үшін API, процесс менеджері, динамикалық жадты бөлу механизмі және т.б. жазылған. Тексерілген жинақ seL4 жобасы әзірлеген CAmkES құралдар жинағын пайдаланады. CAmkES үшін құрамдастарды Rust ішінде де жасауға болады.
Rust компиляция уақытында анықтамалық тексеру, нысанды иелену және нысанның қызмет ету мерзімін бақылау (аумақтары) арқылы және орындалу уақытында жадқа кірудің дұрыстығын бағалау арқылы жад қауіпсіздігін қамтамасыз етеді. Rust сонымен қатар бүтін сандардың толып кетуінен қорғауды қамтамасыз етеді, айнымалы мәндерді пайдалану алдында инициализациялауды талап етеді, әдепкі бойынша өзгермейтін сілтемелер мен айнымалылар тұжырымдамасын пайдаланады және логикалық қателерді азайту үшін күшті статикалық теруді ұсынады.
Ақпарат көзі: opennet.ru