Кампанія Google абвясціла аб адкрыцці напрацовак, звязаных з праектам KataOS, накіраваным на стварэнне абароненай аперацыйнай сістэмай для ўбудаванага абсталявання. Сістэмныя кампаненты KataOS напісаны на мове Rust і выконваюцца па-над мікраядром seL4, для якога на сістэмах RISC-V прадстаўлена матэматычны доказ надзейнасці, якое сведчыць аб поўнай адпаведнасці кода спецыфікацыям, зададзеным на фармальнай мове. Код праекту адкрыты пад ліцэнзіяй Apache 2.0.
У сістэме забяспечана падтрымка платформаў на базе архітэктур RISC-V і ARM64. Для сімуляцыі працы seL4 і асяроддзі KataOS па-над абсталяваннем падчас працэсаў распрацоўкі выкарыстоўваецца фрэймворк Renode. У якасці эталоннай рэалізацыі прапанаваны праграмна-апаратны комплекс Sparrow, які камбінуе KataOS з абароненымі чыпамі на базе платформы OpenTitan. Прапанаванае рашэнне дазваляе сумясціць лагічна верыфікаванае ядро аперацыйнай сістэмы з годнымі даверу апаратнымі кампанентамі (RoT, Root of Trust), пабудаванымі з выкарыстаннем платформы OpenTitan і архітэктуры RISC-V. Апроч кода KataOS у наступным плануецца адкрыццё і ўсіх астатніх кампанентаў Sparrow, уключаючы апаратны складнік.
Платформа развіваецца з аглядкай на ўжыванне ў спецыялізаваных чыпах, разлічаных на выкананне прыкладанняў для машыннага навучання і апрацоўкі канфідэнцыйнай інфармацыі, якім патрабуецца адмысловы ўзровень абароны і пацверджанні адсутнасці збояў. У якасці прыкладу падобных прыкладанняў прыводзяцца сістэмы, якія маніпулююць выявамі людзей і галасавымі запісамі. Выкарыстанне ў KataOS верыфікацыі надзейнасці гарантуе, што ў выпадку збою ў адной частцы сістэмы, гэты збой не распаўсюдзіцца на астатнюю сістэму і, у прыватнасці, на ядро і крытычныя часткі.
Архітэктура seL4 характэрная вынасам частак для кіравання рэсурсамі ядра ў прастору карыстача і ўжыванні для такіх рэсурсаў тых жа сродкаў размежавання доступу, як для карыстацкіх рэсурсаў. Мікраядро не падае гатовых высокаўзроўневых абстракцый для кіравання файламі, працэсамі, сеткавымі злучэннямі і да т.п., замест гэтага яно падае толькі мінімальныя механізмы для кіравання доступам да фізічнай адраснай прасторы, перапыненням і рэсурсам працэсара. Высокаўзроўневыя абстракцыі і драйверы для ўзаемадзеяння з абсталяваннем рэалізуюцца асобна-над мікраядра ў форме задач, якія выконваюцца на карыстацкім узроўні. Доступ такіх задач да наяўных у мікраядра рэсурсаў арганізуецца праз азначэнне правіл.
Для дадатковай абароны ўсе кампаненты, акрамя мікраядра, першапачаткова развіваюцца на мове Rust з выкарыстаннем бяспечных прыёмаў праграмавання, якія мінімізуюць памылкі пры працы з памяццю, якія прыводзяць да такіх праблем як зварот да вобласці памяці пасля яе вызвалення, разнайменаванне нулявых паказальнікаў і вынахад за межы буфера. На Rust у тым ліку напісаны загрузнік прыкладанняў у асяроддзі seL4, сістэмныя сэрвісы, фрэймворк для распрацоўкі прыкладанняў, API для доступу да сістэмных выклікаў, мэнэджар працэсаў, механізм дынамічнага размеркавання памяці і да т.п. Для верыфікаванай зборкі задзейнічаны інструментар CAmkES, які развіваецца праектам seL4. Кампаненты для CAmkES таксама могуць стварацца на мове Rust.
Бяспечная праца з памяццю забяспечваецца ў Rust падчас кампіляцыі праз праверку спасылак, адсочванне валодання аб'ектамі і ўлік часу жыцця аб'ектаў (вобласці бачнасці), а таксама праз адзнаку карэктнасці доступу да памяці падчас выканання кода. Rust таксама падае сродкі для абароны ад цэлалікіх перапаўненняў, патрабуе абавязковай ініцыялізацыі значэнняў зменных перад выкарыстаннем, ужывае канцэпцыю нязменнасці (immutable) спасылак і зменных па змаўчанні, прапануе моцную статычную тыпізацыю для мінімізацыі лагічных памылак.
Крыніца: opennet.ru